Re: [isabelle] the itself type constructor
On Wed, 15 Mar 2006, Michael Norrish wrote:
> 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.
> *** Illegal type for constant "op =" :: 'a itself => 'a itself => bool
> *** At command "datatype".
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and