I normali tipi di dati algebrici haskell equivalgono a grammatiche senza contesto? Che dire di GADTS?

Question

La sintassi per i tipi di dati algebrici è molto simile alla sintassi di Backus–Naur Form, che viene utilizzata per descrivere grammatiche senza contesto. Questo mi ha fatto pensare, se pensiamo al correttore di tipo Haskell come un parser per un linguaggio, rappresentato come un tipo di dati algebrico (costruttori di tipi di nularry che rappresentano i simboli del terminale, per esempio), l'insieme di tutte le lingue accettate è lo stesso del set di lingue libere dal contesto? Inoltre, con questa interpretazione, quale gruppo di linguaggi formali può accettare i GADT?

Answer 1

Prima di tutto, i tipi di dati non sempre descrivono un insieme di stringhe (cioè una lingua). Cioè, mentre un tipo di lista fa, un tipo di albero no. Si potrebbe ribattere che potremmo "appiattire" gli alberi in liste e pensarci come loro lingua. Eppure, per quanto riguarda i tipi di dati come

data F = F Int (Int -> Int) 

o, peggio

data R = R (R -> Int) 

?

I tipi polinomiali (tipi senza -> all'interno) descrivono approssimativamente gli alberi, che possono essere appiattiti (visitati in ordine), quindi utilizziamoli come esempio.

Come avete osservato, scrivendo una CFG come un tipo (polinomiale) è facile, dato che è possibile sfruttare la ricorsione

data A = A1 Int A | A2 Int B 
data B = B1 Int B Char | B2 

sopra A esprime { Int^m Char^n | m>n }.

GADT vanno ben oltre i linguaggi context-free.

data Z 
data S n 

data ListN a n where 
    L1 :: ListN a Z 
    L2 :: a -> ListN a n -> ListN a (S n) 

data A 
data B 
data C 

data ABC where 
    ABC :: ListN A n -> ListN B n -> ListN C n -> ABC 

sopra ABC esprime la (appiattito) lingua A^n B^n C^n, che non è context-free.

Sei praticamente senza restrizioni con GADT, dal momento che è facile codificare con loro aritmetica. Questo è possibile creare un tipo Plus a b c che non è vuoto iff c=a+b con Peano naturals. È inoltre possibile creare un tipo Halt n m che non è vuoto se la macchina Turing m si arresta sull'ingresso m. Quindi, puoi creare una lingua

{ A^n B^m proof | n halts on m , and proof proves it } 

che è ricorsivo (e non in una classe più semplice, approssimativamente).

Al momento, non so se è possibile descrivere in modo ricorsivamente enumerabile (computabilmente enumerabile) le lingue in GADT. Anche nell'esempio di blocco del problema, devo includere il termine "prova" all'interno di GADT per farlo funzionare.

Intuitivamente, se si dispone di una stringa di lunghezza n e si desidera controllare una contro una GADT, è possibile costruire tutti i termini GADT di profondità n, appiattirli, e quindi confrontare alla stringa. Questo dovrebbe dimostrare che tale linguaggio è sempre ricorsivo. Tuttavia, i tipi esistenti rendono questo approccio alla costruzione degli alberi piuttosto complicato, quindi non ho una risposta definitiva al momento.