Stream: Beginner Questions

Topic: ✔ "no type arity" in error message

waynee95 (Apr 21 2022 at 15:08):

It makes sense that this obviously throws an error but I am not sure what the error message concretely means.

value "3 :: bool"

will yield the error message

Type unification failed: No type arity bool :: numeral

Failed to meet type constraint:

Term:  3 :: ??'a
Type:  bool

What does "no type arity" mean here exactly?

Also what is the best way to browse Isabelle source files? When I Ctrl-click on things in Isabelle/jEdit it will bring me to the source file of that thing but it's all red and I cannot further click on things. This makes it really hard to navigate through source files. And the library webpage only supports a small set of "clickable things".

Manuel Eberl (Apr 21 2022 at 15:48):

It basically means that the numeral type class has no instance for the bool type. The numeral type class is what you need in order to write numeric constants like 2, 3, etc.

Any numeric literal for a natural number greater than 1 desugars to something of the form numeral (bit1 (bit0 (bit1 One))), and the numeral function here requires the numeral type class. An instance for this typically exists for any semiring (but not for Booleans since it doesn't make that much sense there).

Manuel Eberl (Apr 21 2022 at 15:50):

As for browsing source files, yes, this is a known limitation. If you open a theory file in Isabelle/jEdit that is part of the current heap image, there you cannot Ctrl+click around in it. One workaround is to start with the Pure image instead of the HOL image, e.g. by running isabelle jedit -l Pure, but then you have to wait for the entire HOL library to build inside Isabelle/jEdit first, which will take a few minutes (or more, depending on your hardware).

waynee95 (Apr 21 2022 at 16:12):

@Manuel Eberl Yeah that it means numerical type class has no instance for bool is what I already imagined. I am not foreign to type classes. I was just a bit confused about the word choice "no type arity".

Thanks for that suggestion, I will try that.

Manuel Eberl (Apr 21 2022 at 16:13):

waynee95 said:

Manuel Eberl Yeah that it means numerical type class has no instance for bool is what I already imagined. I am not foreign to type classes. I was just a bit confused about the word choice "no type arity".

Thanks for that suggestion, I will try that.

Not sure where that terminology comes from. But I imagine that it has something to do with sorts.

Manuel Eberl (Apr 21 2022 at 16:14):

Types can have different sorts associated to them, and type classes are implemented through sorts.

Notification Bot (Apr 21 2022 at 16:14):

waynee95 has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC