相关疑难解决方法(0)

我正在寻找将 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

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

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

• 首先，我们想要全有或全无的子类型。假设我们希望 A 是 B 的子类型，那么我们将永远不想只在 B 下包含 A …

在以下程序中填补空缺是否一定需要非建设性的手段？如果可以，是否x :~: y可以决定？

更一般而言，如何使用引用来指导类型检查器？

（我知道我可以通过定义Choose为GADT 来解决此问题，我专门针对类型系列）

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module PropositionalDisequality where

import Data.Type.Equality
import Data.Void

type family Choose x y where
  Choose x x = 1
  Choose x _ = 2

lem :: (x :~: y -> Void) -> Choose x y :~: 2
lem refutation = _