Search code examples
haskelltype-level-computation

How to use constraints that apply to each type in a heterogenous collection?

I'm trying to figure out heterogenous collections, and there's some kind of a type-checking problem I can't wrap my head around.

data HTypeMap (f :: * -> *) (types :: [*]) where
  HNil :: HTypeMap f '[]
  HCons :: f e -> HTypeMap f types -> HTypeMap f (e ': types)

(It's basically supposed to be a map from types to values of that type, under some functor f). E.g.:

testMap :: HTypeMap Prelude.Maybe '[Prelude.Int, Prelude.String]
testMap = HCons (Prelude.Just 3) (HCons (Prelude.Just "Hello") HNil)

I've been trying to formulate a function that would allow me to run a map in case I know that all of the types in my collection are constrained, to be used like:

showEverything :: AllConstrained Show types => HTypeMap f types -> [String]
showEverything = mapConstrained show


type family AllConstrained (c :: u -> Constraint) (ts :: [u]) :: Constraint where
  AllConstrained c '[] = ()
  AllConstrained c (t ': ts) = (c t, AllConstrained c ts)

My attempts so far:

  1. Just a simple function... GHC won't let me write this type:
mapConstrained :: AllConstrained c types => (forall t. c t => f t -> a) -> HTypeMap f types -> [a]
mapConstrained = _

It says:

• Could not deduce: AllConstrained c0 types
  from the context: AllConstrained c types

I don't understand this at all... I have only one constraint to be considered there, it's c. (I have ScopedTypeVariables on.)

Same goes for a typeclass in the same style... There's some kind of ambiguity here that I don't notice...

2.

This unwieldy one actually works:

data ContraintRunnerF f c r = ContraintRunnerF {runMeF :: forall x. c x => f x -> r}

class MapConstrained c types where
  mapConstrained :: forall a f r. AllConstrained c types => ContraintRunnerF f c r -> HTypeMap f types -> [r]

instance MapConstrained c '[] where
  mapConstrained _ HNil = []

instance MapConstrained c types => MapConstrained c (t ': types) where
  mapConstrained g (HCons e rest) = (runMeF g e) : mapConstrained @c g rest

used like:


showRunnerF :: ContraintRunnerF Prelude.Identity Prelude.Show Prelude.String
showRunnerF = ContraintRunnerF Prelude.show

showRunnerFM :: ContraintRunnerF Prelude.Maybe Prelude.Show Prelude.String
showRunnerFM = ContraintRunnerF Prelude.show

testMap :: HTypeMap Prelude.Maybe '[Prelude.Int, Prelude.String]
testMap = HCons (Prelude.Just 3) (HCons (Prelude.Just "Hello") HNil)

test1 :: [Prelude.String]
test1 = mapConstrained showRunnerFM testMap

but unfortunately even a simple substitution would not typecheck, basically requiring me to specify all the types:

test2 :: [Prelude.String]
test2 = mapConstrained (ContraintRunnerF Prelude.show) testMap

• Could not deduce: (c0 Prelude.Int, c0 [Prelude.Char])
    arising from a use of ‘mapConstrained’

So, questions:

  1. How do I understand the problem GHC has with these approaches?
  2. How do I go about making a function that would address my need?
Solution

  • The type variable c is called ambiguous in the type of mapConstrained because there is never any way to determine what that type variable should be from it's arguments.

    The solution to this is TypeApplications, which allows you to explicitly specify a type for an ambiguous type variable.

    {-# LANGUAGE AllowAmbiguousTypes, TypeApplications, PolyKinds #-}

import Data.Kind

data HTypeMap (f :: * -> *) (types :: [*]) where
  HNil :: HTypeMap f '[]
  HCons :: f e -> HTypeMap f types -> HTypeMap f (e ': types)

type family AllConstrained (c :: u -> Constraint) (ts :: [u]) :: Constraint where
  AllConstrained c '[] = ()
  AllConstrained c (t ': ts) = (c t, AllConstrained c ts)

mapConstrained :: AllConstrained c types => (forall t. c t => f t -> a) -> HTypeMap f types -> [a]
mapConstrained _ _  = undefined

testMap :: HTypeMap Prelude.Maybe '[Prelude.Int, Prelude.String]
testMap = HCons (Prelude.Just 3) (HCons (Prelude.Just "Hello") HNil)

-- Note here that `@Show' is the type application - it applies `mapConstrained' at the type level
test = mapConstrained @Show show testMap

    You once again must specify the type variable explicitly in the second case:

    test2 :: [Prelude.String]
test2 = mapConstrained (ContraintRunnerF @_ @Show Prelude.show) testMap