- 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: Fri, 23 Oct 1998 17:11:44 +0200

[I changed the subject since this email concerns only one topic

of the previous thread.]

I'd like to discuss the necessity to allow existential quantifiers

also for arbitrary expressions a little bit further.

Herbert Kuchen wrote:

*> Michael Hanus wrote:
*

*> > This restriction is due to semantical reasons. Since "let...free"
*

*> > corresponds to existential quantification, it is natural to
*

*> > have it in constraints, but I do not know what is the semantics
*

*> > of a term like "there exists an x such that x+2".
*

*>
*

*> I agree that forcing exp to be of type Constraint is probably
*

*> too restrictive. It might be interesting to allow
*

*>
*

*> let ... free in exp
*

*>
*

*> also with other types of exp, e.g. in
*

*>
*

*> let x free in parent x
*

*>
*

*> parent Bill = Maud
*

*> parent Maud = Jack
*

*>
*

*> it could be used to generate possible values.
*

Here I am interested to see why you need the existential quantifier

exact at this level. If "parent x" occurs only in a condition,

you could raise the declaration of x to the entire condition, e.g.,

lhs | let x free in ...parent x... = rhs

If "parent x" occurs in some right-hand side, you can also declare

x at the top level by

lhs | c = ...parent x... where x free

The same is true for Wolfang's example:

Wolfgang Lux wrote:

*> I don't see it either for that term, but what about:
*

*>
*

*> let xs = [1,2,3] in let ys, y in append ys y =:= xs => y
*

*>
*

*> where append is the flexible version of (++) and => would be defined as
*

*>
*

*> c => x | c == succeeded = x
*

If the big let expression is a right-hand side of some rule,

you can rewrite it as:

lhs = let xs = [1,2,3] in append ys y =:= xs => y where ys,y free

So, I'd like to see an example where the existential quantification

at exactly the scope of some non-constraint expression is really

necessary. Otherwise, I am in favor to omit this possibility

due to two reasons:

1. The declarative meaning of existential quantifiers around

arbitrary terms is unclear (at least for me).

2. Such a restriction can allow the compiler to detect more

programming errors (in particular, type errors).

Best regards,

Michael

Received on Fr Okt 23 1998 - 18:15:00 CEST

Date: Fri, 23 Oct 1998 17:11:44 +0200

[I changed the subject since this email concerns only one topic

of the previous thread.]

I'd like to discuss the necessity to allow existential quantifiers

also for arbitrary expressions a little bit further.

Herbert Kuchen wrote:

Here I am interested to see why you need the existential quantifier

exact at this level. If "parent x" occurs only in a condition,

you could raise the declaration of x to the entire condition, e.g.,

lhs | let x free in ...parent x... = rhs

If "parent x" occurs in some right-hand side, you can also declare

x at the top level by

lhs | c = ...parent x... where x free

The same is true for Wolfang's example:

Wolfgang Lux wrote:

If the big let expression is a right-hand side of some rule,

you can rewrite it as:

lhs = let xs = [1,2,3] in append ys y =:= xs => y where ys,y free

So, I'd like to see an example where the existential quantification

at exactly the scope of some non-constraint expression is really

necessary. Otherwise, I am in favor to omit this possibility

due to two reasons:

1. The declarative meaning of existential quantifiers around

arbitrary terms is unclear (at least for me).

2. Such a restriction can allow the compiler to detect more

programming errors (in particular, type errors).

Best regards,

Michael

Received on Fr Okt 23 1998 - 18:15:00 CEST

*
This archive was generated by hypermail 2.3.0
: So Jan 26 2020 - 07:15:06 CET
*