Stream: Beginner Questions

Topic: Numeric type conversion

Max Nowak (Feb 25 2021 at 14:29):

I am trying to write a quick abbreviation, as follows:

abbreviation threshold :: "nat ⇒ rat"  where
"threshold n ≡ of_int (floor ((of_nat n) / 2) + 1)"

However, that already gives me a warning which I don't understand: Additional type variable(s) in specification of "threshold": 'a, since I have no type variables in that abbreviation?

Then, using that abbreviation...

definition my_def :: "bool" where
"my_def ≡ ∀p. 123 > threshold (length p)"

...I get an error:

Max Nowak (Feb 25 2021 at 14:30):

Operator:  threshold :: ??'a itself ⇒ nat ⇒ rat
Operand:   length p :: nat

And I don't understand where ??'a itself comes from.

Jakub Kądziołka (Feb 25 2021 at 14:41):

The warning tells you that some constants in your abbreviation can have multiple types, so they've been assigned a type variable

Jakub Kądziołka (Feb 25 2021 at 14:43):

If you ctrl+hover over floor, of_nat and 2, you'll see that their inferred types are 'a => int, nat => 'a and 'a respectively

Max Nowak (Feb 25 2021 at 14:43):

Ah, yeah disambiguating with (of_nat n)::rat helped. Glad the solution was so simple, thank you!

Jakub Kądziołka (Feb 25 2021 at 14:44):

you could also use the name rat_of_nat

Max Nowak (Feb 25 2021 at 14:44):

Ahhhh, TIL you can ctrl-hover!

Jakub Kądziołka (Feb 25 2021 at 14:44):

there's also n div 2, which is floored divison

Max Nowak (Feb 25 2021 at 14:46):

Oh yeah that simplifies it further, thank you :)

Jakub Kądziołka (Feb 25 2021 at 14:47):

When you do want to use floor, there's the syntax ⌊a⌋ (which you can type with [. .] and selecting between floor and ceiling in the autocompletion menu)

Jakub Kądziołka (Feb 25 2021 at 14:53):

The reason your threshold abbreviation got a 'a itself parameter is that the actual value of the abbreviation depends on which type you choose. You can think of 'a itself as a witness that tells you which type to actually use

Jakub Kądziołka (Feb 25 2021 at 14:53):

so, if you actually wanted to parametrize your threshold by what type is used for intermediate computation, you could invoke it with threshold TYPE(rat) (length p)

Max Nowak (Feb 25 2021 at 14:54):

Huh, that is neat actually, but not necessary for what I'm doing.

Manuel Eberl (Feb 25 2021 at 23:50):

Yeah you basically almost never want that.

Manuel Eberl (Feb 25 2021 at 23:51):

'a itself is a singleton type, just so that you've heard the term. (They are also used in functional programming)

Last updated: Dec 21 2024 at 16:20 UTC