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
whereas
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.
still confused,
claus
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
