关于串联的一个很好的真实事实是,如果我知道方程中的任何两个变量:
a ++ b = c
然后我知道第三个。
我想在我自己的 concat 中捕捉到这个想法,所以我使用了函数依赖。
{-# Language DataKinds, GADTs, FlexibleContexts, FlexibleInstances, FunctionalDependencies, KindSignatures, PolyKinds, TypeOperators, UndecidableInstances #-}
import Data.Kind (Type)
class Concatable
(m :: k -> Type)
(as :: k)
(bs :: k)
(cs :: k)
| as bs -> cs
, as cs -> bs
, bs cs -> as
where
concat' :: m as -> m bs -> m cs
现在我想出这样的异构列表:
data HList ( as :: [ Type ] ) where
HEmpty :: HList '[]
HCons :: a -> HList as -> HList (a ': as)
但是当我尝试将这些声明为
Concatable
我有一个问题instance Concatable HList '[] bs bs where
concat' HEmpty bs = bs
instance
( Concatable HList as bs cs
)
=> Concatable HList (a ': as) bs (a ': cs)
where
concat' (HCons head tail) bs = HCons head (concat' tail bs)
我不满足我的第三个功能依赖。或者更确切地说,编译器认为我们不相信。
这是因为编译器认为在我们的第二个实例中,
bs ~ (a ': cs)
可能是这种情况。 .如果 Concatable as (a ': cs) cs
可能是这种情况.如何调整我的实例以使所有三个依赖项都得到满足?
最佳答案
所以,正如评论所暗示的,GHC 不会自己解决它,但我们可以通过一些类型级编程来帮助它。介绍一些TypeFamilies
.所有这些函数都是将列表操作提升到类型级别的非常简单的翻译:
-- | This will produce the suffix of `cs` without `as`
type family DropPrefix (as :: [Type]) (cs :: [Type]) where
DropPrefix '[] cs = cs
DropPrefix (a ': as) (a ': cs) = DropPrefix as cs
-- Similar to the logic in the question itself: list concatenation.
type family Concat (as :: [Type]) (bs :: [Type]) where
Concat '[] bs = bs
Concat (head ': tail) bs = head ': Concat tail bs
-- | Naive list reversal with help of concatenation.
type family Reverse (xs :: [Type]) where
Reverse '[] = '[]
Reverse (x ': xs) = Concat (Reverse xs) '[x]
-- | This will produce the prefix of `cs` without `bs`
type family DropSuffix (bs :: [Type]) (cs :: [Type]) where
DropSuffix bs cs = Reverse (DropPrefix (Reverse bs) (Reverse cs))
-- | Same definition of `HList` as in the question
data HList (as :: [Type]) where
HEmpty :: HList '[]
HCons :: a -> HList as -> HList (a ': as)
-- | Definition of concatenation at the value level
concatHList :: (cs ~ Concat as bs) => HList as -> HList bs -> HList cs
concatHList HEmpty bs = bs
concatHList (HCons head tail) bs = HCons head (concatHList tail bs)
使用我们可以使用的这些工具,我们实际上可以达到小时目标,但首先让我们定义一个具有所需属性的函数:
cs
来自 as
和 bs
as
来自 bs
和 cs
bs
来自 as
和 cs
瞧:
concatH ::
(cs ~ Concat as bs, bs ~ DropPrefix as cs, as ~ DropSuffix bs cs)
=> HList as
-> HList bs
-> HList cs
concatH = concatHList
让我们测试一下:
foo :: HList '[Char, Bool]
foo = HCons 'a' (HCons True HEmpty)
bar :: HList '[Int]
bar = HCons (1 :: Int) HEmpty
λ> :t concatH foo bar
concatH foo bar :: HList '[Char, Bool, Int]
λ> :t concatH bar foo
concatH bar foo :: HList '[Int, Char, Bool]
最后是最终目标:
class Concatable (m :: k -> Type) (as :: k) (bs :: k) (cs :: k)
| as bs -> cs
, as cs -> bs
, bs cs -> as
where
concat' :: m as -> m bs -> m cs
instance (cs ~ Concat as bs, bs ~ DropPrefix as cs, as ~ DropSuffix bs cs) =>
Concatable HList as bs cs where
concat' = concatH
λ> :t concat' HEmpty bar
concat' HEmpty bar :: HList '[Int]
λ> :t concat' foo bar
concat' foo bar :: HList '[Char, Bool, Int]
λ> :t concat' bar foo
concat' bar foo :: HList '[Int, Char, Bool]
关于haskell - 创建完全依赖的串联,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/59495874/