From: Mikhail Mandrykin <mandrykin@ispras.ru>

Hello!

I've recently noticed an unexpected thing about the quite common type

proxy ‹Pure.type›. My understanding is that it's convenient to use for

defining type-dependent polymorphic constants, including type class

members with no normal parameters (say, some abstract number ascribed to

a type such as its assumed physical size). The thing is, I can't find

any exhaustiveness theorem related to the constant ‹Pure.type› and its

type ‹'a itself› e.g. "x ≡ Pure.type" or "(x ≡ Pure.type ⟹ P) ⟹ P".

Analogous lemma exists for the unit type in HOL and the type itself

looks similar enough to Haskell's Proxy datatype with a single Proxy

constructor (which should imply exhaustiveness as with other datatypes).

The non-exhaustiveness of ‹'a itself› causes a problem when one

accidentally defines some class axiom with an extra term variable ‹t ::

'a itself› in place of the ‹Pure.type› constant, sometimes the axiom

then cannot be proved if the corresponding instance definition is

specified using the ‹Pure.type› constant, since the definition in the

goal can be neither unfolded nor refined using the exhaustiveness

rewrite/elimination rule. Is this situation intentional due to some

logical limitations I'm not aware of? Of course ‹Pure.type› is part of

Pure and not even HOL, so it's not technically related to datatypes, but

is such exhaustiveness axiom incompatible with something important?

Regards, Mikhail

From: Makarius <makarius@sketis.net>

There is indeed no logical specification of 'a itself as "polymorphic unit

type" in Pure. It could be added in principle, but it is not required:

de-facto the only term used in specifications should be Pure.type.

If there is an "accident" in user-space theory libraries somewhere, why not

repair it where it actually happened?

Makarius

From: Mikhail Mandrykin <mandrykin@ispras.ru>

Makarius писал 2021-05-16 17:23:

de-facto the only term used in specifications should be Pure.type.

If only the ‹Pure.type› form syntactically occurs in terms then there's

indeed no issue. I initially got confused because of the quite

straightforward analogy with types like Proxy and thought just a term ‹t

:: 'a itself› can also be given e.g. in definitions like ‹rep_length t

≡ length (layout_of t)› for "t :: 'a itself" and therefore tried to make

the class axioms more general to account for such definitions, but still

missed some cases. So without extending Pure the correct approach is

just that such "t" shorthands should not even occur

Mikhail

Last updated: Jan 25 2022 at 01:11 UTC