常规的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 }.

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限制,因为用它们编码算术很容易.那就是你可以用Peano自然物建立一个Plus a b c非空的iff 类型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,展平它们,然后与字符串进行比较.这应该证明这种语言总是递归的.但是,存在类型使得这种树构建方法相当棘手,所以我现在还没有明确的答案.