Являются ли регулярные алгебраические типы данных haskell эквивалентными контекстно-свободным грамматикам? Как насчет GADTS?

Question

Синтаксис для типов алгебраических данных очень похож на синтаксис Backus–Naur Form, который используется для описания контекстно-свободных грамматик. Это заставило меня задуматься, если мы подумаем о контролере типа Haskell как синтаксическом анализаторе для языка, представленном как тип алгебраических данных (например, конструкторы типа nularry, представляющие символы терминала), - это набор всех языков, принятых так же, как и набор контекстных свободных языков? Кроме того, с этой интерпретацией, какой набор формальных языков может принимать GADT?

Answer 1

Прежде всего, типы данных не всегда описывают набор строк (т. Е. Язык). То есть, в то время как тип списка делает, тип дерева нет. Можно было бы возразить, что мы могли бы «сгладить» деревья в списках и подумать об этом как о своем языке. Тем не менее, чем о типах данных, как

data F = F Int (Int -> Int) 

или, что еще хуже

data R = R (R -> Int) 

?

Полиномиальные типы (типы без -> внутри) грубо описывают деревья, которые могут быть сплющены (в порядке их посещения), поэтому давайте использовать их в качестве примера.

Как вы заметили, написав CFG как тип (полиномиальное) легко, так как вы можете использовать рекурсию

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

выше A выражает { Int^m Char^n | m>n }.

GADTs выходит далеко за пределы контекстно-свободных языков.

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 

выше ABC выражает (сплющенный) язык A^n B^n C^n, который не является контекстно-свободным.

Вы практически не ограничены GADT, так как с ними легко кодировать арифметику. То есть вы можете построить тип Plus a b c, который не пуст, если c=a+b с Peano naturals. Вы также можете построить тип Halt n m, который не пуст, если машина Тьюринга m останавливается на входе m. Итак, вы можете построить язык

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

, который является рекурсивным (и не более простым классом, примерно).

В настоящий момент я не знаю, можете ли вы описать рекурсивно перечислимые (вычислительно перечислимые) языки в GADT. Даже в примере проблемы остановки я должен включить термин «доказательство» внутри GADT, чтобы он работал.

Наглядно, если у вас есть строка длиной n и вы хотите, чтобы проверить его в отношении GADT, вы можете построить все GADT условия глубины n, расправьте их, а затем сравните строки. Это должно доказать, что такой язык всегда рекурсивный. Однако экзистенциальные типы делают это построение дерева довольно сложным, поэтому у меня нет определенного ответа прямо сейчас.