Stream: Beginner Questions

Topic: Numeric type conversion


view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Jakub Kądziołka (Feb 25 2021 at 14:44):

you could also use the name rat_of_nat

view this post on Zulip Max Nowak (Feb 25 2021 at 14:44):

Ahhhh, TIL you can ctrl-hover!

view this post on Zulip Jakub Kądziołka (Feb 25 2021 at 14:44):

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

view this post on Zulip Max Nowak (Feb 25 2021 at 14:46):

Oh yeah that simplifies it further, thank you :)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Max Nowak (Feb 25 2021 at 14:54):

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

view this post on Zulip Manuel Eberl (Feb 25 2021 at 23:50):

Yeah you basically almost never want that.

view this post on Zulip 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: Sep 25 2021 at 08:21 UTC