I am fiddling with the basics of type-level programming in Haskell, and I was trying to write a function that "homogenizes" a heterogeneous list using a function with a context of kind (* -> *) -> Constraint (e.g., length or fmap (/= x)).
The heterogeneous list is defined as follows:
data HList ls where
HNil :: HList '[]
(:::) :: a -> HList as -> HList (a ': as)
And I have defined a type family AllKind2:
type family AllKind2 c t li :: Constraint where
AllKind2 _ _ '[] = ()
AllKind2 c t ((t _) : xs)) = (c t, AllKind2 c t xs)
The type family works as intended (as far as I can tell with my limited knowledge) as demonstrated with this function that simply returns unit if supplied with a heterogeneous list that can satisfy AllKind2:
unitIfAllIsWell :: forall c t li. AllKind2 c t li => Proxy c -> Proxy t -> HList li -> ()
unitIfAllIsWell _ _ _ = ()
>>> unitIfAllIsWell (Proxy :: Proxy Foldable) (Proxy :: Proxy []) ([] ::: "ok" ::: [1,2] ::: HNil)
()
>>> unitIfAllIsWell (Proxy :: Proxy Foldable) (Proxy :: Proxy []) ("is_list" ::: 10 ::: HNil)
<interactive>:414:1: error:
• Could not deduce: AllKind2 Foldable [] '[Integer]
arising from a use of ‘unitIfAllIsWell’
However, the homogenize function I've written fails at the typecheck:
homogenize
:: forall c t li q. AllKind2 c t li
=> Proxy c
-> Proxy t
-> (forall p q. c t => t p -> q)
-> HList li
-> [q]
homogenize _ _ _ HNil = []
homogenize _ _ f (x ::: xs) = f x : homogenize (Proxy :: Proxy c) (Proxy :: Proxy t) f xs
• Could not deduce: a ~ t p0
from the context: AllKind2 c t li
bound by the type signature for:
homogenize :: forall (c :: (* -> *) -> Constraint)
(t :: * -> *) (li :: [*]) q.
AllKind2 c t li =>
Proxy c
-> Proxy t
-> (forall p q1. c t => t p -> q1)
-> HList li
-> [q]
at HList.hs:(134,1)-(140,8)
or from: li ~ (a : as)
bound by a pattern with constructor:
::: :: forall a (as :: [*]). a -> HList as -> HList (a : as),
in an equation for ‘homogenize’
at HList.hs:142:24-31
‘a’ is a rigid type variable bound by
a pattern with constructor:
::: :: forall a (as :: [*]). a -> HList as -> HList (a : as),
in an equation for ‘homogenize’
at HList.hs:142:24-31
Is the constraint AllKind2 not sufficient to tell the compiler that any element from the HList li will satisfy constraint c t and thus, applying the supplied function f should be valid at the type level?
Am I missing something here? Is what I am attempting even possible?
Even though e.g. AllKind2 Foldable [] '[Int] does not match any equation for AllKind2, it is not understood to be an unsatisifiable constraint. (The general principle is undefined type family applications are just that: undefined, in the sense it could be something but you have no idea what it is.) That's why, even if you know AllKind2 c t (x : xs), you can not deduce x ~ t y for some y by saying "that's the only way to get a defined constraint from AllKind2." You need an equation for the general AllKind2 c t (x : xs) case that dispatches to a class that will contain the actual information.
-- if you know some types satisfy a typeclass, you know they satisfy the superclasses
-- this lets us store and extract the information that x needs to be of form t _
class (c t, x ~ t (UnwrapAllKind2 t x)) => AllKind2Aux c t x where
type UnwrapAllKind2 t x
instance c t => AllKind2Aux c t (t y) where
type UnwrapAllKind2 t (t y) = y
type family AllKind2 c t xs :: Constraint where
AllKind2 c t '[] = ()
AllKind2 c t (x : xs) = (AllKind2Aux c t x, AllKind2 c t xs)
Then your homogenize passes without modification.
Do note that homogenize is overcomplicated. The c is simply not doing anything: homogenize is taking the c t instance as input and just forwarding it to the function being mapped. That function can just use its own c t instance, since t is fixed. There's nothing homogenize can do that the following function cannot do more clearly (note that your homogenize fails even to "restrict" the mapped function to only using c t and not any other properties of t, so it can muddle much more than it can clarify):
class x ~ t (UnApp t x) => IsApp t x where
type UnApp t x
instance IsApp t (t y) where
type UnApp t (t y) = y
type family AllApp t xs :: Constraint where
AllApp t '[] = ()
AllApp t (x : xs) = (IsApp t x, AllApp t xs)
homogenize' :: AllApp t xs => Proxy t -> (forall x. t x -> r) -> HList xs -> [r] -- also, the Proxy t is not strictly necessary
homogenize' t f HNil = []
homogenize' t f (x ::: xs) = f x : homogenize' t f xs -- note that dealing with Proxys is much nicer if you treat them as things that can be named and passed around instead of rebuilding them every time
-- homogenize' (Proxy :: Proxy []) length ([] ::: "ok" ::: [1,2] ::: HNil) = [0, 2, 2]