创建完全依赖的串联

Question

关于连接的一个很好的真实事实是，如果我知道等式中的任意两个变量：

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.

可能就是这种情况

如何调整我的实例以满足所有三个依赖项？

Answer 1

因此，正如评论所暗示的那样，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)

使用这些工具，我们实际上可以达到小时目标，但首先让我们定义一个具有所需属性的函数：

能够从 as 和 bs

cs

能够从 bs 和 cs

as

能够从 as 和 cs

bs

瞧：

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]

创建完全依赖的串联

Creating a completely dependent concatenation

haskell

typeclass

functional-dependencies

type-level-computation