Re: [isabelle] Confusing behavior of a paired set comprehension



On Thu, Apr 5, 2012 at 12:27 PM, Tjark Weber <webertj at in.tum.de> wrote:
> On Thu, 2012-04-05 at 11:25 +0200, Brian Huffman wrote:
>> Isabelle's treatment of bound variables is perfectly consistent with
>> mainstream functional programming languages like Haskell or ML:
>> Function abstractions may shadow existing names.
>>
>> (ghci)
>> Prelude> :t \x -> \x -> x
>> \x -> \x -> x :: t -> t1 -> t1
>>
>> (polyml)
>> fn x => fn x => x
>> val it = fn: 'a -> 'b -> 'b
>
> True, but the original example was "ident S = {(x,x) . x \in S}". Hence
> I believe the following behavior to be more relevant:
>
> (polyml)
>> fn (x,x) => x;
> Error-x has already been bound in this match Found near fn (x, x) => x
> Static Errors

Good point.

So while "Collect (split (%x x. x \<in> S))" is clearly valid input,
the status of the equivalent-according-to-the-parser "{(x, x). x \<in>
S}" is not so clear.

It might be possible to set up an ML parse translation for tuple
abstractions (see section "Tuple syntax" in Product_Type.thy for how
things are implemented now). The parse translation could produce a
syntax error if any variable names are repeated.

I'm not sure whether it would be worth the trouble to implement it,
though, unless more people ask for it.

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.