6

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

{-# 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代码？

4

2 回答 2

6

如果您考虑一下，您会发现您的类型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函数采用任何nuand的链，nd并试图证明它符合特定的pnuand 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并且我正在使用<$>from 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

SNattype 是 kind 的 value level 等价物，因此Nat对于每种类型的 kindNat都只有一个 type 值，SNat这意味着即使删除了 type 的类型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类型（自反性）是一种常用的模式，当我们在构造函数上进行模式匹配时，类型检查器可以统一两种未知类型（Refl并PolyKinds允许它对任何类型都是通用的，让我们将其与Nats 一起使用）。因此，虽然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
于 2014-05-04T08:16:35.720 回答
4

问题不在于数据类型。在类型

listToChain :: forall (t::Nat) (t1::Nat) b. [(b, Direction)] -> Chain t t1 b

您是说对于任何类型t t1 b，您都可以将一对b和 Directions 的列表转换为Chain t t1 b... 但您的函数并非如此，例如：

listToChain _ = Nil

这个结果对任何类型都不起作用，但只有在t, t1两者都是Zero. 这就是 GADT 的重点，它限制了可能的类型。

我怀疑你想要给你的函数的类型是依赖的，比如

listToChain :: (x :: [(b,Direction)]) -> Chain (number_of_ups x) (number_of_downs x) b

但这在 Haskell 中无效，因为 Haskell 没有依赖类型。一种解决方案是使用存在主义

listToChain :: forall b. [(b, Direction)] -> exists (t :: Nat) (t1 :: Nat). Chain t t1 b

这几乎是有效的 Haskell。不幸的是，existentials 需要包装在构造函数中

data AChain b where
   AChain :: Chain t t1 b -> AChain b

然后你可以这样做：

listToChain :: forall b. [(b, Direction)] -> AChain b
listToChain ((x, Center): xs) = case (listToChain xs) of
   AChain y -> AChain (Add x y) 
...
于 2014-05-04T02:40:21.097 回答