flexible contexts and context reduction

[Tom Schrijvers]

On Thu, 27 Mar 2008, Sittampalam, Ganesh wrote:

> Well, Ord Foo doesn't hold, does it? So Ord (a, b) isn't equivalent to 
> (Ord a, Ord b).

It seems you (can) throw logic out of the window with flexible instances. 
So there's no point in talking about equivalences any more. We could still 
capture the operational aspect of it, but we'd need the type/data family 
counterpart of flexible instances.

Considering overlapping instances, there is still a logic, but it's 
implicit in the notation. You'd get for your 
example:

 	(a /= Foo \/ b \= Foo) ==> (Ord a /\ Ord b <=> Ord (a,b))

Again, an overlapping type/data family would be needed for encoding this 
in dictionaries.

Cheers,

Tom

> -----Original Message-----
> From: Simon Peyton-Jones [mailto:simonpj at microsoft.com]
> Sent: 27 March 2008 09:05
> To: Sittampalam, Ganesh; 'Tom Schrijvers'; Ganesh Sittampalam
> Cc: glasgow-haskell-users at haskell.org; Martin Sulzmann
> Subject: RE: flexible contexts and context reduction
>
> Why "unfortunately"? Looks fine to me.
>
> Simon
>
> |
> | Unfortunately, GHC accepts the following:
> |
> | {-# LANGUAGE FlexibleInstances #-}
> | module Foo2 where
> |
> | data Foo = Foo
> |   deriving Eq
> |
> | instance Ord (Foo, Foo) where
> |   (Foo, Foo) < (Foo, Foo) = False
>
> ==============================================================================
> 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
>

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: tom.schrijvers at cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/