it’s a bug. I’m fixing it. Simon From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of Edward Kmett Sent: 22 December 2011 17:03 To: Bas van Dijk Cc: glasgow-haskell-users@haskell.org Subject: Re: ConstraintKinds and default associated empty constraints On Wed, Dec 21, 2011 at 6:45 PM, Bas van Dijk mailto:v.dijk.bas@gmail.com> wrote: I'm playing a bit with the new ConstraintKinds feature in GHC 7.4.1-rc1. I'm trying to give the Functor class an associated constraint so that we can make Set an instance of Functor. The following code works but I wonder if the trick with: class Empty a; instance Empty a, is the recommended way to do this: {-# LANGUAGE ConstraintKinds, TypeFamilies, FlexibleInstances #-} import GHC.Prim (Constraint) import Prelude hiding (Functor, fmap) import Data.Set (Set) import qualified Data.Set as S (map, fromList) class Functor f where type C f :: * -> Constraint type C f = Empty fmap :: (C f a, C f b) => (a -> b) -> f a -> f b class Empty a; instance Empty a instance Functor Set where type C Set = Ord fmap = S.map instance Functor [] where fmap = map testList = fmap (+1) [1,2,3] testSet = fmap (+1) (S.fromList [1,2,3]) Cheers and thanks for a great new feature! Bas This is the same solution I wound up with in https://github.com/ekmett/constraints Adding an argument to the family would work but is somewhat unsatisfying as it mucks with polymorphic recursive use of the dictionary, and with placing constraints on constraints, so I prefer to keep as few arguments as possible. You can go farther with Functor by using polymorphic kinds and indexing the source and destination Category as well as the class of objects in the category. I should probably write up what I've done with this, but doing so lets you have real product and coproduct Category instances, which were previously not possible (a fact which in part drove me to write all the semigroupoid code i have on hackage. -Edward

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. As I understand you, fixing this seems to indicate that () could have any 'a -> Constraint' kind as well. 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. S From: Edward Kmett [mailto:ekmett@gmail.com] Sent: 23 December 2011 15:05 To: Simon Peyton-Jones Cc: Bas van Dijk; glasgow-haskell-users@haskell.org Subject: Re: ConstraintKinds and default associated empty constraints Fair enough. So if I understand you correctly, () is becoming more overloaded as to its kind? Right now it seems it is either * or Constraint depending on context. As I understand you, fixing this seems to indicate that () could have any 'a -> Constraint' kind as well. This raises similar questions about (,) and how to build 'a -> Constraint' products nicely. Sent from my iPad On Dec 23, 2011, at 4:42 AM, Simon Peyton-Jones mailto:simonpj@microsoft.com> wrote: it’s a bug. I’m fixing it. Simon From: glasgow-haskell-users-bounces@haskell.orgmailto:glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of Edward Kmett Sent: 22 December 2011 17:03 To: Bas van Dijk Cc: glasgow-haskell-users@haskell.orgmailto:glasgow-haskell-users@haskell.org Subject: Re: ConstraintKinds and default associated empty constraints On Wed, Dec 21, 2011 at 6:45 PM, Bas van Dijk mailto:v.dijk.bas@gmail.com> wrote: I'm playing a bit with the new ConstraintKinds feature in GHC 7.4.1-rc1. I'm trying to give the Functor class an associated constraint so that we can make Set an instance of Functor. The following code works but I wonder if the trick with: class Empty a; instance Empty a, is the recommended way to do this: {-# LANGUAGE ConstraintKinds, TypeFamilies, FlexibleInstances #-} import GHC.Prim (Constraint) import Prelude hiding (Functor, fmap) import Data.Set (Set) import qualified Data.Set as S (map, fromList) class Functor f where type C f :: * -> Constraint type C f = Empty fmap :: (C f a, C f b) => (a -> b) -> f a -> f b class Empty a; instance Empty a instance Functor Set where type C Set = Ord fmap = S.map instance Functor [] where fmap = map testList = fmap (+1) [1,2,3] testSet = fmap (+1) (S.fromList [1,2,3]) Cheers and thanks for a great new feature! Bas This is the same solution I wound up with in https://github.com/ekmett/constraints Adding an argument to the family would work but is somewhat unsatisfying as it mucks with polymorphic recursive use of the dictionary, and with placing constraints on constraints, so I prefer to keep as few arguments as possible. You can go farther with Functor by using polymorphic kinds and indexing the source and destination Category as well as the class of objects in the category. I should probably write up what I've done with this, but doing so lets you have real product and coproduct Category instances, which were previously not possible (a fact which in part drove me to write all the semigroupoid code i have on hackage. -Edward

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@gmail.com] Sent: 23 December 2011 16:41 To: Simon Peyton-Jones Cc: Bas van Dijk; glasgow-haskell-users@haskell.org Subject: Re: ConstraintKinds and default associated empty constraints On Fri, Dec 23, 2011 at 10:17 AM, Simon Peyton-Jones mailto:simonpj@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

On 1/8/12 8:32 AM, Bas van Dijk wrote:

On 23 December 2011 17:44, Simon Peyton-Jones wrote:

...

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

So am I correct that the `class Empty a; instance Empty a` trick is currently the only way to get default associated empty constraints?

Couldn't the following work? class Functor f where type C f :: * -> Constraint type C f _ = () It seems to me that adding const to the type level (either implicitly or explicitly) is cleaner and simpler than overloading () to be Constraint, *->Constraint, *->*->Constraint,... -- Live well, ~wren

On Mon, Jan 9, 2012 at 12:30 AM, Antoine Latter wrote:

On Sun, Jan 8, 2012 at 11:21 PM, wren ng thornton wrote:

...

Couldn't the following work?

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

I get a parse error from that.

The equivalent:

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

The definitions are accepted by GHC: class Functor f where type FC f a :: Constraint type FC f a = () fmap :: (FC f a, FC f b) => (a -> b) -> f a -> f b instance Functor [] where fmap = map But I don't like the 'a' being an index parameter, and then the following expression: fmap (+1) [1::Int] Gives the error: Could not deduce (FC [] Int) arising from a use of `fmap' In the expression: fmap (+ 1) [1 :: Int] In an equation for `it': it = fmap (+ 1) [1 :: Int]

gives the error:

   Number of parameters must match family declaration; expected 1    In the type synonym instance default declaration for `FC'    In the class declaration for `Functor'

...

It seems to me that adding const to the type level (either implicitly or explicitly) is cleaner and simpler than overloading () to be Constraint, *->Constraint, *->*->Constraint,...

-- Live well, ~wren

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Three things about this ConstraintKinds thread: First, about class Functor f where type C f a :: Constraint type C f a = () vs class Functor f where type C f :: * -> Constraint type C f = \_ -> () I don't know any way of dealing in a decent way with the latter, because it lacks type level lambdas. GHC currently allows only the former. I hope that is enough. If not, perhaps give an example? Second, it's true that the former would permit you to *index* on 'a' as well as being parametric in 'a' (which is probably more what you intend). That's a deficiency, but it's largely a notational one. Maybe there should be some way to specify in a type family definition that some parameters can't be used for indexing. It's orthogonal to the question of Constraint kinds, or of defaults for associated types. Third, () does indeed stand both for the unit tuple and for the empty constraint, depending on context. So the code below works fine with HEAD. I think it's ok with the 7.4 branch too, but it would be safer if someone would check that. I included a test for the case tha Antoine found an error with, namely Could not deduce (FC [] Int) arising from a use of `fmap' Simon =================================================================== {-# LANGUAGE ConstraintKinds, TypeFamilies, FlexibleInstances #-} module CK where import GHC.Prim (Constraint) import Prelude hiding (Functor, fmap) import Data.Set (Set) import qualified Data.Set as S (map, fromList) class Functor f where type C f a :: Constraint type C f a = () fmap :: (C f a, C f b) => (a -> b) -> f a -> f b instance Functor Set where type C Set a = Ord a fmap = S.map instance Functor [] where fmap = map testList = fmap (+1) [1,2,3] testSet = fmap (+1) (S.fromList [1,2,3]) test2 = fmap (+1) [1::Int] | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell- | users-bounces@haskell.org] On Behalf Of Andres Löh | Sent: 09 January 2012 07:28 | To: Antoine Latter | Cc: glasgow-haskell-users@haskell.org | Subject: Re: ConstraintKinds and default associated empty constraints | | Hi. | | > The definitions are accepted by GHC: | > | >   class Functor f where | >       type FC f a :: Constraint | >       type FC f a = () | > | >       fmap :: (FC f a, FC f b) => (a -> b) -> f a -> f b | > | >   instance Functor [] where | >       fmap = map | | Yes. This is what I would have expected to work. | | > But I don't like the 'a' being an index parameter, and then the | > following expression: | > | >   fmap (+1) [1::Int] | > | > Gives the error: | > | >    Could not deduce (FC [] Int) arising from a use of `fmap' | >    In the expression: fmap (+ 1) [1 :: Int] | >    In an equation for `it': it = fmap (+ 1) [1 :: Int] | > | >> gives the error: | >> | >>    Number of parameters must match family declaration; expected 1 | >>    In the type synonym instance default declaration for `FC' | >>    In the class declaration for `Functor' | | I get the same error, but it looks like a bug to me: If I move the | declaration | | type FC f a = () | | to the instance, then the example passes. | | Cheers, | Andres | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Just a note: as section 6 of [1] notes, one way (possibly the only?) to satisfy a universally quantified constraint would be a suitably polymorphic instance — i.e. with a type variable in the head. I think this would mitigate the need for whole program analysis at least in some cases, including our current Functor example. On the other hand, the Empty class does nicely avoid this entire problem for this particular case. [1] — http://www.haskell.org/haskellwiki/Quantified_contexts On Mon, Jan 9, 2012 at 10:44 AM, Gábor Lehel wrote:

On Mon, Jan 9, 2012 at 4:53 PM, Simon Peyton-Jones wrote:

...

Three things about this ConstraintKinds thread:

First, about  class Functor f where    type C f a :: Constraint    type C f a = () vs  class Functor f where    type C f :: * -> Constraint    type C f = \_ -> ()

I don't know any way of dealing in a decent way with the latter, because it lacks type level lambdas.  GHC currently allows only the former.  I hope that is enough.  If not, perhaps give an example?

Second, it's true that the former would permit you to *index* on 'a' as well as being parametric in 'a' (which is probably more what you intend).  That's a deficiency, but it's largely a notational one.  Maybe there should be some way to specify in a type family definition that some parameters can't be used for indexing.  It's orthogonal to the question of Constraint kinds, or of defaults for associated types.

Third, () does indeed stand both for the unit tuple and for the empty constraint, depending on context.  So the code below works fine with HEAD.  I think it's ok with the 7.4 branch too, but it would be safer if someone would check that.  I included a test for the case tha Antoine found an error with, namely            Could not deduce (FC [] Int) arising from a use of `fmap'

Simon

=================================================================== {-# LANGUAGE ConstraintKinds, TypeFamilies, FlexibleInstances #-} module CK where

import GHC.Prim (Constraint)

import Prelude hiding (Functor, fmap)

import           Data.Set (Set) import qualified Data.Set as S (map, fromList)

class Functor f where    type C f a :: Constraint    type C f a = ()

   fmap :: (C f a, C f b) => (a -> b) -> f a -> f b

instance Functor Set where    type C Set a = Ord a    fmap = S.map

instance Functor [] where    fmap = map

testList = fmap (+1) [1,2,3] testSet  = fmap (+1) (S.fromList [1,2,3]) test2 = fmap (+1) [1::Int]

The problem with this is that you can't write, for example:

type OldFunctor f = (Functor f, forall a. C (f a) ~ ())

(If we had quantified contexts[1], then maybe, but we don't, and it doesn't seem like it would be even theoretically possible for indexed constraints without whole program analysis.)

With the other solution, though, you can write:

type OldFunctor f = (Functor f, C f ~ Empty) -- (In the real world I'd rather call these Functor and Exofunctor...)

Again, I have no problem at all with the Empty class, it's the same solution I've used. It's even kind polymorphic if you turn that extension on. The syntax isn't superficially as nice, but it's nice enough, does the job, and I don't see how you could do better short of adding type-level lambdas (so you can write type C f = \_ -> ()).

[1] http://hackage.haskell.org/trac/ghc/ticket/2893

...

| -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell- | users-bounces@haskell.org] On Behalf Of Andres Löh | Sent: 09 January 2012 07:28 | To: Antoine Latter | Cc: glasgow-haskell-users@haskell.org | Subject: Re: ConstraintKinds and default associated empty constraints | | Hi. | | > The definitions are accepted by GHC: | > | >   class Functor f where | >       type FC f a :: Constraint | >       type FC f a = () | > | >       fmap :: (FC f a, FC f b) => (a -> b) -> f a -> f b | > | >   instance Functor [] where | >       fmap = map | | Yes. This is what I would have expected to work. | | > But I don't like the 'a' being an index parameter, and then the | > following expression: | > | >   fmap (+1) [1::Int] | > | > Gives the error: | > | >    Could not deduce (FC [] Int) arising from a use of `fmap' | >    In the expression: fmap (+ 1) [1 :: Int] | >    In an equation for `it': it = fmap (+ 1) [1 :: Int] | > | >> gives the error: | >> | >>    Number of parameters must match family declaration; expected 1 | >>    In the type synonym instance default declaration for `FC' | >>    In the class declaration for `Functor' | | I get the same error, but it looks like a bug to me: If I move the | declaration | | type FC f a = () | | to the instance, then the example passes. | | Cheers, |   Andres | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-- Work is punishment for failing to procrastinate effectively.

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

That would be nice. It would also be nice to be able to use _ in type signatures as in: const :: a -> _ -> a const x _ = x During type checking each _ could be replaced by a new unique type variable. Visa versa should also be possible: during type inferencing each unique type variable could be replaced by a _. Bas On Jan 9, 2012 6:22 AM, "wren ng thornton" wrote:

On 1/8/12 8:32 AM, Bas van Dijk wrote:

...

On 23 December 2011 17:44, Simon Peyton-Jones> wrote:

...

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

So am I correct that the `class Empty a; instance Empty a` trick is currently the only way to get default associated empty constraints?

Couldn't the following work?

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

It seems to me that adding const to the type level (either implicitly or explicitly) is cleaner and simpler than overloading () to be Constraint, *->Constraint, *->*->Constraint,...

-- Live well, ~wren

______________________________**_________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.**org http://www.haskell.org/**mailman/listinfo/glasgow-**haskell-usershttp://www.haskell.org/mailman/listinfo/glasgow-haskell-users