Tipo di controllo e tipi ricorsivi (Scrivere il combinatore Y in Haskell / Ocaml)

Question

Tipo di controllo e tipi ricorsivi (Scrivere il combinatore Y in Haskell / Ocaml)

#1 da (16 voti)
#2 da (2 voti)

21

Quando si spiega il combinatore Y nel contesto di Haskell, di solito si nota che l'implementazione diretta non effettuerà il check-in di tipo Haskell a causa del suo tipo ricorsivo.

Ad esempio, da Rosettacode :

The obvious definition of the Y combinator in Haskell canot be used
because it contains an infinite recursive type (a = a -> b). Defining
a data type (Mu) allows this recursion to be broken.

newtype Mu a = Roll { unroll :: Mu a -> a }

fix :: (a -> a) -> a
fix = \f -> (\x -> f (unroll x x)) $ Roll (\x -> f (unroll x x))

E infatti, la definizione "ovvia" non digita check:

λ> let fix f g = (\x -> \a -> f (x x) a) (\x -> \a -> f (x x) a) g

<interactive>:10:33:
    Occurs check: cannot construct the infinite type:
      t2 = t2 -> t0 -> t1
    Expected type: t2 -> t0 -> t1
      Actual type: (t2 -> t0 -> t1) -> t0 -> t1
    In the first argument of 'x', namely 'x'
    In the first argument of 'f', namely '(x x)'
    In the expression: f (x x) a

<interactive>:10:57:
    Occurs check: cannot construct the infinite type:
      t2 = t2 -> t0 -> t1
    In the first argument of 'x', namely 'x'
    In the first argument of 'f', namely '(x x)'
    In the expression: f (x x) a
(0.01 secs, 1033328 bytes)

La stessa limitazione esiste in Ocaml:

utop # let fix f g = (fun x a -> f (x x) a) (fun x a -> f (x x) a) g;;
Error: This expression has type 'a -> 'b but an expression was expected of type 'a                                    
       The type variable 'a occurs inside 'a -> 'b

Tuttavia, in Ocaml, è possibile consentire i tipi ricorsivi passando l'interruttore -rectypes :

   -rectypes
          Allow  arbitrary  recursive  types  during type-checking.  By default, only recursive
          types where the recursion goes through an object type are supported.

Usando -rectypes , tutto funziona:

utop # let fix f g = (fun x a -> f (x x) a) (fun x a -> f (x x) a) g;;
val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
utop # let fact_improver partial n = if n = 0 then 1 else n*partial (n-1);;
val fact_improver : (int -> int) -> int -> int = <fun>
utop # (fix fact_improver) 5;;
- : int = 120

Essendo incuriosito da sistemi di tipo e inferenza di tipo, questo solleva alcune domande a cui non sono ancora in grado di rispondere.

Innanzitutto, come viene visualizzato il tipo di controllo con il tipo t2 = t2 -> t0 -> t1 ? Avendo inventato quel tipo, immagino che il problema sia che il tipo ( t2 ) si riferisce a se stesso sul lato destro?
Secondo, e forse più interessante, qual è la ragione per Haskell / Ocaml digitare i sistemi per non consentire questo? Immagino che sia una buona ragione poiché Ocaml non lo consentirà anche di default anche se può trattare con tipi ricorsivi se viene fornito l'interruttore -rectypes .

Se questi sono argomenti davvero importanti, apprezzerei i riferimenti alla letteratura pertinente.

type-systems haskell static-typing ocaml

posta beta 27.10.2013 - 21:43

fonte

2 risposte

2

In OCaml, devi passare -rectypes come parametro al compilatore (o inserire #rectypes;; nel toplevel). In parole povere, questo si disattiverà "verifica verifica" durante l'unificazione. La situazione The type variable 'a occurs inside 'a -> 'b non sarà più un problema. Il sistema dei tipi sarà ancora "corretto" (suono, ecc.), Gli alberi infiniti che si presentano come tipi sono talvolta chiamati "alberi razionali". Il sistema di tipi si indebolisce, cioè diventa impossibile rilevare alcuni errori del programmatore.

Vedi la mia lezione sul lambda-calcolo ( a partire dalla diapositiva 27) per ulteriori informazioni sugli operatori del fixpoint con esempi in OCaml.

risposta data 29.10.2013 - 14:50

fonte

Leggi altre domande sui tag type-systems haskell static-typing ocaml

Quando è stato inventato il controllo del codice sorgente? Confusione sulla doppia licenza (MIT / GPL) javascript per l'uso sul mio sito web

score 16 · Accepted Answer

Innanzitutto, l'errore GHC,

GHC sta tentando di unificare alcuni vincoli con x , in primo luogo, lo usiamo come una funzione quindi

x :: a -> b

Quindi lo usiamo come valore per quella funzione

x :: a

E finalmente lo unifichiamo con l'espressione dell'argomento originale

x :: (a -> b) -> c -> d

Ora x x diventa un tentativo di unificare t2 -> t1 -> t0 , tuttavia, non possiamo unificare questo dato che richiederebbe unificare t2 , il primo argomento di x , con x . Da qui il nostro messaggio di errore.

Quindi, perché non i tipi ricorsivi generali. Bene, il primo punto che vale la pena notare è la differenza tra i tipi equi e iso ricorsivi,

equi-ricorsivo è quello che ti aspetteresti che mu X . Type sia esattamente equivalente all'espandersi o piegarlo arbitrariamente.
i tipi iso-ricorsivi forniscono una coppia di operatori, fold e unfold che piegano e spiegano le definizioni ricorsive dei tipi.

Ora i tipi equi-ricorsivi sembrano ideali, ma sono assurdamente difficili da ottenere nei sistemi di tipi complessi. Può effettivamente rendere il controllo dei tipi indecidibile. Non ho familiarità con tutti i dettagli del sistema di tipi di OCaml, ma i tipi completamente equirecursivi in Haskell possono far sì che il typechecker esegua il loop arbitrariamente cercando di unificare i tipi, per impostazione predefinita, Haskell si assicura che il controllo dei tipi termini. Inoltre, in Haskell, i sinonimi di tipo sono stupidi, i tipi ricorsivi più utili sarebbero definiti come type T = T -> () , tuttavia sono quasi immediatamente in linea in Haskell, ma non puoi inline un tipo ricorsivo, è infinito! Pertanto, i tipi ricorsivi in Haskell richiederebbero un'enorme revisione del modo in cui i sinonimi vengono gestiti, probabilmente non vale la pena di fare lo stesso come estensione di un linguaggio.

I tipi Iso-ricorsivi sono un po 'difficili da usare, più o meno devi dire esplicitamente al correttore di tipi come piegare e spiegare i tuoi tipi, rendendo i tuoi programmi più complessi da leggere e scrivere.

Tuttavia, questo è molto simile a quello che stai facendo con il tuo tipo Mu . Roll è fold, e unroll è unfold. Quindi, in realtà, abbiamo i tipi iso-ricorsivi integrati. Tuttavia, i tipi equi-ricorsivi sono troppo complessi, quindi i sistemi come OCaml e Haskell ti costringono a passare le ricorrenze attraverso i fixpoint di livello del tipo.

Ora, se ti interessa, ti consiglio Tipi e linguaggi di programmazione. La mia copia è aperta nelle mie ginocchia mentre scrivo questo per assicurarmi di avere la terminologia giusta:)