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: Dec 21 2024 at 16:20 UTC