常规的Haskell代数数据类型是否等同于上下文无关文法？广义代数数据类型呢？

Question

代数数据类型的语法与Backus–Naur Form的语法非常相似，后者用于描述无上下文语法。这让我想到，如果我们把Haskell类型检查器看作是一个语言的解析器，表示为一个代数数据类型（例如表示终端符号的nularry类型构造函数），那么被接受的所有语言集合是否与上下文无关的语言集合相同？此外，使用这种解释，GADTs可以接受哪些形式化语言集合？

- Nathan BeDell

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表示的是(flattened)语言A^n B^n C^n，它不是上下文无关的。

使用GADTs，你基本上没有限制，因为很容易用它们编码算术运算。 也就是说，你可以构建一个类型Plus a b c，当且仅当Peano自然数中c=a+b时它是非空的。你还可以构建一个类型Halt n m，当且仅当图灵机m 在输入n时停机它是非空的。所以，你可以构建一种语言

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

目前，我不知道您是否能够在GADTs中描述递归可枚举（可计算可枚举）语言。即使在停机问题的例子中，我也必须在GADT中包含“ proof”项才能使其正常工作。

直觉上，如果您有一个长度为n的字符串并且想要针对GADT进行检查，您可以构建所有深度为n的GADT项，将它们展开，然后与字符串进行比较。这应该证明这种语言总是递归的。但是，存在类型使得这种树形建模方法非常棘手，因此我现在没有明确的答案。

- chi

---

在你的CFG示例中，A表示的是{Int^m Char^n| m = n + 1}，而不是{Int^m Char^n| m > n}。 - NightRa