Claus Reinke:
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?)
Yes, I meant to write "data type constructor".
and 'type constructor' (don't you want to exclude
type-defined type constructors here).
It may have been clearer if I had written data type constructor, but
then the Haskell 98 report doesn't bother with that either (so I tend
to be slack about it, too).
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
But note that
ConstT x ~ ConstT x
is malformed.
and i thought 'type family' was meant to suggest type
synonym families, in contrast to 'data family'?
My nomenclature is as follows. The keywords 'type family' introduces
a "type synonym family" and 'data family' introduces a "data type
family" (or just "data family"). The term "type family" includes
both. This follows Haskell's common use of "type constructor", "type
synonym constructor", and "data type constructor".
you did notice that i gave an example of how ghc does
not seem to follow that decomposition rule, didn't you?
Yes, but I didn't see why you think GHC does the wrong thing.
Manuel
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
