Re: [isabelle] Isabelle2016-RC0 - overloaded datatypes



On Sun, 3 Jan 2016, C. Diekmann wrote:

Is typedef (overloaded) dangerous?

The NEWS file says "This provides extra robustness in theory construction."

The isar-ref manual says:

  Recent clarification of overloading in the HOL logic proper @{cite
  "Kuncar-Popescu:2015"} demonstrates how the dissimilar concepts of
  constant definitions versus type definitions may be understood
  uniformly. This requires an interpretation of Isabelle/HOL that
  substantially reforms the set-theoretic model of A. Pitts @{cite
  "pitts93"}, by taking a schematic view on polymorphism and interpreting
  only ground types in the set-theoretic sense of HOL88. Moreover,
  type-constructors may be explicitly overloaded, e.g.\ by making the
  subset depend on type-class parameters (cf.\ \secref{sec:class}). This
  is semantically like a dependent type: the meaning relies on the
  operations provided by different type-class instances.

So it goes beyond the classic understanding of the HOL logic, i.e. the one of HOL4 or HOL-Light.

There is nothing wrong with that. The extra option merely makes clear, where the transition happens, for applications that need extreme forms of reliability (e.g. by translation to OpenTheory or other HOL systems).


	Makarius





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