| 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...) Well, you'll just have to use the Empty class for that situation! Bottom line: I think we have agreed that what GHC implements is all we can reasonably do for now. Yell if you disagree Simon | -----Original Message----- | From: Gábor Lehel [mailto:illissius@gmail.com] | Sent: 09 January 2012 16:45 | To: Simon Peyton-Jones | Cc: Andres Löh; Antoine Latter; glasgow-haskell-users@haskell.org | Subject: Re: ConstraintKinds and default associated empty constraints | | On Mon, Jan 9, 2012 at 4:53 PM, Simon Peyton-Jones | <simonpj@microsoft.com> 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.