Michael Hanus wrote:
> Wolfgang Lux wrote:
> > First I do not see the reason why you want to restrict the expression
> > inside a
> >
> > let ... free in exp
> >
> > to the type of constraint.
>
> 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 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
I think there is an obvious interpretation for that expression, viz. 3,
but this is no longer legal because the whole expression is not of type
constraint.
Regards
Wolfgang
--
Wolfgang Lux Phone: +49-251-83-38263
Institut fuer Wirtschaftinformatik FAX: +49-251-83-38259
Universitaet Muenster Email: lux_at_helios.uni-muenster.de
Received on Fr Okt 23 1998 - 14:45:00 CEST