ConstraintKinds and default associated empty constraints

[Simon Peyton-Jones]

| 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 at gmail.com]
| Sent: 09 January 2012 16:45
| To: Simon Peyton-Jones
| Cc: Andres Löh; Antoine Latter; glasgow-haskell-users at haskell.org
| Subject: Re: ConstraintKinds and default associated empty constraints
| 
| On Mon, Jan 9, 2012 at 4:53 PM, Simon Peyton-Jones
| <simonpj at 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 at haskell.org [mailto:glasgow-haskell-
| > | users-bounces at haskell.org] On Behalf Of Andres Löh
| > | Sent: 09 January 2012 07:28
| > | To: Antoine Latter
| > | Cc: glasgow-haskell-users at 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 at haskell.org
| > | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
| >
| >
| >
| > _______________________________________________
| > Glasgow-haskell-users mailing list
| > Glasgow-haskell-users at haskell.org
| > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
| 
| 
| 
| --
| Work is punishment for failing to procrastinate effectively.