普通的haskell代数数据类型是否等同于上下文无关文法？那GADTS呢？

Question

代数数据类型的语法非常类似于Backus–Naur Form的语法，后者用于描述上下文无关的语法。这让我想到，如果我们认为Haskell类型检查器是一种语言的解析器，表示为一种代数数据类型(例如，表示终端符号的空值类型构造器)，那么所有语言的集合是否与上下文无关语言集相同？此外，有了这种解释，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 }。

GADT远远超出了上下文无关的语言。

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与皮亚诺自然。您还可以构建一个类型的Halt n m，它是非空的，如果图灵机m在输入m上停止。所以，您可以构建一种语言

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

它是递归的(粗略地说，不是在任何简单的类中)。

目前，我不知道您是否可以在GADT中描述递归可枚举(可计算枚举)语言。即使在停止问题的例子中，我也必须在GADT中包含“证明”这个术语才能使它工作。

直观地说，如果您有一个长度为n的字符串，并且希望将其与GADT进行检查，您可以构建所有的GADT深度n项，将它们压平，然后与该字符串进行比较。这应该证明这种语言总是递归的。然而，存在主义类型使得这种树的构建方法相当棘手，所以我现在还没有明确的答案。