Come digitare controllare le definizioni ricorsive usando Algoritmo W?

Question

Io sono l'attuazione Algorithm W (la Hindley-Milner type system) in JavaScript:

La funzione che implementa le regole di cui sopra è typecheck ed ha la seguente firma:

typecheck :: (Context, Expr) -> Monotype 

Si è definito come segue :

function typecheck(context, expression) { 
    switch (expression.type) { 
    case "Var": 
     var name = expression.name; 
     var type = context[name]; 
     return inst(type); 
    case "App": 
     var fun = typecheck(context, expression.fun); 
     var dom = typecheck(context, expression.arg); 
     var cod = new Variable; 
     unify(fun, abs(dom, cod)); 
     return cod; 
    case "Abs": 
     var param = expression.param; 
     var env = Object.create(context); 
     var dom = env[param] = new Variable; 
     var cod = typecheck(env, expression.result); 
     return abs(dom, cod); 
    case "Let": 
     var assignments = expression.assignments; 
     var env = Object.create(context); 

     for (var name in assignments) { 
      var value = assignments[name]; 
      var type = typecheck(context, value); 
      env[name] = gen(context, type); 
     } 

     return typecheck(env, expression.result); 
    } 
} 

A li Informazioni sui tipi di dati:

1. Un contesto è un oggetto che associa gli identificatori ai politipi.

   type Context = Map String Polytype 
   

2. Un'espressione è definito dalla seguente tipo di dati algebrico:

   data Expr = Var { name  :: String       } 
         | App { fun   :: Expr,   arg :: Expr } 
         | Abs { param  :: String,   result :: Expr } 
         | Let { assignments :: Map String Expr, result :: Expr } 
         | Rec { assignments :: Map String Expr, result :: Expr } 
   

Inoltre, abbiamo le seguenti funzioni necessarie per l'algoritmo, ma non sono essenziali alla domanda :

inst :: Polytype -> Monotype 
abs :: (Monotype, Monotype) -> Monotype 
gen :: (Context, Monotype) -> Polytype 

La funzione inst specializzato un una polytype d la funzione gen generalizza un monotipo.

Ad ogni modo, voglio estendere la mia funzione typecheck per consentire recursive definitions così:

Dove:

1. 
2. 

Tuttavia, sono bloccato con un problema di uova e galline. Il contesto numero uno ha le ipotesi v_1 : τ_1, ..., v_n : τ_n. Inoltre, implica e_1 : τ_1, ..., e_n : τ_n. Quindi, per prima cosa è necessario creare il contesto per trovare i tipi di e_1, ..., e_n ma per creare il contesto è necessario trovare i tipi di e_1, ..., e_n.

Come si risolve questo problema? Stavo pensando di assegnare nuove variabili monotipo agli identificatori v_1, ..., v_n e quindi unificare ogni variabile monotipo con il suo rispettivo tipo. Questo è il metodo che OCaml utilizza per i suoi binding let rec. Tuttavia, questo metodo non produce il tipo più generale, come dimostra il seguente codice OCaml:

$ ocaml 
     OCaml version 4.02.1 

# let rec foo x = foo (bar true)  
    and bar x = x;; 
val foo : bool -> 'a = <fun> 
val bar : bool -> bool = <fun> 

Tuttavia, GHC non calcola il tipo più generale:

$ ghci 
GHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help 
Prelude> let foo x = foo (bar True); bar x = x 
Prelude> :t foo 
foo :: Bool -> t 
Prelude> :t bar 
bar :: t -> t 

Come si può vedere, OCaml deduce il tipo val bar : bool -> bool mentre GHC deduce il tipo bar :: t -> t.In che modo Haskell deduce il tipo più generale della funzione bar?

Capisco dalla risposta di @augustss che l'inferenza di tipo per le funzioni polimorfe ricorsive è indecidibile. Ad esempio, Haskell non può dedurre il tipo di funzione seguente size senza annotazioni di tipo supplementari:

data Nested a = Epsilon | Cons a (Nested [a]) 

size Epsilon  = 0 
size (Cons _ xs) = 1 + size xs 

Se specifichiamo il tipo di firma size :: Nested a -> Int quindi Haskell accetta il programma.

Tuttavia, se permettiamo solo un sottoinsieme di tipi di dati algebrici, inductivetypes, quindi la definizione dei dati Nested non è più valido perché non è induttivo; e se non mi sbaglio, la deduzione di tipo delle funzioni polimorfiche induttive è davvero decidibile. In tal caso, qual è l'algoritmo utilizzato per dedurre il tipo di funzioni induttive polimorfiche?

Answer 1

È possibile digitare verificarlo utilizzando la ricorsione esplicita con una primitiva fix avente tipo (a -> a) -> a. Puoi inserire la correzione a mano o automaticamente.

Se si desidera estendere il tipo di inferenze, anche questo è abbastanza semplice. Quando si incontra una funzione ricorsiva f, basta generare una nuova variabile di unificazione e inserire f con questo tipo nell'ambiente. Dopo aver controllato il corpo, unificare il tipo di corpo con questa variabile e quindi generalizzare come al solito. Penso che questo sia quello che suggerisci. Non ti permetterà di dedurre la ricorsione polimorfica, ma questo in generale è indecidibile.