RE: the MPTC Dilemma (please solve)
With help from Martin Sulzmann and Ross Paterson, GHC (HEAD) now
implements a richer form of functional dependencies than Mark Jones's
version, but still decidable etc. The rules for what must appear in the
context of an instance declaration are also relaxed.
The specification is here:
http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extensions
.html#instance-decls
I think this is a step forward, and a serious candidate for Haskell'. I
think that if you stick to these rules, everything is nailed down as
Martin so rightly says it should be. And I am not sure we can go much
further.
Of course -fallow-undecidable-instances still lifts all restrictions,
and then all bets are off.
Many thanks to Ross and Martin. You can try it out by downloading a GHC
snapshot (or by building from source).
Simon
| -----Original Message-----
| From: haskell-prime-bounces@haskell.org
[mailto:haskell-prime-bounces@haskell.org] On Behalf Of
| isaac jones
| Sent: 11 February 2006 01:29
| To: haskell-prime@haskell.org
| Subject: the MPTC Dilemma (please solve)
|
| I've created a wiki page and a ticket to record solutions to what I'm
| calling the "Multi Parameter Type Class Dilemma". It's summarized
| thusly:
|
| MultiParamTypeClasses are very useful, but mostly in the context of
| FunctionalDependencies. They are particularly used in the monad
| transformer library found in fptools. The dilemma is that functional
| dependencies are "very, very tricky" (spj). AssociatedTypes are
| promising but unproven. Without a solution, Haskell' will be somewhat
| obsolete before it gets off the ground.
|
| I've proposed a few solutions. Please help to discover more solutions
| and/or put them on the ticket/wiki.
|
| Wiki page:
| http://hackage.haskell.org/trac/haskell-prime/ticket/90
|
| Ticket:
|
http://hackage.haskell.org/trac/haskell-prime/wiki/MultiParamTypeClasses
Dilemma
|
|
| peace,
|
| isaac
|
|
|
| --
| isaac jones
Simon Peyton-Jones wrote:
Of course -fallow-undecidable-instances still lifts all restrictions, and then all bets are off.
Is the behaviour of GHC with -fallow-undecidable-instances (and -fcontext-stack) well-understood and specifiable? It is a very useful option, as you can join (meet?) classes like this: class P a class Q a class (P a,Q a) => PQ a instance (P a,Q a) => PQ a -- Ashley Yakeley
The specification is here: http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extensions.htm...
two questions/suggestions about this: 1. there are other termination criteria one migh think of, though many will be out because they are not easy to specify. but here is an annoyingly simple example that doesn't fit the current rules even though it is clearly terminating (it's not even recursive): class Fail all -- no instances! class TypeNotEq a b instance Fail a => TypeNotEq a a instance TypeNotEq a b class Test a b where test :: a -> b -> Bool instance TypeNotEq a b => Test a b where test _ _ = False instance Test a a where test _ _ = True main = print $ (test True 'c', test True False) never mind the overlap, the point here is that we redirect from Test a b to TypeNotEq a b, and ghc informs us that the "Constraint is no smaller than the instance head". it is true that the parameters don't get smaller (same number, same number of constructors, etc.), but they are passed to a "smaller" predicate (in terms of call-graph reachability: there are fewer predicates reachable from TypeNotEq than from Test - in particular, Test is not reachable from TypeNotEq). this is a non-local criterion, but a fairly simple one. and it seems very strange to invoke "undecidable instances" for this example (or is there anything undecidable about it?). 2. the coverage condition only refers to the instance head. this excludes programs such as good old record selection (which should terminate because it recurses over finite types, and is confluent -in fact deterministic- because of best-fit overlap resolution): -- | field selection infixl #? class Select label val rec | label rec -> val where (#?) :: rec -> label -> val instance Select label val ((label,val),r) where ((_,val),_) #? label = val instance Select label val r => Select label val (l,r) where (_,r) #? label = r #? label now, it is true that in the second instance declaration, "val" is not covered in {label,(l,r)}. however, it is covered in the recursive call, subject to the very same FD, if that recursive call complies with the (recursive) coverage criterion. in fact, for this particular task, that is the only place where it could be covered. would it be terribly difficult to take such indirect coverage (via the instance constraints) into account? there'd be no search involved (the usual argument against looking at the constraints), and it seems strange to exclude such straightforward "consume a type" recursions, doesn't it? cheers, claus
On Tue, Feb 28, 2006 at 07:53:38PM -0000, Claus Reinke wrote:
class Fail all -- no instances!
class TypeNotEq a b instance Fail a => TypeNotEq a a instance TypeNotEq a b
class Test a b where test :: a -> b -> Bool instance TypeNotEq a b => Test a b where test _ _ = False instance Test a a where test _ _ = True
main = print $ (test True 'c', test True False)
never mind the overlap, the point here is that we redirect from Test a b to TypeNotEq a b, and ghc informs us that the "Constraint is no smaller than the instance head".
it is true that the parameters don't get smaller (same number, same number of constructors, etc.), but they are passed to a "smaller" predicate (in terms of call-graph reachability: there are fewer predicates reachable from TypeNotEq than from Test - in particular, Test is not reachable from TypeNotEq).
Yes, one could waive these restrictions on the constraint and head if they were not part of a cycle. Then when you added an instance that completed a cycle, the restrictions would come into force, on all the instances in the cycle. Non-local criteria are a bit more complex for the programmer, though (ignoring the implementor for the moment). I'll add the possibility to the wiki.
this is a non-local criterion, but a fairly simple one. and it seems very strange to invoke "undecidable instances" for this example (or is there anything undecidable about it?).
Any termination criterion will be necessarily conservative, and will bite in some cases where termination is obvious to the human eye. The question is how far out to push the boundary, trading power for complexity.
participants (4)
-
Ashley Yakeley -
Claus Reinke -
Ross Paterson -
Simon Peyton-Jones