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

From: Manuel M. T. Chakravarty <chak_at_is.tsukuba.ac.jp>

Date: Mon, 26 Oct 1998 16:31:49 +0900

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 Mon Oct 26 1998 - 08:33:00 CET

Date: Mon, 26 Oct 1998 16:31:49 +0900

Michael Hanus <hanus_at_informatik.rwth-aachen.de> wrote,

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 Mon Oct 26 1998 - 08:33:00 CET

*
This archive was generated by hypermail 2.3.0
: Mon Sep 16 2019 - 07:15:04 CEST
*