Michael Hanus <hanus_at_informatik.rwth-aachen.de> wrote,
> [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).
I agree with Michael, as existential quantifiers in
arbitrary expressions destroy referential transparency:
let fv = let x free in x
in
foo fv & bar fv
^
|or however you write conjunction in Curry
is different from
foo (let x free in x) & bar (let x free in x)
This is exactly the problem that occured in Id, which allows
to create I-structures in arbitrary expressions -- and it is
exactly the reason why this is not allowed in Goffin aka
Distributed Haskell <
http://www.score.is.tsukuba.ac.jp/~chak/goffin/>.
Cheers,
Manuel
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
Manuel M. T. CHAKRAVARTY chak_at_score.is.tsukuba.ac.jp
University of Tsukuba, Japan
http://www.score.is.tsukuba.ac.jp/~chak/
SCORE Lab. Inst. of Information Sciences and Electronics
Received on Mo Okt 26 1998 - 08:33:00 CET