RE: flexible contexts and context reduction

Well, Ord Foo doesn't hold, does it? So Ord (a, b) isn't equivalent to (Ord a, Ord b). Ganesh -----Original Message----- From: Simon Peyton-Jones [mailto:simonpj@microsoft.com] Sent: 27 March 2008 09:05 To: Sittampalam, Ganesh; 'Tom Schrijvers'; Ganesh Sittampalam Cc: glasgow-haskell-users@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 ==============================================================================

| Well, Ord Foo doesn't hold, does it? So Ord (a, b) isn't equivalent to (Ord a, Ord b). Indeed not. But that was not what Tom was suggesting (although he was not very explicit). What he meant was this: If you write the instance instance Theta => Foo (T a b) where ... where Theta is an arbitrary context, then, given a dictionary for (Foo (T a b)), you can get dictionaries for each constraint in Theta. Or in logic Theta <=> Foo (T a b) In your example, Theta is empty. If you'd written instance (Show a, Ix b) => Ord (a,b) then you could get a Show a and Ix b dictionaries from an Ord (a,b) dictionary. (But not an Ord a or Ord b one.) S | | Ganesh | | -----Original Message----- | From: Simon Peyton-Jones [mailto:simonpj@microsoft.com] | Sent: 27 March 2008 09:05 | To: Sittampalam, Ganesh; 'Tom Schrijvers'; Ganesh Sittampalam | Cc: glasgow-haskell-users@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 | ==============================================================================

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@microsoft.com] Sent: 27 March 2008 09:05 To: Sittampalam, Ganesh; 'Tom Schrijvers'; Ganesh Sittampalam Cc: glasgow-haskell-users@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@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@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/
participants (3)
-
Simon Peyton-Jones
-
Sittampalam, Ganesh
-
Tom Schrijvers