Tworzenie całkowicie zależnej konkatenacji

Dobrym prawdziwym faktem na temat konkatenacji jest to, że jeśli znam dowolne dwie zmienne w równaniu:

a ++ b = c

Więc znam trzeci.

Chciałbym uchwycić ten pomysł w swoim własnym konkat, więc używam zależności funkcjonalnej.

{-# 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

Teraz wyczaruję listę heterogeniczną w ten sposób:

data HList ( as :: [ Type ] ) where
  HEmpty :: HList '[]
  HCons  :: a -> HList as -> HList (a ': as)

Ale kiedy próbuję zadeklarować je jako Concatableproblem

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)

Nie spełniam mojej trzeciej zależności funkcjonalnej. A raczej kompilator uważa, że ​​nie. Jest tak, ponieważ kompilator uważa, że ​​w naszym drugim przypadku może tak być bs ~ (a ': cs). I może tak być, jeśli Concatable as (a ': cs) cs.

Jak mogę dostosować moje wystąpienia, aby wszystkie trzy zależności były spełnione?

Tak więc, jak sugerują komentarze, GHC nie rozwiąże tego samodzielnie, ale możemy pomóc przy odrobinie programowania na poziomie czcionki. Przedstawmy trochę TypeFamilies. Wszystkie te funkcje są dość prostymi tłumaczeniami manipulacji listami podniesionymi do poziomu typu:

-- | 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)

Dzięki tym narzędziom, które mamy do dyspozycji, możemy faktycznie osiągnąć cel godzinowy, ale najpierw zdefiniujmy funkcję o pożądanych właściwościach:

• Możliwość wnioskowania na cspodstawie asibs
• Możliwość wnioskowania na aspodstawie bsics
• Możliwość wnioskowania na bspodstawie asics

Voila:

concatH ::
     (cs ~ Concat as bs, bs ~ DropPrefix as cs, as ~ DropSuffix bs cs)
  => HList as
  -> HList bs
  -> HList cs
concatH = concatHList

Przetestujmy to:

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]

I wreszcie cel końcowy:

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]