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:[EMAIL PROTECTED]
> 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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
