A while ago, Sebastian Fischer made me aware of a subtle bug in the
type-classes branch of MCC (for those who are not aware of it, the
source is available in the darcs repository at [1]). Consider a type
class
> class Arb a where
> arb :: a
This definition introduces a new overloaded function arb with
no arguments. An instance of this class for type Bool could be
defined by
> instance Arb Bool where
> arb = False ? True
Evaluating the goal
arb::Bool
in the interpreter yields the expected results, namely False
and True. Now let us define a few small functions using arb.
> arbP2 = (arb,arb)
> arbL2 = [arb,arb]
If we evaluate
arbP2 :: (Bool,Bool)
we get the four expected results (False,False), (False,True),
(True,False), and (True,True). But if we evaluate the goal
arbL2 :: [Bool]
we observe a surprising result or rather absence of results.
The interpreter computes only [False,False] and [True,True],
but neither [False,True] and [True,False] as one would expect
and would be computed if arb were a normal top-level function.
This bug is easily explained by MCC's internal translation of
type-classes, which uses the common dictionary approach. The
type-class Arb is replaced by a data type declaration together
with a top-level function for each type class method, i.e,
> data Arb' a = Arb' ({-arb::-} a)
> arb' (Arb' f) = f
The instance declaration is transformed into a top-level
function for each instance method and a function that returns
the instance dictionary for type Bool
> inst'Arb'Bool = Arb' arb'Bool
> arb'Bool = False ? True
The overloaded functions arbP2 and arbL2 receive an additional
argument for each type predicate from their types' contexts, which
are arbP2 :: (Arb a, Arb b) => (a,b) and arbL2 :: Arb a => [a].
> arbP2' da db = (arb' da, arb' db)
> arbL2' da = [arb' da, arb' da]
Observe the essential difference between both functions that
arbL2' receives only a single dictionary, which is used for
both method calls. Now have a careful look at the definition
of inst'Arb'Bool again. Since arb'Bool is a function with no
arguments, Curry's call-time choice semantics means that the
argument of the Arb constructor is evaluated just once per
inst'Arb'Bool call and thus -- unintentionally -- is shared
for both method calls in arbL2'
One can work around this bug by using a different transformation
which forces each argument of a dictionary constructor to become
a function. While there may indeed be good reasons for favoring
such an approach, I believe it is a serious shortcoming of Curry
that the naive dictionary approach cannot be implemented as a
source to source transformation in Curry (at least for the subset
that does not use polymorphic methods). What is lacking here is
the ability to give the user some freedom to specify whether an
expression should be evaluated with call-time choice or with
run-time choice. For instance, one could extend the expression
syntax with
BasicExpr ::= ... | ({ Expr }) | ...
where an expression ({ e }) is evaluated with run-time choice.
E.g., given
dbl x = x + x
main = dbl ({ 0 ? 1 }) =:= 1
the goal main succeeds, which it doesn't with call-time choice.
However, I'm a bit reluctant to such a change because it destroys
the property that a variable in a function always refers to a
single value. Giving up this property apparently has a big impact
on the correctness of some source code transformations (it almost
certainly will break some code in MCC).
A more modest proposal, which would be sufficient to cover the
dictionary transformation, is to restrict run-time choice to
specially marked arguments of data constructors. Just as Haskell
allows marking some data constructor arguments strict by
prefixing the argument type with an exclamation mark, e.g.,
data Complex = Complex !Float !Float
we could mark data constructor arguments as being evaluated with
run-time choice by prefixing the argument types with a question
mark, e.g.,
data Arb a = Arb ?({-arb ::-} a)
This gives a compiler a clear hint on which function arguments are
evaluated with run-time choice and thus must be handled specially.
Thoughts?
Wolfgang
[1]
http://danae.uni-muenster.de/~lux/curry/darcs/type-classes
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Aug 28 2009 - 09:14:28 CEST