ban*_*anx 6 haskell gadt dependent-type data-kinds
为什么使用datakinds构建值更难,而与它们进行模式匹配相对容易？
{-# 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代码？
如果你稍微考虑一下,你会发现你的类型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类型是值电平当量的Nat种类,以便为每种类型的种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类型(反身性)是一种常用的模式进行类型检查统一两名身份不明的类型,当我们模式匹配的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