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

问题描述

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

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

data T = A | B | C

有两个函数f，g返回一个T

f :: T
g :: T

对于当前情况，假设f仅可以返回A或B并且g仅可以返回B或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。

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

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

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

解决方法

定义一个辅助求和类型（用作数据类型），其中每个分支都对应于您的主要类型的版本：

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
import Data.Kind
import Data.Void
import GHC.TypeLits

data Version = AllEnabled | SomeDisabled

然后定义一个类型家族，如果允许该分支，则将版本和构造函数名称（作为类型级别Symbol）映射到类型()，并将其映射到空类型{{ 1}}（如果不允许）。

Void

然后按如下所示定义您的类型：

type Enabled :: Version -> Symbol -> Type
type family Enabled v ctor where
    Enabled SomeDisabled "C" = Void
    Enabled _ _ = ()

（严格性注释可以帮助穷举性检查器。）

可以派生Typeclass实例，但可以分别为每个版本派生：

type T :: Version -> Type
data T v = A !(Enabled v "A")
         | B !(Enabled v "B")
         | C !(Enabled v "C")

这是一个使用示例：

deriving instance Show (T AllEnabled)
deriving instance Eq (T AllEnabled)
deriving instance Show (T SomeDisabled)
deriving instance Eq (T SomeDisabled)

此解决方案使模式匹配和构造更加麻烦，因为那些noC :: T SomeDisabled noC = A () main :: IO () main = print $ case noC of A _ -> "A" B _ -> "B" -- this doesn't give a warning with -Wincomplete-patterns 总是在那儿。

一个变体是每个分支具有一个类型族（如Trees that Grow），而不是两参数类型族。

,

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

仍然，可以使用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，因此它也很不方便。也许可以使用一些聪明的typeclass机械来简化。

,

为每个值赋予其自己的类型会非常糟糕，并且不必要地进行细粒度设置。

您可能想要的只是将类型限制为 property 。例如Coq，那就是subset type：

Inductive T: Type :=
     | A
     | B
     | C.

Definition Retf: Type := { x: T | x<>C }.
Definition Retg: Type := { x: T | x<>A }.

好吧，Haskell无法表达这种价值约束，但这并不能阻止您创建从概念上实现它们的类型。只需使用新类型：

newtype Retf = Retf { getRetf :: T }
mkRetf :: T -> Maybe Retf
mkRetf C = Nothing
mkRetf x = Retf x

newtype Retg = Retg { getRetg :: T }
mkRetg :: ...

然后在f的实现中，您匹配mkRetf的最终结果，如果为Nothing，则会引发错误。这样，不幸的是，实现错误使它C不会产生编译错误，但至少会产生实际错误的函数内部的运行时错误，而不是进一步的错误。

Liquid Haskell是最适合您的选择，它确实支持子集类型。我不能说太多，但是据说它还不错（并且将在新的GHC版本中得到直接支持）。