ConstraintKinds and default associated empty constraints

[Simon Peyton-Jones]

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

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

sorry -- that was simply type incorrect.  () does not have kind *  -> Constraint

S

From: Edward Kmett [mailto:ekmett at gmail.com]
Sent: 23 December 2011 16:41
To: Simon Peyton-Jones
Cc: Bas van Dijk; glasgow-haskell-users at haskell.org
Subject: Re: ConstraintKinds and default associated empty constraints

On Fri, Dec 23, 2011 at 10:17 AM, Simon Peyton-Jones <simonpj at microsoft.com<mailto: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/d60955e3/attachment-0001.htm>