Domanda sul “Tutorial sull’implementazione del lambda calcolo tipizzato in modo dipendente”
-
29-09-2020 - |
Domanda
Ho un leggero problema tecnico con Questo meraviglioso tutorial.A pagina 5 il tutorial parla delle regole di digitazione per i Lambda Simply Typed e presenta il giudizio seguente come derivabile tramite le regole nella figura 3.
Non ho potuto dimostrare nessuno dei due id
né const
per lo stesso motivo.Prendiamo ad esempio il id
esempio.
- Supponiamo che sto cercando una regola di controllo del tipo
CHK
.Dice che percheck types
Dovrei prima eseguire l'inferenza e poi confrontare il risultato con quello che mi aspetto. - Per fare l'inferenza sull'applicazione, devo usare il file
APP
regola che mi costringe subito a dedurre la tipologia del lato sinistro della domanda, vale a dire(id :: α -> α)
- Per farlo sto utilizzando il file
ANN
regola che mi obbliga a verificarloα -> α
è un tipo (e posso dimostrarlo senza problemi).Poi l'ho messo nudoid
simbolo e devo dimostrare che è il tipoα -> α
. - Infine, ecco un problema.Per fare ciò dovrò usare
var
regola, che richiede il tipo diid
da impostare esplicitamente nel contesto Gamma, ma non viene fatto, quindi la dimostrazione sta cadendo a pezzi.
Soluzione
$\mathsf{id}$ E $\mathsf{const}$ non sono variabili del calcolo, ma zucchero sintattico per $\lambda x ightarrow x$ E $\lambda x ightarrow \lambda y ightarrow x$ rispettivamente.Ciò è affermato alla fine del §2.2 e sottilmente trasmesso dall'uso di un carattere sans-serif anziché il corsivo (si tratta di una convenzione tipografica di questo particolare documento, non di una convenzione comune).
Quindi, ad esempio, il giudizio sul tipo$$ Alpha ::\ast, y ::\alpha \vdash (\mathsf{id} ::\alpha ightarrow \alpha) \:sì ::Rightarrow alpha $$è anche il giudizio di tipo$$ Alpha ::\ast, y ::\alpha \vdash (\lambda x ightarrow x ::\alpha ightarrow \alpha) \:sì ::Rightarrow Alpha.$$È una notazione diversa per lo stesso oggetto matematico.