Re: [isabelle] Problems with multiple patterns in simproc_setup



On 25/10/2019 12:31, Tobias Nipkow wrote:
> 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.

These are good observations, and hint at various possibilities of the
design space (also going back to approx. 2007).

The implementation in terms of existing Isabelle concepts is another
issue: when we started to support separate variable scopes as in
'function' or 'inductive', it was a genuine feature addition that
required approx. 10 years to get properly implemented. As a consequence
of recent consolidation, the PIDE markup informs the user about the
difference: blue variables for a simultaneous global scope (e.g.
'simproc_setup') vs. green variables for local bindings with independent
type inference (e.g. in 'function'). Note that "blue" could also mean
"legacy variable treatment, without proper scoping". Moreover, blue
variables still lack the scope-group markup for PIDE.

Generally, I find our situation of scopes and type inference less
confusing than e.g. in Scala. In any case, when I use one of these
rather complex languages (Scala, TypeScript, Haskell etc.) I always rely
on the IDE to tell me what has been worked out by the system.


> 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.

I do agree with the conclusion.


	Makarius




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