Re: [isabelle] read/print consistency?

Brian Huffman wrote:
Similar situations can also arise even when "show types" is on. This happens
often if you use functions like "of_nat :: nat => 'a::semiring_1" or "of_int
:: int => 'a::ring_1" that are polymorphic in the return type. For example,
if you type "thm of_int_less_iff", you get:

"(of_int (?w::int) < of_int (?z::int)) = (?w < ?z)"

Even with "show sorts" enabled, you get no indication that this lemma
applies only to class "ordered_idom".

I thought a bit about this recently when fiddling with HOL4's
pretty-printer.  In the absence of user code getting in the way, I
believe you can do a reasonable job with the following algorithm:

  * all variables get type annotations
  * terms with constants at their head, and where the constant "might
    be polymorphic" (see below) get their types printed as well if the
    constant is applied to n arguments and there are type variables
    that occur after the nth argument that don't appear in the first

    For example, K is a constant with type : 'a -> 'b -> 'a.  If the
    term is

      K x

    Then the term K x will get a type annotation because the 'b of the
    term's type doesn't occur among the arguments that are present
    (the x).  K itself will not get an annotation.

    Nil, the empty list constant, would always get a type annotation
    in this scheme.  In Isabelle, so too would constants like zero.
    This is because they are never applied to any arguments, so their
    polymorphism would always be left dangling.

The "might be polymorphic" test has to do with HOL4's overloading
system.  Terms that are known to print with a form that can in turn
parse back to multiple possible terms are considered polymorphic, even
though they are not in fact polymorphic at all.

With user code about (users can dynamically update the parser/printer
systems with their own code in both Isabelle and HOL4), all bets are
off of course.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.