Claus Reinke wrote,
given that type families are never meant to be partially applied,
perhaps a different notation, avoiding confusion
with type constructor applications in favour of something
resembling products, could make that clearer?
something simple, like braces to group families and indices:
type family {F a} :: * -> *
{F x} y ~ {F u} v <=> {F x} ~ {F u} && y ~ v
would avoid confusion about which parameters need
to be present (no partial application possible) and are
subject to family instance rules, and which parameters are subject
to the decomposition rule.
and David Menendez wrote,
erhaps type families could use a different kind constructor to
distinguish type indexes from type parameters.
Currently, Haskell kinds are generated by this grammar:
kind ::= "*" | kind "->" kind
We create a new production for "family kinds",
fkind ::= kind | kind "-|>" fkind
Now, we can easily distinguish F and G,
F :: * -|> * -> *
G :: * -|> * -|> *
The grammar allows higher-kinded indexes, like (* -> *) -|> *, but
requires all indexes to precede the regular parameters. (That is, you
can't abstract over a family.)
Yes, this is something that we thought about, too. In the System FC
paper, we subscript all type families with their arity to achieve a
weak form of this; ie, we'd write
F_1 Int Bool
to make clear that (F_1 Int) is a non-decomposable family application,
where the outermost application in ((F_1 Int) Bool) is decomposable.
The extra syntax has its advantages (more local information) and
disadvantages (more clutter). We weren't convinced that we need the
extra syntax, so left it out for the moment. However, this is
something that can always be changed if experience shows that programs
are easier to understand with extra syntax. It doesn't affect the
type theory and is really a pure language design question. I'd be
glad to hear some more opinions about this matter.
Manuel
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
