Re: [isabelle] Problems with multiple patterns in simproc_setup

This question is not specific to Isabelle but overlaps with functional programming in general and should have an abstract answer. As I mentioned, the "fun" command typechecks equations separately, and not because this is Isabelle but because this is the standard in functional programming (for good reasons). Thus I had concluded that simproc_setup should behave the same. But the issue is more subtle. The simproc patterns do not guard different equations but one and the same object, the function definition. Hence they are akin to "disjunctive patterns" in OCaml. Type inference for disjunctive patterns is simultaneous, again for good reasons, because the variables are used in the single body that follows the patterns. But patterns in simprocs are again slightly different in that the variables are never used and thus there is no need for simultaneous type inference.

My conclusion is that simproc_patterns are different enough from normal and from disjunctive patterns that there is no abstract argument that they should behave like either.

In the absence of a strong abstract argument, I would indeed leave things as they are.


On 25/10/2019 11:58, Makarius wrote:
On 25/10/2019 11:45, Manuel Eberl wrote:

I don't really undestand what you're trying to say.

The question at hand is: Is the behaviour of simproc_setup here (type
checking all the different patterns simultaneously, in the same context)
what it is supposed to do or not?

The default answer: by default the behaviour of the system is correct
and as intended. There can be nonetheless situations of user confusion:
the system provides tools to work that out, notably for type-inference.

'simproc_setup' might be an odd corner case from the past -- I can't say
on the spot, but 10min of inspecting of the sources and the history
don't show any irregularities so far.

Generally, it is a bad idea to change established behaviour on the spot,
just because the true reasons for it are forgotten, or take a long time
to investigate. The Isabelle jargon for that is "brownian motion":
something could be done like this or like that, and there is no clear
indication for either side. Adhoc changes would make it oscilate back
and forth over time, and break other applications for no particular reason.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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