[Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

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