Am 28/05/2013 13:34, schrieb Lawrence Paulson: > Historical note: when the original high-order unification code was written, > there was no user-level polymorphism. If my memory is correct, the TVar > constructor did not even exist. Polymorphism was only used for type inference > in terms.
correct. i added that part of the code in about 1990. of course i never proved anything about it. tobias > Any idea to unify types while at the same time identifying previously > distinct variables needs to be scrutinised with very great care. Better to > have an exception raised than to have unsound reasoning. > Larry > > On 28 May 2013, at 10:36, Makarius <makar...@sketis.net> wrote: > >> On Tue, 28 May 2013, Stefan Berghofer wrote: >> >>> Types as well as terms are unified. The outermost functions assume >>> the terms to be unified already have the same type. In resolution, >>> this is assured because both have type "prop". >>> >>> So it is the expected behaviour that the unification functions cannot cope >>> with the above example, since it does not satisfy this precondition. >> >> I am getting a bit uneasy about that for two reasons: >> >> (1) There might be really something wrong in Thm.bicompose_aux or >> Thm.assumption that fails to "assure" such implicit assumptions of >> unify.ML. >> >> (2) The notorious problem of "hidden polymorphism", i.e. extra >> generality of types that is not seen on the surface, and thus needs >> to be treated while walking into the term structure. >> >> The second point might be relevant for Pattern.match as well: it does one >> typ_match thy on the outside, and then only for Free/Const/Bound, but not >> for Var. >> >> So we seem to be back at the implicit global assumption that the types of >> Vars happen to work out "magically", without further ado. There used to be >> that comment in really ancient Isabelle versions, before Stefan made an >> explicit check that it does not go wrong, but here it did go wrong. >> >> >> Makarius >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
