[isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading

Christian Sternagel c.sternagel at gmail.com
Mon Nov 24 12:35:39 CET 2014 

Thanks again Dmitriy,

it seems that my "fix" was too quick. Since sending my email yesterday I 
worried already whether doing unification inside adhoc_overloading.ML is 
such a good idea (since the unifier might inject schematic type 
variables stemming from the internal generic theory data of adhoc 
overloading into the ongoing check-phase). Apparently it isn't.

Is there a way to turn arbitrary schematic type variables into ones that 
will not cause problems during type-inference? If so, it might be better 
to just check for unifiability and then inject a variant "v" with its 
most general type but where "polymorphic" variables are made known to 
the context.

I'm mostly guessing here. Maybe somebody with deeper knowledge of the 
system could comment whether this would be feasible (and also the right 
way to go).

cheers

chris

On 11/24/2014 09:03 AM, Dmitriy Traytel wrote:
> Cf. http://isabelle.in.tum.de/testboard/Isabelle/rev/fd70d029af7e
>
> Dmitriy
>
> On 23.11.2014 21:20, Christian Sternagel wrote:
>> *Moved from isabelle-users*
>>
>> Thanks for the crucial hint Dmitriy!
>>
>> Coming back to the original issue of Andreas, some explanation might
>> be in order.
>>
>> What we did until now in adhoc_overloading.ML (more precisely, the
>> function "insert_variants") was to check for a given constant "c" of
>> type "T" whether there is a registered variant "v" whose type unifies
>> with "T". If so, "v" was inserted (but with all type-annotations
>> "flattened" to "dummyT"). After that we just hoped that type-inference
>> would do the trick. Apparently this worked quite well in many
>> situations (or maybe there are just not that many users of
>> "adhoc_overloading" ;)).
>>
>> Be that as it may. In Andreas' example this "flattening" of types
>> leads to somewhat unexpected results. Funnily (or maybe it was to be
>> expected but I don't know the details) everything worked out in
>> top-level thoeries. Somehow types are more polymorphic there (even
>> though HOL is not polymorphic at all ;)). With notepad and a fixed
>> type "'b" the problem occurred (and I guess the same would happen with
>> locales).
>>
>> (I'm not sure whether the TYPE_MATCH exception, which is not raised
>> inside adhoc_overloading.ML but caused by its result, is the best
>> problem-indicator for users here. Maybe there is also space for
>> improvement elsewhere. Comments?)
>>
>> Anyway, attached is the following series of patches (to be applied in
>> this order):
>>
>> delete - fixes a typo
>> drop_semicolons - drops semicolons
>> inst_unifier - uses the obtained unifier to instantiate the type of "v"
>> tune - misc tuning
>>
>> With those applied (the important one is "inst_unifier")
>> "insert_variants" does the following. For a given constant "c" of type
>> "T", check whether there is a variant "v" of type T' such that T and
>> T' unify. If so, apply the obtained type-unifier to "v" and insert the
>> result instead of "c".
>>
>> I hope this resolves your problem Andreas.
>>
>> I tested the change on one of my local files that make heavy use of
>> adhoc overloading. Maybe someone could have a look, push the changes
>> to a test server, and push them to the main repo if everything is fine?
>>
>> cheers
>>
>> chris
>>
>> On 11/23/2014 11:42 AM, Dmitriy Traytel wrote:
>>> Hi Christian,
>>>
>>> just a few weeks ago, I learned that Envir.subst_term_types is indeed
>>> the wrong function when substituting with a unifier (instead it is
>>> intended for matchers).
>>>
>>> The right functions for unifiers in envir.ML are the ones prefixed with
>>> "norm".
>>>
>>> Hope that helps,
>>> Dmitriy
>>>
>>> On 22.11.2014 21:02, Christian Sternagel wrote:
>>>> I'm currently a bit confused by the result of "Sign.typ_unify" (or
>>>> rather the result of applying the corresponding "unifier"). So maybe
>>>> the problem stems from my ignorance w.r.t. to its intended result.
>>>>
>>>> After applying the attached "debug" patch for the following
>>>>
>>>>   consts pure :: "'a ⇒ 'b"
>>>>
>>>>   definition pure_stream :: "'a ⇒ 'a stream"
>>>>   where "pure_stream = sconst"
>>>>
>>>>   adhoc_overloading pure pure_stream
>>>>
>>>>   consts ap_stream :: "('a ⇒ 'b) stream ⇒ 'a stream ⇒ 'b stream"
>>>> (infixl "◇" 70)
>>>>   consts S_stream :: "(('a ⇒ 'b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c) stream"
>>>>
>>>>   declare [[show_variants]]
>>>>
>>>>   term "pure id :: ('b ⇒ 'b) stream"
>>>>
>>>> we obtain the output
>>>>
>>>> oconst type: (??'a ⇒ ??'a) ⇒ ('b ⇒ 'b) stream
>>>> variant type: ?'a ⇒ ?'a stream
>>>> ("unifier:",
>>>>  {(("'a", 0), (["HOL.type"], "??'a ⇒ ??'a")),
>>>>    (("?'a", 0),
>>>>      (["HOL.type"],
>>>>       "'b"))}) (line 165 of
>>>> "/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
>>>> ("candidate term:",
>>>>  Const ("Scratch.pure_stream",
>>>>         "?'a
>>>>          ⇒ ?'a Stream.stream")) (line 167 of
>>>> "/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
>>>> ("after unification:",
>>>>  Const ("Scratch.pure_stream",
>>>>         "(??'a ⇒ ??'a)
>>>>          ⇒ (??'a
>>>>              ⇒ ??'a) Stream.stream")) (line 168 of
>>>> "/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
>>>> "pure_stream id"
>>>>   :: "('a ⇒ 'a) stream"
>>>>
>>>> The result of unification is a bit surprising to me, since the
>>>> obtained "unifier" seems to claim that
>>>>
>>>>   ('b => 'b) => ('b => 'b) stream
>>>>
>>>> and
>>>>
>>>>   (??'a => ??'a) => (??'a => ??'a) stream
>>>>
>>>> are equal. What am I missing here? Maybe Envir.subst_term_types is not
>>>> the way to apply the typenv obtained by typ_unify? (In this special
>>>> case, if I would call subst_term_types twice with the same typenv, the
>>>> result would be as I expected.)
>>>>
>>>> cheers
>>>>
>>>> chris
>>>>
>>>> Btw: the "delete" patch (which is to be applied before "debug") fixes
>>>> a typo in the description of "no_adhoc_overloading". It is entirely
>>>> unrelated to the issue at hand, but maybe somebody could apply it
>>>> anyway.
>>>>
>>>> On 11/21/2014 07:31 PM, Christian Sternagel wrote:
>>>>> Dear Andreas,
>>>>>
>>>>> Thanks for the report, I'll have a look. First an immediate
>>>>> observation:
>>>>>
>>>>> When adding the following to Scratch.thy
>>>>>
>>>>> declare [[show_variants]]
>>>>>
>>>>> notepad
>>>>> begin
>>>>>    fix f :: "('b ⇒ 'b ⇒ 'a) stream"
>>>>>    and x :: "'b stream"
>>>>>    term "pure id :: ('b => 'b) stream"
>>>>>
>>>>> the first "term" results in
>>>>>
>>>>> "pure_stream id"
>>>>>    :: "('c ⇒ 'c) stream"
>>>>>
>>>>> while the second results in
>>>>>
>>>>> "pure_stream id"
>>>>>    :: "('b ⇒ 'b) stream"
>>>>>
>>>>> So it is not surprising that the first causes problems while matching.
>>>>> Why, however "'c" is produced instead of "'b" is not immediately clear
>>>>> to me. I'll investigate.
>>>>>
>>>>> cheers
>>>>>
>>>>> chris
>>>>>
>>>>> On 11/21/2014 04:09 PM, Andreas Lochbihler wrote:
>>>>>> Dear experts on adhoc overloading,
>>>>>>
>>>>>> When I want to instantiate variables in a theorem using the attribute
>>>>>> "of", sometimes the exception TYPE_MATCH gets raised. This seems
>>>>>> strange
>>>>>> to me because I would expect that adhoc_overloading either complains
>>>>>> about not being able to uniquely resolve an overloaded constant or
>>>>>> exchanges the constant in the AST.
>>>>>>
>>>>>> By adding more type annotations, I have so far been able to
>>>>>> circumvent
>>>>>> the exception, but there seems to be a check missing. Attached you
>>>>>> find
>>>>>> a small example.
>>>>>>
>>>>>> Best,
>>>>>> Andreas
>>>
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

More information about the isabelle-dev mailing list