RE: flexible contexts and context reduction
Because I want to be able to make Foo values where the parameter type isn't in Ord, too. I just want unFoo to work on specific Foo values where it is. -----Original Message----- From: Claus Reinke [mailto:claus.reinke@talk21.com] Sent: 27 March 2008 12:25 To: Sittampalam, Ganesh; Ganesh Sittampalam Cc: glasgow-haskell-users@haskell.org Subject: Re: flexible contexts and context reduction perhaps i'm missing something but, instead of trying to deduce conditions from conclusions, why can't you just follow ghc's suggestion, and add the constraints to the constructor? data Foo a where Foo1 :: a -> Foo a Foo2 :: (Ord a,Ord b) => Foo a -> Foo b -> Foo (a, b) (possibly with another constraint on Foo1) claus
A closer example to what I was actually doing was this:
{-# LANGUAGE GADTs #-} module Foo where
data Foo a where Foo1 :: a -> Foo a Foo2 :: Foo a -> Foo b -> Foo (a, b)
unFoo :: Ord a => Foo a -> a unFoo (Foo1 a) = a unFoo (Foo2 x y) = (unFoo x, unFoo y)
[in the real code I did actually use the Ord constraint in the base case]
The error I get is this:
Foo.hs:10:20: Could not deduce (Ord a2) from the context () arising from a use of `unFoo' at Foo.hs:10:20-26 Possible fix: add (Ord a2) to the context of the constructor `Foo2' In the expression: unFoo x In the expression: (unFoo x, unFoo y) In the definition of `unFoo': unFoo (Foo2 x y) = (unFoo x, unFoo y)
Foo.hs:10:29: Could not deduce (Ord b1) from the context () arising from a use of `unFoo' at Foo.hs:10:29-35 Possible fix: add (Ord b1) to the context of the constructor `Foo2' In the expression: unFoo y In the expression: (unFoo x, unFoo y) In the definition of `unFoo': unFoo (Foo2 x y) = (unFoo x, unFoo y)
Which suggests that GHC has also lost track of the fact that Ord (a, b) is true. But it would certainly be necessary to get from Ord (a, b) to (Ord a, Ord b) to get that to work.
============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================
Because I want to be able to make Foo values where the parameter type isn't in Ord, too. I just want unFoo to work on specific Foo values where it is.
but your recursive function requires a recursive constraint, which your data type does not guarantee by construction, and which the Ord instances do not guarantee due to lack of closed classes. a rather pedestrian approach would record during construction whether or not all parts are in Ord (see below). i really wanted to record that information only in the leaf, using the type family and the commented-out parts to propagate the information through Foo2, but unfortunately, ghc does not see that the only case for which And returns True requires both parameters to be True (closed families/classes would help, again?), so i had to split up Foo2 as well. not pretty, but might get you a step further? perhaps some of Oleg's workarounds for closed classes and context-based overloading might help to merge the four constructors into two again. that would get rid of the junk (you can't promise too much, but you can promise too little by using the wrong constructor version below). claus {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} module Foo where data True = T data False = F type family And a b :: * type instance And True True = True type instance And True False = False type instance And False True = False type instance And False False = False data Foo ord a where Foo1 :: a -> Foo False a Foo1o :: Ord a => a -> Foo True a -- Foo2 :: And oa ob ~ ord => ord -> Foo oa a -> Foo ob b -> Foo ord (a, b) Foo2 :: Foo oa a -> Foo ob b -> Foo False (a, b) Foo2o :: Foo True a -> Foo True b -> Foo True (a, b) unFoo :: Foo True a -> a unFoo (Foo1o a) = if a>a then a else a -- unFoo (Foo2 T x y) = (unFoo x, unFoo y) unFoo (Foo2o x y) = (unFoo x, unFoo y)
A closer example to what I was actually doing was this:
{-# LANGUAGE GADTs #-} module Foo where
data Foo a where Foo1 :: a -> Foo a Foo2 :: Foo a -> Foo b -> Foo (a, b)
unFoo :: Ord a => Foo a -> a unFoo (Foo1 a) = a unFoo (Foo2 x y) = (unFoo x, unFoo y)
[in the real code I did actually use the Ord constraint in the base case]
Hi, Would passing around witnesses help? Of course you need to know about the witness you want when creating the Foo's, but I'm not sure about your needs... {-# LANGUAGE TypeOperators, GADTs, RankNTypes #-} data Foo a where Foo1 :: Witness a -> a -> Foo a Foo2 :: Witness a -> Witness b -> Foo a -> Foo b -> Foo (a,b) unFoo :: (forall x y . Witness x -> Witness y -> Witness (x,y)) -> Foo a -> (a, Witness a) unFoo f (Foo1 w x) = (x, w) unFoo f (Foo2 wa wb fa fb) = ((ra, rb), f wa' wb') where (ra,wa') = unFoo f fa (rb,wb') = unFoo f fb data Witness a where OrdW :: Ord a => Witness a IdW :: Witness a unFooOrd :: (Ord a) => Foo a -> a unFooOrd = fst . unFoo (\OrdW OrdW -> OrdW) Regards, Tris On Thu, Mar 27, 2008 at 08:29:03AM -0400, Sittampalam, Ganesh wrote:
Because I want to be able to make Foo values where the parameter type isn't in Ord, too. I just want unFoo to work on specific Foo values where it is.
-----Original Message----- From: Claus Reinke [mailto:claus.reinke@talk21.com] Sent: 27 March 2008 12:25 To: Sittampalam, Ganesh; Ganesh Sittampalam Cc: glasgow-haskell-users@haskell.org Subject: Re: flexible contexts and context reduction
perhaps i'm missing something but, instead of trying to deduce conditions from conclusions, why can't you just follow ghc's suggestion, and add the constraints to the constructor?
data Foo a where Foo1 :: a -> Foo a Foo2 :: (Ord a,Ord b) => Foo a -> Foo b -> Foo (a, b)
(possibly with another constraint on Foo1)
claus
A closer example to what I was actually doing was this:
{-# LANGUAGE GADTs #-} module Foo where
data Foo a where Foo1 :: a -> Foo a Foo2 :: Foo a -> Foo b -> Foo (a, b)
unFoo :: Ord a => Foo a -> a unFoo (Foo1 a) = a unFoo (Foo2 x y) = (unFoo x, unFoo y)
[in the real code I did actually use the Ord constraint in the base case]
The error I get is this:
Foo.hs:10:20: Could not deduce (Ord a2) from the context () arising from a use of `unFoo' at Foo.hs:10:20-26 Possible fix: add (Ord a2) to the context of the constructor `Foo2' In the expression: unFoo x In the expression: (unFoo x, unFoo y) In the definition of `unFoo': unFoo (Foo2 x y) = (unFoo x, unFoo y)
Foo.hs:10:29: Could not deduce (Ord b1) from the context () arising from a use of `unFoo' at Foo.hs:10:29-35 Possible fix: add (Ord b1) to the context of the constructor `Foo2' In the expression: unFoo y In the expression: (unFoo x, unFoo y) In the definition of `unFoo': unFoo (Foo2 x y) = (unFoo x, unFoo y)
Which suggests that GHC has also lost track of the fact that Ord (a, b) is true. But it would certainly be necessary to get from Ord (a, b) to (Ord a, Ord b) to get that to work.
============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer:
http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
-- Tristan Allwood PhD Student Department of Computing Imperial College London
participants (3)
-
Claus Reinke -
Sittampalam, Ganesh -
Tristan Allwood