Creating a completely dependent concatenation

Question

A nice true fact about concatenation is that if I know any two variables in the equation:

a ++ b = c

Then I know the third.

I would like to capture this idea in my own concat so I use a functional dependency.

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

Now I conjure heterogeneous list like so:

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

But when I try to declare these as Concatable I have an issue

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)

I don't satisfy my third functional dependency. Or rather the compiler believes we do not. This is because the compiler believes that in our second instance it might be the case that bs ~ (a ': cs). And it could be the case if Concatable as (a ': cs) cs.

How can I adjust my instances so that all three of the dependencies are satisfied?

Serrulation

The key trouble seems to be bs cs -> as, because we need non-local information about bs and cs to decide if as should be a cons or a nil. We need to find out how to represent this information; what context would we add to a type signature to guarantee it when it can't be directly deduced? – Orthoptic

To expand what luqui said: imagine we know bs and cs, and we want to exploit the fundep, i.e. we want to reconstruct as. To do it in a deterministic way, we expect to be able to commit to a single instance and follow that recipe. Concretely, assume bs = (Int ': bs2) and cs = (Int ': cs2). Which instance do we choose? It is possible that such Int in cs comes from bs (and as is empty). It is also possible that is comes from (nonempty) as instead, and that Int will appear again in cs later on. We need to dig deeper in cs to know and GHC won't do that. – Streetcar

Very roughly put, GHC will accept fundeps that can be proved using a simple form of induction from the instances. Here, one of them requires a kind of double induction to be proved (or so it seems), and the compiler won't go that far. – Streetcar

Answer 1

So, as comments suggest, GHC is not gonna figure it out on it's own, but we can help it with a bit of type level programming. Let's introduce some TypeFamilies. All of these functions are pretty straightforward translations of list manipulation lifted to the type level:

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

With this tools at our disposal we can actually get to hour goal, but first let's define a function with the desired properties:

• Ability to deduce cs from as and bs
• Ability to deduce as from bs and cs
• Ability to deduce bs from as and cs

Voila:

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

Let's test it:

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]

And finally the end goal:

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]

Korey

Well done! I even suspected this might be impossible but you solved it transparently and elegantly. – Orthoptic