Sequence over heterogeneous list in Haskell

Question

Consider following definition of a HList:

infixr 5 :>
data HList (types :: [*]) where
  HNil :: HList '[]
  (:>) :: a -> HList l -> HList (a:l)

And a type family Map to map over typelevel lists:

type family Map (f :: * -> *) (xs :: [*]) where
    Map f '[] = '[]
    Map f (x ': xs) = (f x) ': xs

Now I would like to define sequence equivalence for HLists. My attempt looks like

hSequence :: Applicative m => HList (Map m ins) -> m (HList ins)
hSequence HNil = pure HNil
hSequence (x :> rest) = (:>) <$> x <*> hSequence rest

But I get errors like this:

Could not deduce: ins ~ '[]
       from the context: Map m ins ~ '[]
         bound by a pattern with constructor: HNil :: HList '[]

For me it looks like the compiler isn't sure that if Map m returns [] on some list then the list is empty. Sadly, I don't see any way to convince it to that fact. What should I do in this situation?

---

I am using GHC 8.6.5 with following extensions:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

Answer 1

HList is quite an unwieldy type. I recommend using something like this one instead, which is similar to one from vinyl.

{-# language PolyKinds, DataKinds, GADTs, ScopedTypeVariables, RankNTypes, TypeOperators #-}
import Data.Kind
import Control.Applicative

infixr 4 :>

-- Type is the modern spelling of the * kind
data Rec :: [k] -> (k -> Type) -> Type 
where
  Nil :: Rec '[] f
  (:>) :: f a -> Rec as f -> Rec (a ': as) f

htraverse
  :: forall (xs :: [k]) (f :: k -> Type) (g :: k -> Type) m.
     Applicative m
  => (forall t. f t -> m (g t))
  -> Rec xs f -> m (Rec xs g)
htraverse _f Nil = pure Nil
htraverse f (x :> xs) =
  liftA2 (:>) (f x) (htraverse f xs)

If you like, you can define

hsequence
  :: forall (xs :: [k]) (g :: k -> Type) m.
     Applicative m
  => Rec xs (Compose m g) -> m (Rec xs g)
hsequence = htraverse getCompose

Note that

HList xs ~= Rec xs Identity

Answer 2

This GADT preserves the spine ("length") of type level lists past type erasure:

data Spine (xs :: [k]) :: Type where
  NilSpine :: Spine '[]
  ConsSpine :: Spine xs -> Spine (x : xs)

From this, we can prove these lemmas:

mapNil' :: forall f xs. Map f xs ~ '[] => Spine xs -> xs :~: '[]
mapNil' NilSpine = Refl

type family Head (xs :: [k]) :: k where Head (x : _) = x
type family Tail (xs :: [k]) :: [k] where Tail (_ : xs) = xs
data MapCons f y ys xs =
  forall x xs'. (xs ~ (x : xs'), y ~ f x, ys ~ Map f xs') => MapCons
mapCons' :: forall f xs y ys. Map f xs ~ (y : ys) => Spine xs -> MapCons f y ys xs
mapCons' (ConsSpine _) = MapCons

Now, Spine is a singleton family: Spine xs has exactly one value for each xs. We can therefore erase it.

mapNil :: forall f xs. Map f xs ~ '[] => xs :~: '[]
mapNil = unsafeCoerce Refl -- safe because mapNil' exists
mapCons :: forall f xs y ys. Map f xs ~ (y : ys) => MapCons f y ys xs
mapCons = unsafeCoerce MapCons -- safe because mapCons' exists

These lemmas can then be used to define your function:

hSequence :: forall m ins. Applicative m => HList (Map m ins) -> m (HList ins)
hSequence HNil | Refl <- mapNil @m @ins = pure HNil
hSequence (x :> rest) | MapCons <- mapCons @m @ins = (:>) <$> x <*> hSequence rest

By starting with Spine, we can build a justification for why our logic works. Then, we can erase all the singleton junk we don't need at runtime. This is an extension of how we use types to build a justification for why our programs work, and then we erase them for the runtime. It's important to write mapNil' and mapCons' so we know what we're doing works.

Answer 3

First, there's an error here:

type family Map (f :: * -> *) (xs :: [*]) where
    Map f '[] = '[]
    Map f (x ': xs) = (f x) ': Map f xs
                             --^^^^^-- we need this

After that is fixed, the issue here is that we need to proceed by induction on ins, not on Map f ins. To achieve that, we need a singleton type:

data SList :: [*] -> * where
    SNil  :: SList '[] 
    SCons :: SList zs -> SList ( z ': zs )

and then an additional argument:

hSequence :: Applicative m => SList ins -> HList (Map m ins) -> m (HList ins)
hSequence SNil         HNil        = pure HNil
hSequence (SCons ins') (x :> rest) = (:>) <$> x <*> hSequence ins' rest

This now compiles. Matching on SNil / SCons refines ins to either '[] or z ': zs, so Map m ins can be unfolded one step as well. This allows us to make the recursive call.

As usual, we can remove the additional singleton argument through a suitable typeclass. I'm reasonably sure that some of this can be automated exploiting the singletons library.

class SingList ins where
    singList :: SList ins

instance SingList '[] where
    singList = SNil

instance SingList zs => SingList (z ': zs) where
    singList = SCons singList

hSequence2 :: (Applicative m, SingList ins)
              => HList (Map m ins) -> m (HList ins)
hSequence2 = hSequence singList