[Haskell-cafe] Equality constraints in type families

[David Menendez]

On Mon, Mar 24, 2008 at 12:14 AM, Manuel M T Chakravarty
<chak at cse.unsw.edu.au> wrote:
>  One difference between type families and (value-level) functions is
>  that not all parameters of a type family are treated the same.  A type
>  family has a fixed number of type indicies.  We call the number of
>  type indicies the type family's arity and by convention, the type
>  indicies come always before other type parameters.  In the example
>
>    type family F a :: * -> *
>
>  F has arity 1, whereas
>
>    type family G a b :: *
>
>  has arity 2.  So, the number of named parameters given is the arity.
>  (The overall kind is still F :: * -> * -> *; ie, the arity is not
>  obvious from the kind, which I am somewhat unhappy about.)

Perhaps 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.)

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>