## Stream: Beginner Questions

### Topic: "'a itself" documentation

#### Max W. Haslbeck (Jul 21 2021 at 08:47):

Does anyone know where to find documentation on the "itself" type constructor? Why is it needed? Same question for the "dummy" datatype.

#### Manuel Eberl (Jul 21 2021 at 08:55):

When you define something like

``````definition P :: bool where
"P = (∀x y. x = y)"
``````

or

``````definition Q :: bool where
"Q = finite UNIV"
``````

you have an implicit dependency on a type parameter `'a` that does not appear in the type of `P` and `Q`, e.g. the value of `P` and `Q` may depend on which type you pick. Therefore, an artificial dummy parameter of type `'a itself` is introduced to make this explicit, where `'a itself` is a singleton type whose only value is `Pure.type`.

This allows you to write e.g. `P (Pure.type :: nat itself)` to specify that you want the `P` for the type `nat`. A more convenient way to write the values of this singleton type is with the `TYPE` syntax, e.g. `P TYPE(nat)`.

One "real-life" example of this is the dimension of a Euclidean space. Euclidean spaces in Isabelle/HOL are modelled as a type class `euclidean_space`, and then you can define

``````definition dimension :: "'a :: euclidean_space ⇒ nat" where
"dimension = card (Basis :: 'a set)"
``````

and then use this as e.g. `dimension TYPE(real) = 1`, `dimension TYPE(complex) = 2`.

#### Manuel Eberl (Jul 21 2021 at 08:58):

Not sure if or where this is documented.

#### Manuel Eberl (Jul 21 2021 at 08:58):

As for the "dummy" datatype, not sure what you mean by that.

#### Manuel Eberl (Jul 21 2021 at 09:00):

There is `Pure.dummy_pattern`, which I think is not a "proper" term and is used for pattern matching (i.e. the `_` that you can write in `case` expressions, function definitions, etc.)

#### Manuel Eberl (Jul 21 2021 at 09:00):

Not sure if that's what you meant.

#### Manuel Eberl (Jul 21 2021 at 09:01):

Or are you talking about the

``````datatype (plugins only: extraction) "term" = dummy_term
``````

from `HOL.Code_Evaluation`?

#### Max W. Haslbeck (Jul 21 2021 at 09:03):

Manuel Eberl said:

Or are you talking about the

``````datatype (plugins only: extraction) "term" = dummy_term
``````

from `HOL.Code_Evaluation`?

No, just the type

``````term "x :: dummy"
``````

#### Lukas Stevens (Jul 21 2021 at 09:09):

If that is the same as `Term.dummyT`, then it is often used to leave type holes in a term and then fill them with `Syntax.check_term`.

#### Max W. Haslbeck (Jul 21 2021 at 10:02):

@Manuel Eberl

Thanks.

Manuel Eberl said:

Not sure if or where this is documented.

I could not find an explanation for it, neither in the Isabelle sources nor via google. Isabelle is probably really hard to use if you don't share an office with an Isabelle elder :stuck_out_tongue:

#### Manuel Eberl (Jul 21 2021 at 10:08):

Found it! §2.3.2 of the Isabelle/Isar implementation manual.

#### Manuel Eberl (Jul 21 2021 at 10:09):

Perhaps the explanation is a bit less, uh, easy to understand than the one I wrote above.

#### Manuel Eberl (Jul 21 2021 at 10:09):

I'm not even sure where I learnt about this; I think I just encountered it at some point and then it seemed kind of obvious what it was.

#### Manuel Eberl (Jul 21 2021 at 10:09):

But yeah I'm sure it can be confusing at first.

Last updated: Jul 15 2022 at 23:21 UTC