C'est juste une surcharge comme (a, b) dans Haskell: ça peut être à la fois un type et une valeur. Vous pouvez utiliser le même classeur pour Π et λ et typechecker décidera du contexte que vous voulez dire. Si vous Typecheck un liant contre un autre, le premier est λ et celle-ci est Π - et c'est la raison pour laquelle vous ne pouvez pas remplacer sans ambiguïté * avec λ x . x - car alors l'ancien liant pourrait être Π et celle-ci est * (* comme liant ça n'a aucun sens pour moi). Il ya un plus gros problème avec ∀ = λ et * = λ x . x: par la transitivité * = ∀ x . x, qui est un moyen courant de postuler False - ce type doit être inhabité dans un système de son, donc vous n'aurez aucun type du tout.
Il y avait un fil récent sur Coq-club "Similitudes entre forall et fun" (gmane.org me donne "Un tel message", est-il juste moi?), Voici quelques extraits:
Dominic Mulligan:
Et voici une autre avec une petite bibliographie montrant un travail similaire:
http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/jfp05.pdf
Ironie du sort, selon ce document, Coquand a présenté pour la première fois le Calcul de Constructions avec un seul liant unifié, suivant une convention établie par De Bruijn dans AutoMath.
Thorsten Altenkirch:
Une fonction et son type sont des concepts très différents, même si elles ont une certaine similitude syntaxique superficielle.
Surtout pour le nouveau venu cette identification est très confuse et complètement trompeuse. Je pense que l'on devrait comprendre les concepts théoriques de ce qu'ils signifient et non comment ils ressemblent.
Andreas Abel:
Mon étudiant Matthias Benkard a également travaillé sur un tel système, voir "Type Vérification sans Types"
http://www.cse.chalmers.se/~abela/benkardThesis.pdf
Notez que la système décrit au premier lien a Π-réduction (c.-à-d.vous pouvez appliquer des types pi comme des lambdas) - votre système l'aura aussi, si vous unifiez Π et λ en interne (par opposition à syntaxiquement). Et le système décrit au deuxième lien unifie les types et les valeurs
Une conséquence immédiate est l'absence de toute distinction entre types et leurs habitants: Chaque valeur est un type contenant lui-même et toutes ses parties; et inversement, chaque type est une valeur composite constituée de ses habitants.
donc il est vraiment juste un liant (sauf pour les let et peut-être fix).
Désolé, je ne comprends pas comment vous savez quand ça devrait être un Pi et quand ça devrait être un λ par contexte. Pourriez-vous élaborer un peu sur la distinction? – MaiaVictor
À titre d'exemple simple, 'λ (a: *) -> λ (x: a) -> a' appliqué à lui-même. Ce qui se passerait? Puisque 'a: *' et que tout est un type, ce terme n'accepterait-il pas tout? – MaiaVictor
@Viclib, j'ai un peu typechecker pour une théorie de type dépendante de base, je vais essayer de fusionner 'Π' et' λ'. Si vous avez '[a: *] -> [x: a] -> a' et que vous l'appliquez, le premier classeur agit comme un lambda et le résultat est [[: [x: a] -> a] -> a'. – user3237465