## 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 07 2023 at 20:16 UTC