Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
>> "in/out" are semantically very symmetric. I invented "xtor" out of sheer desperation and would happily trade it against "inout" or "io" or even "thru".
I don't have a strong position about these names. Just a historic note: These were initially called "fold" and "unfold,"
which I still think are the most accurate names. Of course, they clash with traditional combinator names, and this is why we renounced them.
All the best,
From: Jasmin Blanchette [mailto:jasmin.blanchette at inria.fr]
Sent: 17 November 2015 15:16
To: Dmitriy Traytel
Cc: Manuel Eberl; cl-isabelle-users at lists.cam.ac.uk; Andrei Popescu
Subject: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
> I am against the renaming. Note that âinâ is a keyword in ML and you would need to start decorating the identifiers in the ML code with âxâ, âââ or â0â.
We have clashes with many other names, e.g. "rec" (a keyword, or a recursor), "map", "fold" (ML functions one does not want to shadow), even "in"... (Grep "recx", "mapx", "foldx", "inx".) Such clashes, and their crude fix with an "x", are not pretty, but they are a reasonable price to pay for having the right names at the Isar level.
But there is in fact a possible confusion at the ML level, which is much worse than the inelegant "inx": "in" is already used in the code for set membership (\<in>), e.g.
val inx = mk_in Asets sets T;
So maybe statu quo is best for now.
> Also in/out are much less symmetric than ctor/dtor. We have actual code that is parametric in the view (there the name xtor is used).
"in/out" are semantically very symmetric. I invented "xtor" out of sheer desperation and would happily trade it against "inout" or "io" or even "thru".
This archive was generated by a fusion of
Pipermail (Mailman edition) and