Re: Proposal: Relaxing restrictions in Curry

From: Sergio Antoy <antoy_at_cs.pdx.edu>
Date: Tue, 02 Nov 2004 08:58:14 -0800

Michael writes:

> I'd like to propose to relax two restrictions in the definition
> of Curry which seem to me unnecessarily strong.
>
> The first one is related to the introduction of free variables.
> The current language definition (Curry Report, C.3) requires
> that in an expression of the form
>
> let x free in e
>
> e must be of type "Success" (1).
>
> On the one hand, this seems justified by the fact that existential
> quantification is reasonable for constraints only.

I agree with your proposal, because I somewhat disagree with the
justification. The justification would hold for a construct of
the kind

    exists x such that e

In this case, e should be a constraint and, noticeably, the
expression should be boolean.

> On the other hand, this demands for some nasty transformations
> if one needs local variables in a non-constraint scope. For
> instance, the (currently illegal) definition
>
> f x = \y -> let z free in g x y z -- (2)
>
> (where (g x y z) is not of type Success) can be transformed
> in the valid Curry program
>
> f x = g' x
> g' x y = g x y z where z free
>
> The transformation can be avoided by introducing a
> "generate-free-variable" function (actually, this is the
> solution which I often use):
>
> f x = \y -> g x y any
> any = z where z free
>
> Both solutions are less readable than (2). Furthermore,
> the alternatives demonstrate that restriction (1) is not
> really necessary. In particular, if one defines a type
> isomorphic to Success, the restriction becomes questionable.
>
> Thus, I propose to drop the restriction (2).
> This would also make the application of let and where
> "more equivalent".

I agree.

> The second restriction concerns the sequential conjunction
> of constraints, which is currently defined as
>
> (&>) :: Success -> Success -> Success
> c &> x | c = x
>
> in the prelude.
>
> We have a number of applications where we want to put constraints
> during a functional evaluation. Until now, we have defined for this
> purpose a "guard" function that takes a constraint and an expression as
> input and is the identity on the second argument provided that the
> constraint is satisfied. Thus, it is defined as
>
> guard :: Success -> a -> a
> guard c x | c = x
>
> so that you can use it as in (guard (x=:=1) (2+x)).
> Now, you see that the definition of the guard function is
> identical to (&>) apart from the different types.
> Since such a guard function is quite useful, I propose
> to generalize the type of (&>) to
>
> (&>) :: Success -> a -> a
>
> so that it is a general function to establish new constraints
> during arbitrary computations.
>
>
> Since both proposals have no influence on existing programs but
> allow more valid Curry programs, I see no problem in them.
> However, maybe somebody sees some problem?

I agree with this too. Wouldn't the definition of &> be
simpler as follows

   (&>) :: Success -> a -> a
   Success &> x = x

Sergio

_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Wed Nov 03 2004 - 08:47:40 CET

This archive was generated by hypermail 2.3.0 : Mon Sep 23 2019 - 07:15:05 CEST