Dear Wolfgang,
thanks for your immediate feedback.
You wrote:
> > - Section 4.2: Definition of well-typed programs added by means of
> > typing rules.
>
> The typing rule for let without existentially quantified variables is
> missing and recursion is missing. (The explanations following the
> typing rules suggest that you intend polymorphic recursion, i.e.
> Milner-Mycroft typability.)
You are right, polymorphic recursion is allowed if all types
are explicitly provided (similarly to Haskell, I guess, but
I couldn't find a precise definition of a well-typed program
in the Haskell report). However, if the types must be inferred,
then it depends on the type inferencer which types can be
inferred (usually, polymorphic recursion is then not allowed,
but one can do better, see, for instance, Mercury).
Concerning the let, I omitted it since the let and local
functions also do not occur in the definition of the operational
semantics. Thus, I implicitly assume (but I take your point,
this must be explicitly stated somewhere in the report)
that the kernel program (for which well-typedness and the
semantics is defined) has been lambda-lifted so that it does not contain
local declarations.
> There is another point in the report, which is was wondering about for
> some time. In section 2.6 the report says that "Curry delays
> application of unknown functions until the function becomes
> known". However I don't see how this should ever happen. The only way
> how an uninstantiated variable might become bound is either via
> pattern matching or by unification in an equational
> constraint. Neither is possible for functional values, however,
> because they are not data terms. Am I overlooking something here?
You are right again, with the current definition of equational
constraints as unifiability of data terms, uninstantiated
higher-order variables can never be bound. This remark is
more related to possible extensions of Curry (again, I should
better make this point clear in the report). For instance, an
implementation may guess user-defined functions for uninstantiated
higher-order variables. Since this results in a large search space,
I am in favor of another approach: consider partial applications
of functions as constructor terms, e.g., the partial application
"(+) 1" is considered as a constructor term "plus1 1" where
"plus1" is a unary constructor. Thus, the definition of
an n-ary function implies the implicit declaration of n-1
constructors. Then, you can instantiate a free variable f
of type "Int->Int" by solving the equational constraint
"f =:= (+) 1". The implementation of this is very simple
(it is already done in our TasteCurry system) and it has
some nice applications, although the declarative semantics
is not so clear.
Best regards,
Michael
Received on Do Jan 14 1999 - 15:02:00 CET
This archive was generated by hypermail 2.3.0
: Do Feb 01 2024 - 07:15:05 CET