创建完全依赖的并置

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，可能会是这种情况。

如何调整我的实例，以便满足所有三个依赖关系？

关于串联的一个不错的真实事实是，如果我知道方程式中的任何两个变量：a ++ b = c那么我知道第三个变量。我想在我自己的concat中捕捉到这个想法，所以我使用了功能性的...

Answer 1

因此，正如评论所建议的那样，GHC不会自己解决它，但是我们可以通过一些类型级别的编程来帮助它。让我们介绍一些TypeFamilies。所有这些功能都是将列表操作提升到类型级别的非常简单的转换：