Hello Michael,
> - 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.)
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?
Regards
Wolfgang
--
Wolfgang Lux Phone: +49-251-83-38263
Institut fuer Wirtschaftinformatik FAX: +49-251-83-38259
Universitaet Muenster Email: lux_at_helios.uni-muenster.de
Received on Do Jan 14 1999 - 12:05:00 CET