GADT and constraints [Was: Rebindable syntax for monads and arrows]
Simon Peyton-Jones wrote: |[ data MyVec a where |[ MkMyVec :: (Foo a) => a -> MyVec a
f x = case x of MkMyVec x -> <rhs>
constraints are always solved *lazily* when inferring, so we'd infer f :: Foo [a] => MyVec a -> ... even without any overlap
but they are solved *eagerly* when checking against a user-supplied type sig so when checking f :: Eq a => MyVec a => ... we'd accept the program. (If there were overlapping instances, we'd complain about them.)
I can't understand how constraints float at all. In the following code:
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? BTW, when I tried to do
data U a where Ub :: Foo1 => a -> U a Uc :: Foo2 => a -> U a
I received a message
Couldn't match kind `*' against `k_a1QK -> *' In the class declaration for `Foo2'
which I found quite interesting. 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).
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
participants (2)
-
Martin Sulzmann -
oleg＠pobox.com