0

我有以下

data Expr = Condition v
          | And Expr Expr
          | Or Expr Expr

并且我被要求考虑以下无类型版本才能完成：

data Expr e where

我不确定我应该为构造函数写什么。我尝试了以下方法：

data Expr e where
  Condition :: v -> Expr v
  And :: -- really not sure what to do with this one
  OR :: Expr b -> (Expr b -> Expr a) -> Maybe Expr a -> Expr b

此外，由于v可以是任何类型，即int等bool，是否可以将其称为以下（上）并声明v稍后的类型？

data v = IntVat int

任何帮助将非常感激 ：）

编辑：更改了整个帖子以添加更多信息和清晰度（基于我对练习的理解）。

基本上，我需要帮助找出data Expr = Condition v...etc作为参考的 GADT 的构造函数。

4

2 回答 2

3

如果我使用基本表达式语言作为激励示例在 GADT 上设置作业，那么我会想到这样的答案：

data Expr v where
    Literal :: v -> Expr v
    And     :: Expr Bool -> Expr Bool -> Expr Bool
    Or      :: Expr Bool -> Expr Bool -> Expr Bool
    -- and I'd probably add some things like this to
    -- show why the type variable is useful
    Equal   :: Expr Int -> Expr Int -> Expr Bool
    If      :: Expr Bool -> Expr v -> Expr v -> Expr v

你可以看到为什么你可以称它为“类型化”表达式：类型变量的实例化看起来像是一种小语言的类型化规则：

a : Bool         b : Bool
-------------------------
    And a b : Bool

a : Int          b : Int
------------------------
    Equal a b : Bool

等等

于 2012-04-26T17:27:03.540 回答
0

对我来说，这听起来像是一种存在主义。我必须承认，我从来没有真正使用过它们，我只是试图理解它们；无论如何，也许它的意思是这样的：

data Expr = forall v. Condition v
          | And Expr Expr
          | Or Expr Expr

然后你有一个像这样的 GADT（他们概括存在主义，见这里）：

data Expr where
    Condition :: v -> Expr
    And :: Expr -> Expr -> Expr
    Or :: Expr -> Expr -> Expr

虽然，这不会（据我理解这个概念）有多大意义，因为你不能v用于任何事情。

另一方面，这会（我希望）更有意义（因为有一个“条件”）：

class Testable v where
    test :: v -> Bool

data Expr where
    Condition :: Testable v => v -> Expr
    And :: Expr -> Expr -> Expr
    Or :: Expr -> Expr -> Expr

那么你可以做，例如

eval :: Expr -> Bool
eval (Condition v) = test v
eval (And e1 e2) = (eval e1) && (eval e2)
eval (Or e1 e2) = (eval e1) || (eval e2)

这将适用于不同类型的“条件”。

不过，我没有测试这段代码，而且，正如我所说，我并不是真正的存在主义专业人士。我希望我的代码是正确的，但请告诉我任何人，如果你知道得更好（或者我完全错了......）

于 2012-04-26T09:33:12.957 回答