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