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?Czy regularne algebraiczne typy danych w języku haskell są odpowiednikami gramatyk bez kontekstu? A co z GADTS?
Odpowiedz
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.
- 1. Co jest najbliżej Haskell GADTs i typeklasses w F #?
- 2. Algebraiczne typy danych Haskella: "pseudo-rozszerzenie"
- 3. Sprawdzanie, czy dwa masywne słowniki w języku Python są odpowiednikami
- 4. Dlaczego typy bez konstruktorów danych są poprawne?
- 5. Haskell: dane algebraiczne vs krotka
- 6. Rodzaj Pisanie algebraiczne danych w Scala
- 7. Czy współczesne dialekty regularne nie są regularne?
- 8. Czy quadprog i frontcon są odpowiednikami w Matlabie?
- 9. Co to jest gramatyka bez kontekstu?
- 10. Generowanie instrukcji n z gramatyk bezkontekstowych
- 11. Czy anonimowe typy w języku C# są dostępne poprzez odbicie?
- 12. Czy Haskell obsługuje zamknięte typy polimorficzne?
- 13. Są domyślnie typem algebry danych haskell?
- 14. Haskell użytkowania typy danych dobrych practicies
- 15. Czy typy nieskończone (inaczej typy rekursywne) nie są możliwe w języku F #?
- 16. Dlaczego niektóre napisy w języku Python są drukowane z cudzysłowami, a niektóre drukowane są bez cudzysłowów?
- 17. Haskell: Wyrażenia regularne i dane.Teksty
- 18. Typeclasses i GADTs
- 19. Co to są "rozszerzone typy całkowite"?
- 20. Wyrażenie regularne z a = i a;
- 21. Znaczenie tyldy w Haskell typy (równości Type)
- 22. Typowe odlewanie GADTs
- 23. Jak mogę zmienić swoje typy danych bez powodowania ponownej kompilacji w Haskell?
- 24. Haskell- (typ deklaracja) co to jest "a"?
- 25. Czy typy MakeGenericType/generic nie są zbierane?
- 26. Co to są różne typy certyfikatów, formaty w kryptografii
- 27. PHP PDO ODBC - Typy danych są niezgodne w równym operatora
- 28. Typy przekazywania jako argumenty funkcji w Haskell?
- 29. Sprawdź, czy dwa typy ogólne są równe
- 30. W jaki sposób są pakowane małe typy danych w C#
W twoim przykładzie CFG, '' 'A''' wyraża' '' '' ''^^^^^| m = n + 1} '' ', nie' '' m> n} '' ' – NightRa
@NightRa Rzeczywiście, dzięki. Powinien być teraz naprawiony. – chi