haskell - 如何用 GADT 表示变量类型的构造函数列表？

Question

我正在为我参与的研究项目实现一个小型 DSL。由于这是几乎所有对 GADT 的解释的示例，我认为现在是真正开始使用它们的好时机。显而易见的表达式(算术等)运行良好，但我的 DSL 需要支持用户定义的函数，这是我遇到问题的地方。

没有 GADT，我的表达式类型的结构看起来有点像这样(浓缩为一个最小的例子):

data Expr = IntConst Int
          | BoolConst Bool
          | Plus Expr Expr
          | Times Expr Expr -- etc
          | AndAlso Expr Expr -- etc
          | Call String [Expr] -- function call!

转换为GADT，如何表达Call规则？

data Expr a where
     IntConst :: Int -> Expr Int
     BoolConst :: Bool -> Expr Bool
     Plus :: Expr Int -> Expr Int -> Expr Int
     Times :: Expr Int -> Expr Int -> Expr Int
     AndAlso :: Expr Bool -> Expr Bool -> Expr Bool
     Call :: ???

我的第一个想法是，如果没有一些 super 花哨的依赖类型，这是不可能的，因为没有办法知道给定的用户函数将接受什么类型(也是返回类型，但我可以通过 Call return Expr a 并专门在施工现场)。我可以通过添加规则“删除”类型来强制它进行类型检查

     EraseInt :: Expr Int -> Expr a
     EraseBool :: Expr Bool -> Expr a

但似乎我首先失去了拥有 GADT 的好处。我还认为可能有一些其他的 rankN 多态性我可以在 Call 中使用(某种存在类型？)，但我想出的似乎都没有用。

帮忙吗？

Answer 1

也许你不需要为你想要的东西走依赖路线。将构建函数和调用函数分开的解决方案怎么样？这允许您在构建函数时键入函数，这样您就可以进行类型检查调用。

data Expr a where
     IntConst  :: Int -> Expr Int
     BoolConst :: Bool -> Expr Bool
     Plus      :: Expr Int -> Expr Int -> Expr Int
     Times     :: Expr Int -> Expr Int -> Expr Int
     AndAlso   :: Expr Bool -> Expr Bool -> Expr Bool
     Fun       :: String -> Expr (a->b)
     Call      :: Expr (a->b) -> Expr a -> Expr b

-- type checks
test = Call (Fun "f" :: Expr (Int -> Int)) (IntConst 1)

-- doesn't type check
test' = Call (Fun "f" :: Expr (Int -> Int)) (BoolConst False) 

对于具有多个参数的函数，您可以通过多次调用以柯里化(Currying)的方式工作，即

 Call (Call (Fun "f" :: Expr (Int->Int->Int)) (IntConst 1)) (IntConst 1) 

或者您可以用您的语言实现元组。