bonjour,
 
je travaille sur la théorie des types et pourtant je n'arrive pas à définir ce que c'est précisément
j'ai utilisé google mais la seule réponse que je trouve est : "c'est une formalisation"
 
est-ce quelqu'un aurait des indices pour m'aider ?
 
je ne demande pas nécesairement une explication de 10 pages mais quelques lignes pour que je puisse mieux comprendre
Merci d'avance

Me rappelle pas en avoir entendu parler...
C'est dans quel domaine ?

informatique théorique, récriture
 
je sais à quoi ça sert mais pas ce que c'est
 
exemple extrait d'une thèse :
"
De nombreux assistants à la démonstration mathématique sont à l'heure actuelle basés sur
ce principe, tels que les systèmes Coq [11], LEGO [43], NuPrl [36], ALF [44] et Agda pour n'en
citer que quelques-uns. Ces logiciels sont basés sur un formalisme - la théorie des types, ou
l'une de ses nombreuses variantes - qui se distingue de la théorie des ensembles non seulement
en considérant les programmes comme des objets primitifs, mais surtout en procédant à une
identification complète des notions de preuve et de proposition avec les notions de programme
et de type respectivement.
Pourtant, contrairement au lambda-calcul pur ou aux langages de la famille ML, la théorie des
types est généralement basée sur une approche dans laquelle chaque objet est "décoré" avec un
certain nombre d'annotations de type qui permettent de déterminer le type de cet objet sans
la moindre ambiguïté. En particulier, la théorie des types ne permet de construire que des
fonctions dont le domaine de définition est donné à l'avance, réintroduisant ainsi un peu de
la conception riemannienne là où les succès du -calcul pur semblaient indiquer au contraire
que l'on pouvait enfin se passer de la notion de domaine de définition "

vous vous égarez messieurs
je vous parle de théorie informatique

Ca doit être pour faire la distinction entre les langages faiblement typés (les trucs de porc comme asp) et les langages fortement typés (comme le C).
 
Me semble avoir vu ça il y a longtemps en info théo, hummm...
 
Je dirais : c'est une classe pour décrire une entité. (mots choisis de bon pour être particulièrement dangeureux, attention)  
 
Effectivement ça se rapproche de la théorie ensembliste. Une valeur de type Int peut être contenu dans une variable de type Float, mais pas l'inverse.
 
Ceci dit, ça reste trés vague...

 
merci de participer
 
le problème est que j'ai des liens mais qu'aucun ne définit ce que c'est
pour le moment, je comprends ça comme une formalisatin permettant de représenter les programmes à l'aide d'un système de type, ainsi on peut utiliser le principe qui a été démontré disant qu'un élément bien typé est normalisable, ie qu'il a une terminaison.

Up parce que 1/ ça m'intéresse, et 2/ j'adorerais qu'une dame m'offre des bonbons!

leg9 > je te promets plus de détails à ce sujet puisque l'an prochain, cela sera le domaine de mon DEA

voilà
j'ai quelques nouvelles pistes pour définir ce qu'est la théorie des types.
 
En étudiant la logique, on a eu 2 axes contradictoires pour considérer les prédicats :
  1. tout prédicat est un objet
  2. tout prédicat peut s'appliquer à tout objet
 
si on a comme base 1 et 2, on obtient le paradoxe de Russel.
On a exploré les 2 pistes :
  . La théorie des ensembles consiste à dire 1 est vrai et 2 est faux.
  . La théorie des types consiste à dire 1 est faux et 2 est vrai.
 
voilà.
Dès que je sais mieux l'expliquer je continue

Sa va peut etre etre a coté de la plaque ...
http://membres.lycos.fr/pierret/thobjd04.htm

non ça ne correspond pas au sujet mais c'est une forme d'utilisation de la théorie
 
 
merci d'essayer

Essaie de faire venir nraynaud sur ton topic ( un forumeur qui passe de temps en temps sur programmation ) qui devrait peut être pouvoir répondre à ta question.

 
c ptet paske asp n'est pas un langage mais une couche de presentation   (pour .net j'entend).

Un type est un attribut, une appartenance à une classe de caractéristiques précise.
 
Après je pense qu'on peut descendre plus bas : à savoir comment découper les types de façons à ce que chaque type soit unique, et donc à chercher ce qu'est une caractéristique.
 
J'aime : c'est de l'abstraction pure