常规的haskell代数数据类型等同于上下文无关语法？ GADTS怎么样？

首先,数据类型并不总是描述一组字符串(即语言).也就是说,虽然列表类型是,树类型不.有人可能反驳说,我们可以把树木变成列表,把它们当作他们的语言.然而,数据类型如何

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,这不是上下文的.

您几乎不受GADTs限制,因为它们可以很容易地编码算术.

那就是你可以建立一个类型加一个b c,它是非空的,如果c = a与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,展平它们,然后与字符串进行比较.这应该

证明这种语言总是递归的.然而,存在类型使这个树构建

方法很棘手,所以我现在没有确定的答案.