Re: Type classes in GADTs

2008-10-30 Thread Jason Dagit 
On Wed, Oct 29, 2008 at 10:20 PM, C Rodrigues [EMAIL PROTECTED] wrote:

 I discovered that closed type classes can be implicitly defined using GADTs  
 The GADT value itself acts like a class dictionary.  However, GHC (6.83) 
 doesn't know anything about these type classes, and it won't infer any class 
 memberships.  In the example below, an instance of Eq is not recognized.

 So is this within the domain of GHC's type inference, not something it shoud 
 infer, or a bug?

 {-# OPTIONS_GHC -XTypeFamilies -XGADTs -XEmptyDataDecls #-}
 module CaseAnalysisOnGADTs where

 -- Commutative and associative operators.
 data CAOp a where
Sum:: CAOp Int
Disj   :: CAOp Bool
Concat :: CAOp String

I guess when you write something like this the type checker doesn't
look at the closed set of types that 'a' can take on.  I don't know
why that would be a problem in your example, but if we did this:

data CAOp a where
   Sum :: CAOp Int
   Disj  :: CAOP Bool
   Concat :: CAOp String
   Weird :: Show a = CAOp a

Now we have a problem, because the set of types for is { Int, Bool,
String, forall a. Show a = a}.  It's not a closed set anymore.  And I
think, but I'm just making this up, that the above set of type must be
hard to reason about.  I think it would essentially be:

data Show a = CAOp a where ...

And GHC won't allow that, presumably for a good reason.  Neat example,
and I hope someone sheds more light on this.

By the way, since you mention ghc6.8.3, does that mean some other
version of GHC permits noEvidenceOfEq to type check?  I tried 6.6.1
but that didn't accept it either.

Jason
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type classes in GADTs

2008-10-30 Thread Daniil Elovkov 

Jason Dagit wrote:

On Wed, Oct 29, 2008 at 10:20 PM, C Rodrigues [EMAIL PROTECTED] wrote:

I discovered that closed type classes can be implicitly defined using GADTs  
The GADT value itself acts like a class dictionary.  However, GHC (6.83) 
doesn't know anything about these type classes, and it won't infer any class 
memberships.  In the example below, an instance of Eq is not recognized.

So is this within the domain of GHC's type inference, not something it shoud 
infer, or a bug?

{-# OPTIONS_GHC -XTypeFamilies -XGADTs -XEmptyDataDecls #-}
module CaseAnalysisOnGADTs where

-- Commutative and associative operators.
data CAOp a where
   Sum:: CAOp Int
   Disj   :: CAOp Bool
   Concat :: CAOp String


I guess when you write something like this the type checker doesn't
look at the closed set of types that 'a' can take on.  I don't know
why that would be a problem in your example, but if we did this:

data CAOp a where
   Sum :: CAOp Int
   Disj  :: CAOP Bool
   Concat :: CAOp String
   Weird :: Show a = CAOp a

Now we have a problem, because the set of types for is { Int, Bool,
String, forall a. Show a = a}.  It's not a closed set anymore.  And I
think, but I'm just making this up, that the above set of type must be
hard to reason about.  I think it would essentially be:

data Show a = CAOp a where ...



I agree with Jason here. Actually we can think of quite a lot of examples where 
the type checker _can_ know something what we see as obvious. But that 
something is a special case of a more general situation which is far less 
obvious and knowing it may require serious program analysis.

Then, regarding handling some special cases, I think it's a matter of keeping 
type checker predictable and clean.

In this particular case, handling this situation would require type checker to look at 
the _values_ of the given datatype, which as I understand Haskell type checker doesn't. 
If we later add members to CAOp the valid program may become invalid, though the 
signature of CAOp hasn't changed. That doesn't look good. Not all members of 
CAOp may be exported from a module, that would have to be taken into account as well, 
probably.

In your example, why not just do

traditionalEvidenceOfEq :: Eq a = D a - Bool


--
Daniil Elovkov

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: Type classes in GADTs

2008-10-30 Thread C Rodrigues 

Thanks for the explanation.  I see how this wouldn't behave nicely with 
automatic class constraint inference.  I didn't test the example on any other 
GHC versions.

I will probably end up passing in the Eq dictionary from outside like Daniil 
suggested.  I would prefer to do the following, but GHC doesn't accept the type 
signature.

evidenceOfEq :: CAOp a - (Eq a = b) - b

Neither does it accept data EqConstraint a b = EqConstraint (Eq a = b).  
Foiled again.
_
Want to read Hotmail messages in Outlook? The Wordsmiths show you how.
http://windowslive.com/connect/post/wedowindowslive.spaces.live.com-Blog-cns!20EE04FBC541789!167.entry?ocid=TXT_TAGLM_WL_hotmail_092008___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type classes in GADTs

2008-10-30 Thread Thomas Schilling 
2008/10/30 C Rodrigues [EMAIL PROTECTED]:
 evidenceOfEq :: CAOp a - (Eq a = b) - b

isn't that the same as:

  evidenceOfEq :: Eq a = CAOp a - b - b


 Neither does it accept data EqConstraint a b = EqConstraint (Eq a = b).  
 Foiled again.

same here:

  data Eq a = EqConstraint a b = EqConstraint b.

although this must be a typo, since it doesn't make any sense to me.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users