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 _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
