[isabelle-dev] Additional type variable(s) in specification

[John Matthews]

As another user data point, a few months back I ran into this same  
issue of the type I specified not being the type Isabelle gave me  
back. It was pretty confusing at the time and it took me a while to  
figure out what was going on.

-john

On Dec 2, 2010, at 11:26 AM, Makarius wrote:

> On Thu, 2 Dec 2010, Alexander Krauss wrote:
>
>> I'll have a look at the code and see if packages can reject this  
>> from the user, while still being composable. This applies to all  
>> packages.
>
> In fact I've made this error already in 2005, and it was Alex  
> himself who convinced me more recently that packagages cannot  
> realistically do any check here, because the thing is so obscure  
> that hardly any package author will get to the point.
>
> Back to history: in 2005 Brian had a paper on TPHOLs with a footnote  
> about an unexpected crash of the typedef package due to hidden  
> polymorphism in the set involved, not the type.  What I did then is  
> to make the typedef package insert "itself" arguments in the way one  
> would think of as a first idea.  This made the problem go away for  
> the moment, although it complicated the package implementation.   
> When Larry was asking me about that change of typedef later, I also  
> failed to explain to him both the problem and its solution.
>
> After Local_Theory.define started handling the problem uniformly  
> once and for all, I could remove lots of strange code from typedef,  
> and be sure at the same time that all other (localized) packages  
> would stop crashing
> on the same kind of problem.
>
>
> When we speak about "users" of packages it covers both ML and Isar  
> theory sources, e.g. the function package is a user of the inductive  
> package. It is important to keep modularity here.
>
> The system is able to distinguish between things that are visible in  
> the source vs. internal uses of the same specifciation mechanisms to  
> some extent, but one needs to look very closely at that when  
> modifying the behaviour here.  We have already a long track record  
> of very abscure crashes due to errors that are emitted too eagerly,  
> e.g. in declaration attributes that insist in certain input and  
> choke on the transformed version after some interpretations.
>
> Part of the inherent complexity of local theory specifications is  
> due to interpretation wrt. the "target context", which always  
> happens when writing down specifications like 'definition' or  
> 'inductive'.  This is not the primitive consts + defs that we had  
> many yours ago.  And of course, the extra complexity localized  
> specifications was not introduced for fun, but to address concrete  
> problems that had accumulated over a couple of years of less  
> systematic treatment of these issues.  Compared to the situation  
> before it, there are very little problems left that need some fine  
> tuning.
>
>
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2205 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101202/07363dbe/attachment.bin>