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 MHonArc.