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:
- 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:
- How do I understand the problem GHC has with these approaches?
- How do I go about making a function that would address my need?
CodePudding user response:
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