I have a higher order list GADT defined like so:
data HList as where
HNil :: HList '[]
HCons :: a -> HList as -> HList (a ': as)
I can write a function that gets me the first item from that list, provided it is non-empty:
first :: HList (a ': as) -> HList '[a]
first (HCons a _) = HCons a HNil
However, if I make a new type Cat
and a type family that merely applies every type in a type-level list to Cat
(kind of like a type level map):
newtype Cat a = Cat a
type family MapCat (as :: [*]) :: [*] where
MapCat '[] = '[]
MapCat (a ': as) = Cat a ': MapCat as
And a type CatList
which converts a list of types to a HList
full of those types applied to Cat
:
type CatList cs = HList (MapCat cs)
I can't write a similar function that works on CatList
.
first' :: CatList (a ': as) -> CatList '[a]
first' (HCons a _) = HCons a HNil
It errors out with:
Couldn't match type ‘MapCat as0’ with ‘MapCat as’
NB: ‘MapCat’ is a type function, and may not be injective
The type variable ‘as0’ is ambiguous
Expected type: CatList (a : as) -> CatList '[a]
Actual type: CatList (a : as0) -> CatList '[a]
In the ambiguity check for:
forall a (as :: [*]). CatList (a : as) -> CatList '[a]
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
Testing.fst :: CatList (a : as) -> CatList '[a]
What's going wrong? Here is a gist with the entire code.
Let's start with a simpler example:
throws
While this compiles fine:
And this:
Here is another example, that closer to your problem:
The error is
But this works:
and this:
since
TF_Id a
immediately reduces toa
in both cases.So the compiler throws an error every time it cannot reduce
SomeTypeFamily a
, wherea
is some type variable, that was not determined previously.So if we want to fix this:
without redefining the type family, we need to determine
d
in theerr
type signature. The simplest way isOr we can define a datatype for this:
And now back to the
first'
function:This compiles fine. You can use it like this:
which prints
Cat3:[]
.But the only thing the compiler must know to reduce
MapCat as
is a weak head normal form ofas
, so we do not actually need to provide this additional type information inProxy :: Proxy '[Int, Bool]
. Here is a better way:So
first'
now receives something, that looks like the length of a list. But can we do this statically? Not so fast:throws
Data constructor LZ comes from an un-promotable type ListWHNF …
. We cannot use indexed datatypes as indices in Haskell.Having some sort of functional dependencies, that would allow to associate a term of one type and the weak head normal form of a term of another, we could probably do the trick, but I am not aware about anything like that in GHC (but I am not an expert). In Agda this is simply
So if the only thing, we need to infer a list, is its length, then we can replace a list with
n
nested tuples. Abusing the notation,[?, ?] :: [*]
becomes(? :: *, (? :: *, Lift ⊤))
and all these?
can now be inferred automatically among with the inhabitant of⊤
(Agda's equivalent of()
). But in Agda there is no distinction between value-level and type-level programming, so there are no such problems at all.