Homogenize a heterogenous list with a funtion that has a particular kind of context-CodePudding

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?

CodePudding user response：

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]