Haskell 中的子集代数数据类型或类型级集

Question

假设您有大量类型和大量函数，每个函数都返回这些类型的“子集”。

让我们用一个小例子来使情况更加明确。这是一个简单的代数数据类型：

data T = A | B | C

并且有两个函数f，g它们返回一个T

f :: T
g :: T

对于手头的情况，假设重要的是f只能返回 a AorB并且g只能返回 a Bor C。

我想在类型系统中对此进行编码。以下是一些可能需要这样做的原因/情况：

• 让函数f并g拥有比仅仅提供更多信息的签名::T
• 强制实现f并且g不要意外返回实现的用户然后意外使用的禁止类型
• 允许代码重用，例如当涉及仅对类型子集进行操作的辅助函数时 T
• 避免样板代码（见下文）
• 使重构（更！）更容易

一种方法是拆分代数数据类型并根据需要包装各个类型：

data A = A
data B = B
data C = C

data Retf = RetfA A | RetfB B 
data Retg = RetgB B | RetgC C

f :: Retf
g :: Retg

这是有效的，并且很容易理解，但带有很多样板，用于频繁展开返回类型Retf和Retg.

我认为多态性在这里没有任何帮助。

因此，可能这是依赖类型的情况。它不是真正的类型级别列表，而是类型级别集，但我从未见过类型级别集。

最后，目标是通过类型对领域知识进行编码，以便可以进行编译时检查，而不会产生过多的样板文件。（当有很多类型和很多功能时，样板真的很烦人。）

Answer 1

我过去尝试过实现类似的目标，但没有取得太大成功——我对我的解决方案不太满意。

尽管如此，我们仍然可以使用 GADT 来编码这一约束：

data TagA = IsA | NotA
data TagC = IsC | NotC
    
data T (ta :: TagA) (tc :: TagC) where
   A :: T 'IsA  'NotC
   B :: T 'NotA 'NotC
   C :: T 'NotA 'IsC

-- existential wrappers
data TnotC where TnotC :: T ta 'NotC -> TnotC
data TnotA where TnotA :: T 'NotA tc -> TnotA

f :: TnotC
g :: TnotA

然而，由于指数的包装/展开，这很快就会变得无聊。消费者函数更方便，因为我们可以编写

giveMeNotAnA :: T 'NotA tc -> Int

要求除了A. 相反，生产者函数需要使用存在性。

在具有许多构造函数的类型中，它也会变得不方便，因为我们必须使用具有许多标签/参数的 GADT。也许这可以通过一些聪明的类型类机制来简化。