ConstraintKinds and default associated empty constraints

[Edward Kmett]

On Fri, Dec 23, 2011 at 10:17 AM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

>  Right now it seems it is either * or Constraint depending on context. ***
> *
>
> ** **
>
> Correct.  Tuple bracket are used for both types and Constraints, and we
> have to decide which from context.  ****
>
> **
>

Whew, that agrees with my original understanding. =)

My attempt at forming a new understanding was driven by your example.

class Functor f where
>    type C f :: * -> Constraint
>    type C f = ()


such that

C :: (* -> *) -> * -> Constraint

In that, you put () in a position where it would have kind * -> Constraint,
hence my confusion when you subsequently stated that there was a bug that
needed to be fixed. =)

No.  () has kind * or Constraint, depending on context, never a ->
> Constraint.****
>
> Similarly (,) has kind * -> * -> * or Constraint -> Constraint ->
> Constraint, depending on context.
>

**
>
> Imaging that there are two sorts of parens, one for types and one for
> constraints.  We figure out which is intended from context.
>

Yep. We have a small compiler here at ClariFi for a very Haskell-like
language in which we've implemented pretty much this same scheme.

That said, instead of magically swapping kinds out we instead take the
superkind level and introduce subtyping at that level, giving us two
superkinds, say, Box and Circle, such that Circle is a sub-superkind of Box
and both * and Constraint have superkind Circle.

Then (,) :: forall (a: Circle). a -> a -> a and you don't need to swap
kinds on fully saturated tuples, and it can kind check types like '(,) ()'
in isolation without issue.

-Edward
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20111223/835ac2b0/attachment.htm>