[Haskell] Re: Rebindable syntax for monads and arrows
Simon PeytonJones
simonpj at microsoft.com
Mon Jan 10 23:31:18 EST 2005
 You can to do this with GADTs:

 data MyVec a where
 MkMyVec :: (FinSet a) => Vec a > MyVec a

 instance Monad MyVec where
 return a = MkMyVec (vreturn a)
 etc.

 GADTs are scheduled for version 6.4 of GHC. The version of GHC now in
 CVS does not currently allow this however, see GHC bug #1097046.
I'm not sure how to fix this bug, or even if it is a bug. Let me
explain why.
Usually GHC is reluctant to perform context reduction by applying
instance declarations. Two reasons:
1. Postponing context reduction give more opportunities for sharing
2. With overlapping instance declarations, eager context reduction may
select an instance declaration "too early"; later, more type
information
may be available.
In fact, when you force context reduction by giving a type signature,
GHC complains if (2) applies with its "the instance selected depends on
the instantiation of x" message.
Now, suppose we have
f x = case x of
MkMyVec x > <rhs>
where (x::MyVec a) the <rhs> gives a constraint (Foo [a]). And suppose
we have
instance (Eq a, MyVec a) => Foo [a]
then you may say that f should get type
f :: Eq a => MyVec a > ...
because the MyVec part gets discharged by the MkMyVec pattern match,
leaving only the Eq a part. Fine. Now suppose there's an overlapping
instance declaration for Foo, say Foo [Char]. Then GHC would decline to
select the Foo [a] instance, so we'd infer the type
f :: Foo [a] => MyVec a > ....
There would be no error message in either case, just a different type
inferred. A programmer might well find this odd. Sometimes the MyVec
constraints are handled by the MkMyVec constructor, and sometimes they
aren't.
The root of the difficulty is that the MkMyVec constructor captures
constraints that mention no existentiallyquantified type variable, so
it'd make perfect sense to float them outwards. (In contrast,
constraints mentioning existentiallyquantified type variables *must* be
dealt with at the pattern match.)
Here's one idea. If you specify a type signature for 'f' then matters
are much clearer. In my example, if you specify
f :: Eq a => MyVec a > ...
then it's absolutely clear what constraints are available at the pattern
match (namely Eq a, MyVec a), and we solve all the constraints there.
So the rule would be:
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
usersupplied 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.)
But I suspect that programmers will prefer a more woolly rule that does
as much constraint solving as it can (provided all instance selection is
uniquely determined). That would give the slightly surprising behaviour
I describe above if an overlapping instance declaration was added.
Thoughts anyone?
Simon
More information about the Haskell
mailing list