Czy regularne algebraiczne typy danych w języku haskell są odpowiednikami gramatyk bez kontekstu? A co z GADTS?

Question

Składnia algebraicznych typów danych jest bardzo podobna do składni Backus–Naur Form, która jest używana do opisu gramatyk bezkontekstowych. To mnie zastanowiło, jeśli pomyślimy o sprawdzaniu typu Haskella jako parserze dla języka, przedstawionym jako algebraiczny typ danych (na przykład konstruktory nularry reprezentujące symbole terminali), to zestaw wszystkich języków akceptowany tak samo jak zestaw języków bez kontekstu? Ponadto, z taką interpretacją, jaki zestaw języków formalnych akceptują GADT?

Answer 1

Po pierwsze, typy danych nie zawsze opisują zestaw łańcuchów (tj. Język). Oznacza to, że podczas gdy typ listy ma, typ drzewa nie. Można przeciwstawić się, że możemy "spłaszczyć" drzewa na listy i uważać je za ich język. Jednak co z typów danych, takich jak

data F = F Int (Int -> Int) 

lub, co gorsza

data R = R (R -> Int) 

?

Typy wielomianowe (typy bez -> wewnątrz) z grubsza opisują drzewa, które można spłaszczyć (odwiedzane w kolejności), więc użyjmy ich jako przykładu.

Jak zaobserwowaliśmy, pisząc CFG jako (wielomian) typu jest łatwe, ponieważ można wykorzystać rekurencji

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

powyżej A wyraża { Int^m Char^n | m>n }.

GADT wykraczają daleko poza języki wolne od kontekstu.

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 

powyżej ABC wyraża (spłaszczone) język A^n B^n C^n, która nie jest wolna od kontekstu.

Nie masz ograniczeń w GADT, ponieważ łatwo z nimi kodować arytmetyczne. To można zbudować typ Plus a b c, który nie jest pusty iff c=a+b z naturals Peano . Można również zbudować typ Halt n m, który nie jest pusty w przypadku zatrzymania na wejściu m. Można więc zbudować język, który jest rekurencyjny (a nie w prostszej klasie).

W tej chwili nie wiem, czy można opisywać rekursywnie przeliczalne (przeliczalne na komputer) języki w GADT. Nawet w przypadku problemu z zatrzymaniem problemu muszę wprowadzić w GADT termin "dowód", aby działało.

Intuicyjnie, jeśli ciąg długości n i chcesz sprawdzić się przed GADT można budować wszystkie warunki GADT głębokości n, spłaszczyć je, a następnie porównać do łańcucha. To powinno być udowodnić, że taki język jest zawsze rekurencyjny. Jednak typy egzystencjalne sprawiają, że budowanie tego drzewa jest dość skomplikowane, więc nie mam teraz definitywnej odpowiedzi.