2015-12-06 24 views
6

L'articolo Simpler, Easier! afferma che potrebbe essere possibile codificare i sistemi di tipi dipendenti anche senza la presenza di "Pi", ovvero, è possibile riutilizzare il costruttore "Lam" per questo. Ma come può essere vero, se "Pi" e "Lam" sono trattati in modo diverso in alcuni casi?È effettivamente possibile rimuovere "Pi" da Calculus of Constructions?

Inoltre, è possibile rimuovere "Star"? Penso che potresti sostituire tutte le occorrenze di "λ x. X" (id).

risposta

6

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).

+0

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

+0

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

+1

@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