Dominique Unruh wrote:
>> This answers the question why there is no harm in removing sorts (at
>> least from constants and definitions, not of course from class
>> axioms). I am still wondering what the reasons for doing so are. At a
>> first glance, at least, it would seem more natural to me if the
>> constants and definitional axioms would have sort annotation. Also,
>> the argument given by Florian ("definitions not only *can* ignore sort
>> constraints, but *must* ignore sort constraints, otherwise this
>> unfolding would not be possible in all situations.") does not convince
>> me, because since in a normal proof, we would never even have an
>> occurrence of a constant with the "wrong" sorts, so there is no need
>> for a definition that allows unfolding in such situations.I also think that the "unfolding principle" would still work with class constraints, under the assumption that the terms are well-sorted, which would then also have to be checked on the low level... On the other hand, the fact that definitions can be class-less shows that the two concepts are mostly orthogonal, which I guess does simplify the kernel a little bit. Making the other axioms also class-less (possibly with internalized OFCLASS constraints) would make things more regular... As Andy mentioned, there will be some changes in the management of type classes in the near future, but a few problems need to be sorted out first. With the situation as in Isabelle 2009 or 2009-1, it is probably very hard to translate proofs that involve type classes, since the Thm.class_triv and Thm.unconstrainT inference rules do not produce proper proof terms. The missing information can probably be reconstructed, but this is not fun at all. >> Also, as >> mentioned by Andreas, stripping sort constraints may make it much >> harder to interpret Isabelle/HOL in other logics (be it ZF as in >> Andreas case, or my experiments of translating Isabelle/HOL to Coq). Our hope is to be able to eliminate classes from proof terms (and, in a separate step, also from definitions) entirely, which makes such translations much simpler again. Alex
