Stream: Beginner Questions

Topic: ✔ Number literals and explicit type annotations

waynee95 (Feb 15 2022 at 21:39):

I know that number literals are overloaded in Isabelle/HOL and that explicit type annotations are necessary in the following cases.
Most of the time I following the rule of thumb of "if there's an error involving number literals, add explicit type annotations".

But I wanted to understand the errors that arise in the following examples a little bit better:

Doing

value "5 - 10"

will yield the error

Wellsortedness error:
Type 'a not of sort term_of
Cannot derive subsort relation {minus,numeral} < term_of

and doing

value "5 + 10"

will yield the error

Wellsortedness error:
Type 'a not of sort term_of
Cannot derive subsort relation numeral < term_of

I would say that both cases cause an error because a) number literals are overloaded and b) the operations + and - are also overloaded, so Isabelle does not know which functions to apply here.

1. Why does the second example not mention plus in the error message but the first example does mention minus?
2. And what does numeral < term_of mean?

If these questions can be answered by looking into the official docs, any pointers to them would be appreciated.

Mathias Fleury (Feb 16 2022 at 05:54):

class numeral = one + semigroup_add

So numerals always have an addition

Mathias Fleury (Feb 16 2022 at 05:55):

(I just did a control-click on numeral, because I did not remember it either)

Manuel Eberl (Feb 18 2022 at 15:46):

What value does (in its default setting) is to run the code generator on the given term and then execute the generated ML code. The result is an ML value, and that ML value then has to be converted back to a HOL term in order to be displayed. This is done with the term_of type class that contains a function that converts a value of the type to a representation of a HOL term. See the theory HOL.Code_Evaluation for more details.

There are instances of term_of for pretty much anything you should ever encounter, but of course that only works if the term in question is monomorphic. If there are free type variables in there, those do not have the term_of sort (and indeed that approach cannot work even on a conceptual level – how would you execute ML code that contains free variables?).

There are other modes for value that can work with free variables, namely ‘nbe’ (normalisation by evaluation) and ‘simp’ (using the simplifier), but they are much slower.

value [nbe] "3"
value [simp] "3"

With these, you get the result 1 + 1 + 1 :: 'a :: numeral, which is not particularly helpful, but at least it works.

A more useful example would be this:

value [nbe] "replicate 3 x"

Here you get the result [x, x, x] (for some reason, ‘simp’ does not seem to work here).

Manuel Eberl (Feb 18 2022 at 15:49):

Oh and numeral < term_of simply means that the sort numeral subsumes term_of. Your term has the sort numeral, but we also need the term_of class here, and that would only be possible if numeral subsumed term_of. Which it doesn't. (And even if it did, you would then get another error due to the polymorphic nature of the term you are trying to evaluate. Something about free dictionaries being present.)

waynee95 (Feb 18 2022 at 20:48):

@Manuel Eberl @Mathias Fleury Thanks that clarified a lot!

Notification Bot (Feb 18 2022 at 20:48):

waynee95 has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC