haskell - 是否有带有显式子类型的 ADT 名称？

Question

我正在为将 ADT 与显式子类型相结合的数据类型寻找合适的名称。

在我的一个应用程序中，我使用类似于 ADT 的结构来表示解析树，并在其上执行递归模式匹配。我发现如果我可以将 ADT 与子类型结合起来会很方便，如下例所示:

注意:示例是用 Haskell 的语法编写的，但这不是 Haskell 代码。

data Empty = Empty
data Expr = Int Int | Add Expr AddOp Expr
data OptionalExpr =
| Empty  // I want to make Empty a subtype of OptionalExpr
| Expr   // I want to make Expr  a subtype of OptionalExpr

在上面的例子中，我首先定义了 2 种类型:Empty 和 Expr。然后我将这两种类型设为 OptionalExpr 的子类型。我意识到这种数据类型并不常见。显然 Haskell 和 OCaml 都不支持它。但我不知道其他功能语言。

我正在寻找将 ADT 与显式子类型相结合的东西，而不是多态变体中的结构隐含子类型。这个要求有几个理由:

首先，我们想要全有或全无子类型。假设我们希望 A 是 B 的子类型，那么我们将永远不想在 B 下仅包含 A 的一些变体。要么 A 是 B 的子类型，在这种情况下 B 包括 A 的所有变体，要么 A 是不是 B 的子类型，在这种情况下，B 不包含 A 的任何变体。我们不允许介于两者之间的灰色区域。

其次，我们不希望 B 在任何意义上都是开放的。我们想到了一组非常特定的 B 子类型。我们不希望仅仅通过实现类型类或类似的东西就成为 B 的实例。

第三，假设类型 A 有大量的变体。我们想让类型 B 成为 A 的父类(super class)型。将所有变体复制到 B 中，正如多态变体所要求的那样，太麻烦且容易出错。

第四，当我们只想表达一个子类型时，我们不想引入新的值构造器。在上面的示例中，我们可以将 OptionalExpr 编写为具有 2 个值构造函数的 ADT，如下所示:data OptionalExpr = EmptyExpr | NonEmptyExpr Expr , 或者我们可以使用 Maybe ，但在我的应用程序中这是 Not Acceptable ，因为嵌入的级别可能非常深，解构像 (L1 (L2 (L3 (L4 (L5 value_wanted))))) 这样的深度嵌入值将是一场噩梦.

为了让您了解为什么存在这样的要求，我在下面展示了一个更具体的示例:

PrimaryExpr = ID | LeftParen Expr RightParen
UnaryExpr = PrimaryExpr | NegateOp PrimaryExpr    // -
MultExpr  = UnaryExpr | MultExpr MultOp UnaryExpr // *
AddExpr   = MultExpr  | AddExpr  AddOp MultExpr   // +
CompExpr  = AddExpr | AddExpr CompOp AddExpr
Expr = CompExpr

上面的例子表达了一个子类型层次结构，表达了AddExpr是一个CompExpr，但是一个CompExpr不是一个AddExpr这样的思想。对于这个具体的例子，有人向我建议，我可以只用 Expr 替换 UnaryExpr、MultExpr、AddExpr 等。也就是说，我可以将所有类型定义为单一类型。这会丢失类型约束，例如 CompExpr 不是 AddExpr，并且因为我正在对这些类型进行递归模式匹配，所以我需要静态强制执行此层次结构的约束。

我在文献中寻找的这种数据类型有名称吗？还是我在寻找一些甚至没有意义的东西？如果您认为是这种情况，我为什么要寻找 absurd 的东西？感谢您的任何指示。

编辑:即使我已经用 Haskell 的语法编写了上述代码片段，但我并没有在 Haskell 中编写我的应用程序。我使用我自己的语言和我自己的数据类型，所以我不受 Haskell 语义的限制。我正在寻找文献中类似概念的指针，因此当我为我的项目写报告时，我似乎并没有重新发明一些新东西。我尝试了所有我能想到的谷歌关键字，但没有返回任何正确的结果，所以我在这里问。

Answer 1

在评论中，你说:

I'm not sure how to encode a subtype hierarchy using GADTs. If you think it is doable, would you mind providing an answer with an example as to how the type hierarchy given in my example may be encoded?

因此，我在这里给出这个问题的答案。关键思想是提供一个类型级函数(在宿主语言中，这里是 Haskell)用于计算子类型关系(目标语言的类型系统，这里是您的自定义 EDSL)。为简单起见，我将完整地说明子类型关系，但可以使用标准类型级编程来减少重复并酌情提高抽象级别。首先，需要的扩展:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

现在子类型关系的定义:

data Level = Primary | Unary | Mult | Add | Comp

type family Subtype a b where
    Subtype Primary a       = True
    Subtype Unary   Primary = False
    Subtype Unary   a       = True
    Subtype Mult    Primary = False
    Subtype Mult    Unary   = False
    Subtype Mult    a       = True
    Subtype Add     Add     = True
    Subtype Add     Comp    = True
    Subtype Add     a       = False
    Subtype Comp    Comp    = True
    Subtype Comp    a       = False

封闭类型族用于保证子类型关系不能被客户扩展(您的第二个属性)。最后，目标语言术语的 GADT 可以使用子类型关系作为对其构造函数的约束。

data Expr a where
    ID      :: Subtype Primary a ~ True => Expr a
    Paren   :: Subtype Primary a ~ True => Expr b -> Expr a
    Negate  :: Subtype Unary   a ~ True => Expr Unary -> Expr a
    Times   :: Subtype Add     a ~ True => Expr Mult -> Expr Mult -> Expr a
    Plus    :: Subtype Add     a ~ True => Expr Add -> Expr Add -> Expr a
    Compose :: Subtype Comp    a ~ True => Expr Comp -> Expr Comp -> Expr a

请注意，因为 Paren 的参数是多态的，您将需要对包含的术语进行类型注释，以表达您希望将该术语视为子类型层次结构的哪个“级别”。我希望您也需要使用您正在设计的任何语言来执行此操作。在 ghci 中，我们可以询问样本词的类型:

:t Compose (Times ID ID) (Negate (Paren (Plus ID ID :: Expr Add)))
Compose (Times ID ID) (Negate (Paren (Plus ID ID :: Expr Add)))
  :: (Subtype 'Comp a ~ 'True) => Expr a

我认为，这或多或少是您对本学期所期望的类型。您还可以看到表达式层次结构是严格执行的，尽管我敢说错误消息不是 100% 清楚的(因为它是用宿主语言术语而不是目标语言术语编写的):

:t Negate (Plus ID ID)

<interactive>:1:9:
    Couldn't match type ‘'False’ with ‘'True’
    Expected type: 'True
      Actual type: Subtype 'Add 'Unary
    In the first argument of ‘Negate’, namely ‘(Plus ID ID)’
    In the expression: Negate (Plus ID ID)