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

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

Ответы

Ответ 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, который не пуст, если if c=a+b с Peano натуралы. Вы также можете создать тип Halt n m, который не пуст, если машина Тьюринга m останавливается на входе m. Итак, вы можете создать язык

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

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

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

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