Existential quantification in expressions

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