CODEWITHSUNDEEP
haskelltype-level-computationhlist
purefn
purefn

Reputation: 836

Can HListElim be composed with another function?

Given 

{-# LANGUAGE TypeFamilies, KindSignatures #-}
{-# LANGUAGE GADTs, DataKinds, TypeOperators #-}

import Data.HList
import Data.Singletons
import Data.Singletons.Prelude.List

type family HListElim (ts :: [*]) (a :: *) :: * where
    HListElim '[] a = a
    HListElim (t ': ts) a = t -> HListElim ts a

hListUncurry :: HListElim ts a -> HList ts -> a
hListUncurry f HNil = f
hListUncurry f (HCons x xs) = hListUncurry (f x) xs

hListCurryExpl :: Sing ts -> (HList ts -> a) -> HListElim ts a
hListCurryExpl SNil f = f HNil
hListCurryExpl (SCons _ r) f = \x -> hListCurryExpl r (f . HCons x)

hListCurry :: SingI ts => (HList ts -> a) -> HListElim ts a
hListCurry = hListCurryExpl sing

(adapted from https://gist.github.com/timjb/516f04808f0c4aa90c26 and reroute)

I'd like to be able to write a function like the following

hListCompose :: (a -> b) -> HListElim as a -> HListElim as b

My first attempt was 

hListCompose f g = hListCurry (fmap f (hListUncurry g))

But GHC is telling me that 

Could not deduce (HListElim ts0 b ~ HListElim ts b)
from the context (HasRep ts)
  bound by the inferred type for ‘hListCompose’:
             HasRep ts => (a -> b) -> HListElim ts a -> HListElim ts b
  at src/Webcrank/Wai/T.hs:64:1-55
NB: ‘HListElim’ is a type function, and may not be injective
The type variable ‘ts0’ is ambiguous
Expected type: (a -> b) -> HListElim ts a -> HListElim ts b
  Actual type: (a -> b) -> HListElim ts0 a -> HListElim ts0 b
When checking that ‘hListCompose’
  has the inferred type ‘forall (ts :: [*]) a b.
                         SingI ts =>
                         (a -> b) -> HListElim ts a -> HListElim ts b’
Probable cause: the inferred type is ambiguous

Is this even possible?

Upvotes: 3

Views: 86

Answers (1)

Cactus
Cactus

Reputation: 27636

GHC is right in this case: the basic problem is that because type families need not be injective, HListElim as a doesn't specify what the as are. (To see why, consider that HListElim '[] (a -> b) ~ HListElim '[a] b).

You can get around this if you are willing to add an extra Singleton argument to hListCompose to give the HList explicitly:

{-# LANGUAGE ScopedTypeVariables #-}
hListCompose :: forall a b as. Sing as -> (a -> b) -> HListElim as a -> HListElim as b
hListCompose s f = go s
  where
    go :: forall ts. Sing ts -> HListElim ts a -> HListElim ts b
    go SNil = f
    go (SCons _ ts) = \g x -> go ts (g x)

Upvotes: 2

Related Questions