flexible contexts and context reduction

[Tristan Allwood]

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 at talk21.com] 
> Sent: 27 March 2008 12:25
> To: Sittampalam, Ganesh; Ganesh Sittampalam
> Cc: glasgow-haskell-users at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-- 
Tristan Allwood
PhD Student
Department of Computing
Imperial College London