Definizione di un tipo

Penso che la tua vera lotta qui sia una con decidibilità, che è totalmente comprensibile in questo contesto, quindi parliamone per un momento.

La tua prima menzione di un sistema di tipi è abbastanza semplice, in pratica hai un set e tutto in quel set rappresenta il suo tipo. Ora, il tipo di ognuno di questi elementi è sfortunatamente indecidibile perché a questo punto sono solo valori indipendenti. Questo tipo di ostacola l'intero scopo di un sistema di tipi ed è davvero più indicativo di un sistema non tipizzato. Questo è simile al calcolo lambda non tipizzato dove ci sono insiemi ma nessun identificatore legato insieme ai valori per delineare il loro insieme recintato.

Quindi ti sei reso conto di questa indecidibilità e hai deciso una soluzione che ha senso: legare il valore a un alias che identifica il suo insieme racchiudendolo come "tipo" in modo da avere ogni valore come tupla (tipo, valore). Questo è molto simile al lambda-mu calcolo che è in effetti un'estensione del sopra menzionato calcolo lambda sopra descritto (o potrebbe essere più vicino a semplicemente digitato lambda calcolo correggimi se mi sono confuso). Comunque ah; c'è una presa lì, di nuovo quale tipo è legato a un input e l'output impostato per una funzione è indecidibile in alcune situazioni.

Quindi, un altro raffinamento che decidi, va bene dettero i tipi di input e output e i possibili elementi nella mia funzione! Aha! Ora abbiamo reso la determinazione dei tipi abbastanza decidibili! Anche se sembra un po 'cruft, e ora abbiamo bisogno di definizioni di tipo ricorsive su tutti i tipi di astrazione per continuare a costruire pezzi di pezzi qui, questo sembra un po' complicato e oneroso no? Bene, sì, lo è. Sfortunatamente questo è esattamente come funziona e ora hai inserito Dattilografia dipendente .

La gravosità parla di uno dei motivi per cui le implementazioni di questo tipo di sistema sono così rare. Comunque c'è un altro problema in questo tipo di sistema ed è un po 'stupido: finora non si sa come fare un controllo di totalità veramente (questo è il controllo che si ottiene quando si rende decidibile il sistema di tipo che è ciò che sembri essere dopo) tipo di sistema che può essere completato. Il problema è che quando si effettua il controllo della totalità, tutti i possibili input e output sono garantiti dal compilatore, il che significa che ora abbiamo la decidibilità della terminazione dei programmi, quindi non problema di interruzione necessario per la completezza della funzionalità.

Molte lingue complete di non turing sono ancora molto utili quindi non è una necessità, e questi tipi di linguaggi sono spesso usati per gli assistenti di prove in cui il codice detta un sacco di possibilità di input e output e la compilazione stessa dice in pratica "Sì , questo è un sistema logico valido. " dimostrando così tutto ciò che il codice ha dichiarato.

Perché qualcuno deve farlo, mi avvicinerò a questo da una prospettiva più matematica. I tipi in effetti assomigliano agli insiemi, ma è più piacevole pensarli "nominalmente" piuttosto che "strutturalmente".

Questo significa essenzialmente che a : Foo /= a : Bar .

Ora, con questo in mente, possiamo pensare ai tipi come insiemi, ma questo è piuttosto difficile da discutere poiché i set sono spesso visualizzati strutturalmente. Le cose si fanno interessanti quando le consideriamo come oggetti di una categoria. Quindi le funzioni totali tra i tipi (una funzione che non è mai indefinita) formano frecce in questa categoria. Mi riferirò a questa categoria come STLC .

L'insieme delle funzioni di identità specializzate (id :: Foo -> Foo...) forma la composizione della freccia e della composizione dell'identità f . g == f (g x) form. Ora che abbiamo una categoria, è piacevole pensare ad altri concetti teorici di categoria, i due interessanti sono prodotti ed esponenziali.

Per i prodotti consideriamo 3 operazioni

cross  : A -> B -> A X B
first  : A X B  -> A
second : A X B  -> B

Quindi notiamo che le tuple formano prodotti in STLC .

Quindi considera gli esponenziali. Questi formano l'interessante spina dorsale delle funzioni di ordine superiore. Vogliamo 2 funzioni per alcune frecce f : A X B -> C

curry(f) : A X B   -> C^B
eval(f)  : C^B X B -> C

Questo formalizza la nozione dietro le funzioni di ordine superiore, sono gli esponenziali di STLC . Quindi una funzione

f : A -> (B -> C)

In realtà è una freccia da A a% esponenzialeC^B.

C'è una freccia unica per ogni tipo dal tipo di falsy. Questo è un tipo senza testimoni di alcun tipo. In Haskell

data Falsy =

Ultimo ma non meno importante, considera un oggetto terminale T . Questo è banalmente formato da un tipo con esattamente un testimone. Tradizionalmente questo è chiamato Unit o True . In Haskell

data Unit = Unit

Con questi, possiamo effettivamente stabilire quale sia la rappresentazione di un valore, è un "punto" (una freccia da Unit -> A ). In un sistema di tipo sano, la categoria che forma è ben definita. Oppure, ci sono abbastanza frecce da p : Unit -> A in modo che se per tutto p , f . p = g . p , poi f = g .

La categoria che ho descritto qui descrive i sistemi di tipi di Haskell, ML e della maggior parte degli altri linguaggi tradizionali.

Quindi come risposta diretta alla tua domanda. Un tipo è un oggetto di una categoria cartesiana chiusa con gli oggetti iniziale e finale che sono rispettivamente curry-howard False e True, valori di funzione che formano esponenziali e frecce e coppie che formano prodotti.