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