Email Gateway (Apr 16 2021 at 19:06): Email Gateway (Apr 16 2021 at 19:06):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
Email Gateway (May 16 2021 at 14:23):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
Email Gateway (May 17 2021 at 13:56):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: Apr 19 2024 at 08:19 UTC