Email Gateway (Aug 17 2022 at 14:14): Email Gateway (Aug 17 2022 at 14:14):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Using the repository version of Isabelle, and working in HOL, I find I
can't write
datatype 'a atyp_tag = aword "'a itself" | aptr_tt
It gives me the strangest error too. If I write "option" instead of
"itself" it works. If I write "foo" instead of "itself" it gives me
an error because foo is not a recognised constructor. But with
"itself", I get
*** Illegal type for constant "op =" :: 'a itself => 'a itself => bool
*** At command "datatype".
Should my declaration work?
Michael.
Email Gateway (Aug 17 2022 at 14:14):From: Makarius <makarius@sketis.net>
The error is not as strange as it seems if your ask the type-inference
about this situation:
term "(x::'a itself) = x"
*** Type unification failed: No way to get itself :: type
*** Type error in application: Incompatible operand type
*** Operator: op = :: ??'a => ??'a => bool
*** Operand: x :: 'a itself
Which says that itself is not a HOL type. It can be made one by issueing
an (axiomatic) arity declaration.
Anyway, what is the motivation for using 'a itself within a datatype? Note
that the following version is already polymorphic in the same sense as 'a
itself would make it:
datatype 'a atyp_tag = aword | aptr_tt
term "aword :: bool atyp_tag"
term "aword :: nat atyp_tag"
term "aword :: 'a list atyp_tag"
Incidently, aptr_tt will depend on the type argument in the very same
manner! There is no way to hide this dependency, which would essentially
be an existential type.
Makarius
Last updated: May 03 2024 at 12:27 UTC