[Haskell] GADT and constraints [Was: Rebindable syntax for monads and arrows]

[Martin Sulzmann]

Hi,

 > I can't understand how constraints float at all. In the following code:
 > 

Ex1:

 > > class Foo1 a  where foo1 :: a -> String
 > > class Foo2 a  where foo2 :: a -> String
 > >
 > > instance Foo1 Bool where foo1 _ = "Bool"
 > > instance Foo2 Char where foo2 _ = "Char"
 > >
 > > data U a where
 > >   Ub :: a -> U a
 > >   Uc :: a -> U a
 > >
 > > foo (Ub a) = foo1 a
 > > foo (Uc a) = foo2 a
 > 
 > What is the type of foo? GHC snapshot 6.3.20041106 happily accepts
 > that code, and even infers 
 > 	*M> :t foo
 > 	foo :: forall a. (Foo2 a, Foo1 a) => U a -> String
 > 
 > but that seems odd. In any value of type U a, either Ub alternative is
 > present, or Uc. They can never be both. Then why do we get the
 > constraint that is the intersection of the two constraints rather than
 > the union of them?  

Inference is conservative and combines (ie. intersects) the results
from both branches. The type is correct (Chameleon infers the same type).

Take a look at 

 A Unifying Inference Framework for Hindley/Milner with Extensions 
(http://www.comp.nus.edu.sg/~sulzmann/)

for a detailed description of inference.


 > BTW, when I tried to do
 > 

Ex2:

 > > data U a where
 > >   Ub :: Foo1 => a -> U a
 > >   Uc :: Foo2 => a -> U a
 > 
 > 

Replace Foo1 by Foo1 a and Foo2 by Foo2 a.
then  foo has type U a -> String


 > Anyway, even though GHC accepts the code and infers the type for foo,
 > the function is unusable. An attempt to evaluate 'foo (Ub True)' ends
 > up in an error message that there is no instance of Foo2 Bool. Indeed,
 > there isn't. But why that should matter if I'm only interested in the
 > Ub alternative? Again, the function 'foo' seems legitimate, and can be
 > easily expressed either in Martin Sulzmann's interpretation of GRDT
 > via existentials, or using the typeclass representation of GADT. For
 > example:
 > 
 > > data Ub a = Ub a
 > > data Uc a = Uc a
 > >
 > > class Foo t where foo:: t -> String
 > >
 > > instance Foo1 a => Foo (Ub a) where 
 > >     foo (Ub a) = foo1 a
 > > instance Foo2 a => Foo (Uc a) where 
 > >     foo (Uc a) = foo2 a
 > 
 > Here, the constraint Foo is clearly the `union' of Foo1 and Foo2 (the
 > discriminated union at that).
 > 

You're encoding Ex2 and not Ex1. Ex2 uses GADTs (aka GRDTs, ...)
but Ex1 only uses ordinary algebraic data types.

Martin