Esistono firme di tipi che Haskell non è in grado di verificare?

Question

This paper stabilisce che l'inferenza di tipo (detta "tipabilità" nella carta) nel sistema F è indecidibile. Quello che non ho mai sentito nominare altrove è il secondo risultato del documento, ovvero che "il controllo del tipo" in F è anche indecidibile. Qui la domanda "verifica tipo" significa: dato un termine t, tipo T e ambiente di scrittura A, è il giudizio A ⊢ t : T derivabile? Che questa domanda sia indecidibile (e che sia equivalente alla questione della tipabilità) è sorprendente per me, perché sembra intuitivamente come dovrebbe essere una domanda più facile a cui rispondere.

Ma in ogni caso, visto che Haskell è basato sul sistema F (o F-omega, anche), il risultato sul tipo di controllo sembrerebbe suggerire che ci sia un termine Haskell t e digitare T in modo tale che il compilatore essere in grado di decidere se t :: T è valido. Se è così, sono curioso di sapere che tipo di termine e tipo sono ... se non è il caso, che cosa sto fraintendendo?

Presumibilmente comprendere la carta porterebbe ad una risposta costruttiva, ma io sono un po 'fuori dalla mia profondità :)

Answer 1

Ecco un esempio di implementazione di livello tipo di calcolo SKI a Scala: http://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/

L'ultimo esempio mostra una iterazione illimitata. Se fai lo stesso in Haskell (e sono abbastanza sicuro che puoi farlo), hai un esempio di "espressione non classificabile".

Answer 2

Il controllo del tipo può essere reso decidibile arricchendo opportunamente la sintassi. Ad esempio, nel documento, abbiamo lambda scritto come \x -> e; per digitare-verificare, è necessario indovinare il tipo di x. Tuttavia, con una sintassi opportunamente arricchita, questo può essere scritto come \x :: t -> e invece, che risolve il problema. Allo stesso modo, nel documento, consentono ai lambda di livello testo di essere impliciti; ovvero, se e :: t, quindi anche e :: forall a. t. Per eseguire il controllo ortografico, devi indovinare quando e quanti forall aggiungere e quando eliminarli. Come in precedenza, si può fare questo più deterministico con l'aggiunta di sintassi: aggiungiamo due nuovi espressione forma /\a. e e e [t] e due nuova regola di battitura che dice che se e :: t, poi /\a. e :: forall a. t, e se e :: forall a. t, quindi e [t'] :: t [t'/a] (dove le parentesi in t [t'/a] sono parentesi di sostituzione). Quindi la sintassi ci dice quando e quante forche aggiungere e quando eliminarle.

Quindi la domanda è: possiamo passare da Haskell a termini di sistema F sufficientemente annotati? E la risposta è sì, grazie ad alcune restrizioni critiche poste dal sistema di tipo Haskell. Il più critico è che tutti i tipi sono di prima scelta *. Senza entrare troppo nel dettaglio, "rank" è relativo al numero di volte che devi andare a sinistra di un costruttore -> per trovare uno forall.

Int -> Bool -- rank 0? 
forall a. (a -> a) -- rank 1 
(forall a. a -> a) -> (forall a. a -> a) -- rank 2 

In particolare, questo limita il polimorfismo un po '. Non possiamo digitare qualcosa di simile con i tipi di rango uno:

foo :: (forall a. a -> a) -> (String, Bool) -- a rank-2 type 
foo polymorphicId = (polymorphicId "hey", polymorphicId True) 

La prossima restrizione più critico è che le variabili di tipo possono essere sostituite solo da tipi monomorfa. (Questo include altre variabili di tipo, come a, ma non tipi polimorfi come forall a. a.) Ciò garantisce in parte che la sostituzione di tipo conserva la rank-one-ness.

Si scopre che se si effettuano queste due restrizioni, quindi non solo è decidibile il tipo-inferenza, ma si ottiene anche minimo tipi.

Se passiamo da Haskell a GHC, possiamo parlare non solo di cosa è tipabile, ma di come appare l'algoritmo di inferenza. In particolare, in GHC, ci sono estensioni che rilassano le due precedenti restrizioni; in che modo GHC fa l'inferenza in quell'impostazione? Bene, la risposta è che semplicemente non ci prova nemmeno. Se vuoi scrivere termini usando queste caratteristiche, devi aggiungere le annotazioni di battitura di cui abbiamo parlato fino al paragrafo 1: devi annotare esplicitamente dove forall s viene introdotto ed eliminato. Quindi, possiamo scrivere un termine che rifiuta il type-checker di GHC? Sì, è semplice: usa semplicemente tipi o impraticabilità di secondo grado non annotati (o superiori). Ad esempio, il seguente non digitare-controllo, anche se ha un tipo di annotazione esplicita ed è tipizzabile con rango di due tipi:

{-# LANGUAGE Rank2Types #-} 
foo :: (String, Bool) 
foo = (\f -> (f "hey", f True)) id 

* In realtà, limitando di rango due è sufficiente a rendere decidibile, ma l'algoritmo per i tipi di rango uno può essere più efficiente. Classificare tre tipi già fornisce al programmatore una corda sufficiente a rendere il problema di inferenza indecidibile. Non sono sicuro che questi fatti fossero noti al momento in cui il comitato ha scelto di limitare Haskell ai tipi di grado 1.