CODEWITHSUNDEEP
haskelltypeclassfunctor
Leander
Leander

Reputation: 1395

mapping operation for heterogenous List

I have a simple heterogenous List

data HList (ts :: [Type]) where
    HNil :: HList '[]
    (:&:) :: t -> HList ts -> HList (t ': ts)

infixr 5 :&:

and am trying to define a heterogeneous map:

type family ToDomain (xs :: [Type]) :: [Type] where
    ToDomain '[] = '[];
    ToDomain ((a -> b) ': r) = a ': ToDomain r

type family ToCoDomain (xs :: [Type]) :: [Type] where
    ToCoDomain '[] = '[];
    ToCoDomain ((a -> b) ': r) = b ': ToCoDomain r

mapH :: forall mappings input output.
    (input ~ ToDomain mappings, output ~ ToCoDomain mappings)
    => HList mappings -> HList input -> HList output
mapH HNil HNil = HNil
mapH (f :&: maps) (x :&: ins) = (f x) :&: mapH maps ins

this does not compile (i would be really surprised if this would actually work) since GHC can't infer the correctness of the recursion. I am unsure how to convince GHC of the correctness.

Upvotes: 1

Views: 69

Answers (2)

chi
chi

Reputation: 116139

You need to prove that mappings only has functions inside. This can be made with an additional GADT.

data OnlyFunctions (ts :: [*]) where
   FNil :: OnlyFunctions '[]
   FCons :: OnlyFunctions ts -> OnlyFunctions ((a->b) ': ts)

mapH :: forall mappings input output.
    (input ~ ToDomain mappings, output ~ ToCoDomain mappings)
    => OnlyFunctions mappings -> HList mappings -> HList input -> HList output
mapH FNil HNil HNil = HNil
mapH (FCons h) (f :&: maps) (x :&: ins) = (f x) :&: mapH h maps ins

The issue is that ToDomain '[Int,Bool] is a valid type -- even if ToDomain does not simplify in such case. Hence GHC can not assume that the mappings list of types is made of functions, only.

You can remove the additional argument through a custom type class, if needed.

class OF (ts :: [*]) where
   onlyFun :: OnlyFunctions ts
instance OF '[] where
   onlyFun = FNil
instance OF ts => OF ((a -> b) ': ts) where
   onlyFun = FCons onlyFun

mapHsimple :: forall mappings input output.
    (input ~ ToDomain mappings, output ~ ToCoDomain mappings, OF mappings)
    => HList mappings -> HList input -> HList output
mapHsimple = mapH onlyFun

Upvotes: 2

dfeuer
dfeuer

Reputation: 48580

If you want mapping operations, you're almost certainly better off defining

data Rec (f :: k -> *) (ts :: [k]) where
  RNil :: Rec f '[]
  (:&:) :: f t -> Rec f ts -> Rec f (t ': ts)

infixr 5 :&:

Now you can define a general

rmap :: (forall a. f a -> g a) -> Rec f ts -> Rec g ts

and

rzipWith :: (forall a. f a -> g a -> h a) -> Rec f ts -> Rec g ts -> Rec h ts

This generally makes things rather easier. In this case, you could use

data Fun :: * -> * where
  Fun :: (a -> b) -> Fun (a -> b)

data Dom :: * -> * where
  Dom :: a -> Dom (a -> b)

data Cod :: * -> * where
  Cod :: b -> Cod (a -> b)

Now you can write

zoop :: Rec Fun fs -> Rec Dom fs -> Rec Cod fs
zoop = rzipWith (\(Fun f) (Dom x) -> Cod (f x))

In fact, some of this is slight overkill; you should be able to get away with a newtype wrapping a type family for Dom. You could even do so for Cod, but that might make the result less usable.

Upvotes: 2

Related Questions