ConstraintKinds and default associated empty constraints
Simon PeytonJones
simonpj at microsoft.com
Mon Jan 9 19:04:47 CET 2012
 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 PeytonJones
 Cc: Andres Löh; Antoine Latter; glasgowhaskellusers at haskell.org
 Subject: Re: ConstraintKinds and default associated empty constraints

 On Mon, Jan 9, 2012 at 4:53 PM, Simon PeytonJones
 <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 typelevel lambdas (so you can write type C f = \_ > ()).

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


 >
 >  Original Message
 >  From: glasgowhaskellusersbounces at haskell.org [mailto:glasgowhaskell
 >  usersbounces at haskell.org] On Behalf Of Andres Löh
 >  Sent: 09 January 2012 07:28
 >  To: Antoine Latter
 >  Cc: glasgowhaskellusers 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
 > 
 >  _______________________________________________
 >  Glasgowhaskellusers mailing list
 >  Glasgowhaskellusers at haskell.org
 >  http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
 >
 >
 >
 > _______________________________________________
 > Glasgowhaskellusers mailing list
 > Glasgowhaskellusers at haskell.org
 > http://www.haskell.org/mailman/listinfo/glasgowhaskellusers



 
 Work is punishment for failing to procrastinate effectively.
More information about the Glasgowhaskellusers
mailing list