[Haskell-cafe] Equality constraints in type families
claus.reinke at talk21.com
Mon Mar 24 07:45:06 EDT 2008
>>>> type family F a :: * -> *
>>> F x y ~ F u v <=> F x ~ F u /\ y ~ v
> words, in a type term like (F Int Bool), the two parameters Int and
> Bool are treated differently. Int is treated like a parameter to a
> function (which is what you where expecting), whereas Bool is treated
> like a parameter to a vanilla data constructor (the part you did not
> expect). To highlight this distinction, we call only Int a type
> index. Generally, if a type family F has arity n, it's first n
> parameters are type indicies, the rest are treated like the parameters
> of any other type constructor.
i'm not sure haskell offers the kind of distinction that we
need to talk about this: 'data constructor' is value-level,
'type constructor' doesn't distinguish between type- vs
data-defined type constructors. i think i know what you
mean, but it confuses me that you use 'data constructor'
(should be data/newtype-defined type constructor?)
and 'type constructor' (don't you want to exclude
type-defined type constructors here).
data ConstD x y = ConstD x
type ConstT x y = x
'ConstD x' and 'ConstT x' have the same kind, that
of type constructors: * -> *. but:
ConstD x y1 ~ ConstD x y2 => y1 ~ y2
forall y1, y2: ConstT x y1 ~ ConstT x y2
and i thought 'type family' was meant to suggest type
synonym families, in contrast to 'data family'?
you did notice that i gave an example of how ghc does
not seem to follow that decomposition rule, didn't you?
ghc seems to behave almost as i would expect, not as
the decomposition rule seems to suggest.
More information about the Haskell-Cafe