- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Michael Hanus <hanus_at_informatik.rwth-aachen.de>

Date: Thu, 14 Jan 1999 14:58:25 +0100

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

Date: Thu, 14 Jan 1999 14:58:25 +0100

Dear Wolfgang,

thanks for your immediate feedback.

You wrote:

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.

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
: Sa Okt 01 2022 - 07:15:04 CEST
*