Questo è solo un sovraccarico come (a, b) in Haskell: può essere sia un tipo che un valore. Puoi utilizzare lo stesso binder per Π e λ e typechecker deciderà dal contesto che intendi. Se si TYPECHECK un legante contro un altro, poi il primo è λ e la seconda è Π - ed è per questo che non si può senza ambiguità sostituire * con λ x . x - perché allora l'ex legante potrebbe essere Π e la seconda è * (* come legante non ha senso per me). C'è un problema più grande con ∀ = λ e * = λ x . x: dalla transitività * = ∀ x . x, che è un modo comune di postulare False - questo tipo deve essere disabitato in un sistema audio, quindi non si avranno affatto tipi.
c'era un filo di recente su Coq-club "somiglianze tra forall e divertente" (gmane.org mi dà "No tale messaggio", è solo a me?), Ecco alcuni stralci:
Dominic Mulligan:
Ed ecco un altro con una piccola bibliografia che punta al lavoro simile:
http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/jfp05.pdf
Ironia della sorte, secondo quel documento Coquand ha presentato per la prima volta il Calcolo delle costruzioni con un unico raccoglitore unificato, seguendo una convenzione stabilita da De Bruijn in AutoMath.
Thorsten Altenkirch:
funzioni e il loro tipo sono molto diversi concetti, anche se presentano alcuni superficiale somiglianza sintattica.
Soprattutto per il nuovo arrivato questa identificazione è molto confusa e completamente fuorviante. Penso che uno dovrebbe capire il tipo di concetti teorici da cosa significano e non come sembrano.
Andreas Abel:
Il mio studente Matthias Benkard anche lavorato su un tale sistema, vedere "Tipo controllo senza Tipi"
http://www.cse.chalmers.se/~abela/benkardThesis.pdf
Si noti che la sistema descritto al primo collegamento ha la riduzione Π (espuoi applicare i pi-tipi proprio come lambdas) - il tuo sistema lo avrà anche tu, se unifichi Π e λ internamente (al contrario di sintatticamente). E il sistema descritto al secondo link unifica tipi e valori
Una conseguenza immediata è l'assenza di distinzione tra tipi ei loro abitanti: Ogni valore è un tipo contenente stessa e tutte le sue parti; e viceversa, ogni tipo è un valore composito composto dai suoi abitanti.
quindi non c'è davvero un solo legante (ad eccezione di let e forse fix).
Spiacente, non capisco come sia possibile sapere quando dovrebbe essere un Pi e quando dovrebbe essere un λ per contesto. Potresti approfondire un po 'la distinzione? – MaiaVictor
Come un semplice esempio, 'λ (a: *) -> λ (x: a) -> a' applicato a se stesso. Cosa succederebbe? Poiché 'a: *' e tutto è un tipo, questo termine non dovrebbe accettare tutto? – MaiaVictor
@Viclib, ho un piccolo tipografo per una teoria del tipo dipendente di base, cercherò di unire 'Π' e' λ'. Se hai '[a: *] -> [x: a] -> a' e lo applichi a se stesso, il primo raccoglitore si comporta come un lambda e il risultato è' [x: [a: *] -> [x: a] -> a] -> a'. – user3237465