haskell - 使用数据种类使用 GADT 动态构建值

Question

为什么用数据类型构建值更难，而与它们进行模式匹配相对容易？

{-# LANGUAGE  KindSignatures
            , GADTs
            , DataKinds
            , Rank2Types
 #-}

data Nat = Zero | Succ Nat

data Direction = Center | Up | Down | UpDown deriving (Show, Eq)

data Chain :: Nat -> Nat -> * -> * where
    Nil    :: Chain Zero Zero a
    AddUp  :: a -> Chain nUp nDn a -> Chain (Succ nUp) nDn a
    AddDn  :: a -> Chain nUp nDn a -> Chain nUp (Succ nDn) a
    AddUD  :: a -> Chain nUp nDn a -> Chain (Succ nUp) (Succ nDn) a
    Add    :: a -> Chain nUp nDn a -> Chain nUp nDn a

lengthChain :: Num b => Chain (Succ Zero) (Succ Zero) a -> b
lengthChain = lengthChain'

lengthChain' :: forall (t::Nat) (t1::Nat) a b. Num b => Chain t t1 a -> b
lengthChain' Nil = 0
lengthChain' (Add   _ rest) = 1 + lengthChain' rest
lengthChain' (AddUp _ rest) = 1 + lengthChain' rest
lengthChain' (AddDn _ rest) = 1 + lengthChain' rest
lengthChain' (AddUD _ rest) = 1 + lengthChain' rest

chainToList :: Chain (Succ Zero) (Succ Zero) a -> [(a, Direction)]
chainToList = chainToList'

chainToList' :: forall (t::Nat) (t1::Nat) a. Chain t t1 a -> [(a, Direction)]
chainToList' Nil = []
chainToList' (Add a rest) = (a, Center):chainToList' rest
chainToList' (AddUp a rest) = (a, Up):chainToList' rest
chainToList' (AddDn a rest) = (a, Down):chainToList' rest
chainToList' (AddUD a rest) = (a, UpDown):chainToList' rest

listToChain :: forall (t::Nat) (t1::Nat) b. [(b, Direction)] -> Chain t t1 b
listToChain ((x, Center): xs) = Add x (listToChain xs)
listToChain ((x, Up):xs) = AddUp x (listToChain xs)
listToChain ((x, Down): xs) = AddDn x (listToChain xs)
listToChain ((x, UpDown): xs) = AddUD x (listToChain xs)
listToChain _ = Nil

我正在尝试构建一种数据类型来控制类似于列表的结构，不同之处在于我们可能会向元素添加箭头。此外，我要求某些函数仅在向上箭头和向下箭头的数量正好等于 1 的列表上运行。

在上面的代码中，函数listToChain编译失败，同时 chainToList正常编译。我们如何修复 listToChain代码？

Answer 1

如果你稍微思考一下，你会发现你的 listToChain 的类型是不可能的。可以工作，因为它接受 (b, Direction) 的值没有方向的类型级别信息，它仍然应该以某种方式找出结果 Chain 的方向索引类型在编译时。这显然是不可能的，因为在运行时这些值可以由用户输入或从套接字等读取。

您需要跳过中间列表并直接从编译时验证的值构建您的链，或者您可以将结果链包装在存在类型中并执行运行时检查以将存在类型具体化为更精确的类型。

所以，给定一个存在的包装器，比如

data SomeChain a where
    SomeChain :: Chain nu nd a -> SomeChain a

您可以实现 listToChain作为

listToChain :: [(b, Direction)] -> SomeChain b
listToChain ((x, Center): xs) = withSome (SomeChain . Add x)   (listToChain xs)
listToChain ((x, Up):xs)      = withSome (SomeChain . AddUp x) (listToChain xs)
listToChain ((x, Down): xs)   = withSome (SomeChain . AddDn x) (listToChain xs)
listToChain ((x, UpDown): xs) = withSome (SomeChain . AddUD x) (listToChain xs)
listToChain _                 = SomeChain Nil

使用辅助函数 withSome为了更方便地包装和展开存在。

withSome :: (forall nu nd. Chain nu nd b -> r) -> SomeChain b -> r
withSome f (SomeChain c) = f c

现在我们有一个可以传递的存在，它隐藏了精确的上下类型。当我们想调用像 lengthChain 这样的函数时期望我们需要在运行时验证内容的特定向上和向下计数。一种方法是定义一个类型类。

class ChainProof pnu pnd where
    proveChain :: Chain nu nd b -> Maybe (Chain pnu pnd b)

proveChain函数采用任何 nu 的链和 nd并试图证明它符合特定的pnu和 pnd .实现 ChainProof需要一些重复的样板文件，但除了我们需要的一对一案例 lengthChain 之外，它可以为任何所需的起伏组合提供证据。 .

instance ChainProof Zero Zero where
    proveChain Nil          = Just Nil
    proveChain (Add a rest) = Add a <$> proveChain rest
    proveChain _            = Nothing

instance ChainProof u Zero => ChainProof (Succ u) Zero where
    proveChain (Add a rest)   = Add a   <$> proveChain rest
    proveChain (AddUp a rest) = AddUp a <$> proveChain rest
    proveChain _              = Nothing

instance ChainProof Zero d => ChainProof Zero (Succ d) where
    proveChain (Add a rest)   = Add a   <$> proveChain rest
    proveChain (AddDn a rest) = AddDn a <$> proveChain rest
    proveChain _              = Nothing

instance (ChainProof u (Succ d), ChainProof (Succ u) d, ChainProof u d) => ChainProof (Succ u) (Succ d) where
    proveChain (Add a rest)   = Add a   <$> proveChain rest
    proveChain (AddUp a rest) = AddUp a <$> proveChain rest
    proveChain (AddDn a rest) = AddDn a <$> proveChain rest
    proveChain (AddUD a rest) = AddUD a <$> proveChain rest
    proveChain _              = Nothing

以上需要语言扩展MultiParamTypeClasses和 FlexibleContexts我正在使用 <$>来自 Control.Applicative .

现在我们可以使用证明机制为任何需要特定向上和向下计数的函数创建一个安全的包装器

safe :: ChainProof nu nd => (Chain nu nd b -> r) -> SomeChain b -> Maybe r
safe f = withSome (fmap f . proveChain)

这似乎是一个不令人满意的解决方案，因为我们仍然需要处理失败情况(即 Nothing )，但至少只需要在顶层进行检查。在给定的 f 内我们对链的结构有静态保证，不需要做任何额外的验证。

替代解决方案

上述方案虽然实现简单，但每次验证时都必须遍历并重新构建整个链。另一种选择是将向上和向下计数作为单例自然数存储在存在对象中。

data SNat :: Nat -> * where
    SZero :: SNat Zero
    SSucc :: SNat n -> SNat (Succ n)

data SomeChain a where
    SomeChain :: SNat nu -> SNat nd -> Chain nu nd a -> SomeChain a

SNat type 是等效于 Nat 的值级别kind 这样对于每种类型的种类 Nat类型为 SNat 的值只有一个这意味着即使类型 t的 SNat t被删除，我们可以通过对值进行模式匹配来完全恢复它。通过扩展，这意味着我们可以恢复 Chain 的完整类型。在存在主义中，只需对自然物进行模式匹配，而不必遍历链条本身。

构建链变得更加冗长

listToChain :: [(b, Direction)] -> SomeChain b
listToChain ((x, Center): xs) = case listToChain xs of
    SomeChain u d c -> SomeChain u d (Add x c)
listToChain ((x, Up):xs)      = case listToChain xs of
    SomeChain u d c -> SomeChain (SSucc u) d (AddUp x c)
listToChain ((x, Down): xs)   = case listToChain xs of
    SomeChain u d c -> SomeChain u (SSucc d) (AddDn x c)
listToChain ((x, UpDown): xs) = case listToChain xs of
    SomeChain u d c -> SomeChain (SSucc u) (SSucc d) (AddUD x c)
listToChain _                 = SomeChain SZero SZero Nil

但另一方面，证明变得更短(尽管有些毛茸茸的类型签名)。

proveChain :: forall pnu pnd b. (ProveNat pnu, ProveNat pnd) => SomeChain b -> Maybe (Chain pnu pnd b)
proveChain (SomeChain (u :: SNat u) (d :: SNat d) c)
    = case (proveNat u :: Maybe (Refl u pnu), proveNat d :: Maybe (Refl d pnd)) of
        (Just Refl, Just Refl) -> Just c
        _ -> Nothing

这使用 ScopedTypeVariables为 ProveNat 显式选择类型类实例我们想使用。如果我们得到自然数匹配请求值的证据，那么类型检查器很乐意让我们返回 Just c无需进一步检查。
ProveNat被定义为

{-# LANGUAGE PolyKinds #-}

data Refl a b where
    Refl :: Refl a a

class ProveNat n where
    proveNat :: SNat m -> Maybe (Refl m n)

Refl type (reflexivity) 是一种常用的模式，当我们在 Refl 上进行模式匹配时，它可以使类型检查器统一两种未知类型。构造函数(和 PolyKinds 允许它对任何类型通用，让我们将它与 Nat 一起使用)。所以虽然proveNat接受 forall m. SNat m如果我们可以在 Just Refl 上进行模式匹配之后，我们(更重要的是类型检查器)可以确定 m和 n实际上是同一种类型。
ProveNat 的实例非常简单，但同样需要一些显式类型来帮助推理。

instance ProveNat Zero where
    proveNat SZero = Just Refl
    proveNat _ = Nothing

instance ProveNat n => ProveNat (Succ n) where
    proveNat m@(SSucc _) = proveNat' m where
        proveNat' :: forall p. ProveNat n => SNat (Succ p) -> Maybe (Refl (Succ p) (Succ n))
        proveNat' (SSucc p) = case proveNat p :: Maybe (Refl p n) of
            Just Refl -> Just Refl
            _         -> Nothing
    proveNat _ = Nothing