*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] difficulties with polymorphic record extension*From*: "Elsa L. Gunter" <egunter at illinois.edu>*Date*: Mon, 8 Aug 2016 14:43:52 -0500*Cc*: "Bergvelt, David Paul" <bergvel1 at illinois.edu>*In-reply-to*: <05b34ed6-e754-dca6-d9bf-a38a64a7dfea@inf.ethz.ch>*References*: <3d0f8b8d-4359-6a26-880e-05208ea78cb0@illinois.edu> <05b34ed6-e754-dca6-d9bf-a38a64a7dfea@inf.ethz.ch>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

---Elsa On 7/27/16 9:15 AM, Andreas Lochbihler wrote:

Dear Elsa,The excessive polymorphism is due to the way record extensions areconstructed. Input syntax like (|Instructions = a, Directions = b,edgeTyping = c|) are translated into the record construction functionsXXX_ext, i.e., "generalized_control_flow_graph_context_ext" and"generalized_control_flow_graph_ext". Each of these takes as the lastargument what is to be put into the extension slot. Hence,âInstructions =a, Directions = b, edgeTyping =c, Nodes = d, Edges = e, labeling = fâ is translated to generalized_control_flow_graph_context_ext a b c (generalized_control_flow_graph_ext d e f ())and it is this term on which type inference works. After thetranslation, the connection between the type variables ingeneralized_control_flow_graph_context_ext andgeneralized_control_flow_graph_ext is lost. So there is no way for thetype inference algorithm to see that you want the type variables to beinstantiated to the same. As the translation happens before typeinference, it is not (easily) possible to add sensible typeannotations, either. In summary, you need some sort of externalenforcement that will show up in your input syntax.I do not know what you came up with, but the simplest thing that comesto my mind is to use a cast operator as an abbreviation. Here is asmall example:record 'a foo = foo :: 'a record 'a bar = "'a foo" + bar :: 'a abbreviation (input) BAR :: "'a bar â 'a bar" where "BAR x â x" term "BAR âfoo = 0, bar = 0â"As BAR is an input abbreviation, it really only shows up in theformulas you write, but it never shows up in any theorem, so it doesnot affect your reasoning.Hope this helps, Andreas On 27/07/16 15:38, Elsa L. Gunter wrote:Dear Isabelle community, I am having difficulty building records they way I want. I may well have forgotten something, but the behavior I am see with extending polymorphic records is surprising to me. First I define: record ('instr,'dir) generalized_control_flow_graph_context = Instructions :: "'instr set" Directions :: "'dir set" edgeTyping :: "'instr â ('dir â nat)set" If I then enter declare [[show_types = true]] term "âInstructions =a, Directions = b, edgeTyping =câ" I get "âInstructions = a::'a set, Directions = b::'b set, edgeTyping = c::'a â ('b â nat) setâ" :: "('a, 'b) generalized_control_flow_graph_context" as output, which is what I would expect. Now I wish to extend this record to a new record with additional fields, introducing some new type variables, but also sharing the type variables already used in generalized_control_flow_graph_context. So I enter the following: record ('instr,'dir,'node) generalized_control_flow_graph = "('instr,'dir) generalized_control_flow_graph_context" + Nodes :: "'node set" Edges :: "'node â ('dir Ã 'node)set" labeling :: "'node â 'instr" The intent is that the types of 'dir and 'instr are shared between Instructions, Directions, edgeTyping, Edges and labeling. When I create at element of this extended record type as follows I get the given results: term "âInstructions =a, Directions = b, edgeTyping =c, Nodes = d, Edges = e, labeling = fâ" "âInstructions = a::'a set, Directions = b::'b set, edgeTyping = c::'a â ('b â nat) set, Nodes = d::'e set, Edges = e::'e â ('d Ã 'e) set, labeling = f::'e â 'câ" :: "âInstructions :: 'a set, Directions :: 'b set, edgeTyping :: 'a â ('b â nat) set, Nodes :: 'e set, Edges :: 'e â ('d Ã 'e) set, labeling :: 'e â 'câ" Note that the types of Nodes, Edges, labeling are completely independent of those for Instructions, Directions and edgeTyping, despite the same types being used in both parts of the generalized_control_flow_graph record definition. I know each type gets separately parsed separately, but it seems plausible that the whole record extension package could infer that the types used in one part of the definition where to be the same as those of the same name in other parts. These extra degrees of freedom present problems where type variables can end up buried on the right-hand side of a definition without being captured by the left hand side, where they would if the desired type constraints had been enforced. I have found a number of crufty ways around the difficulty, but I would appreciate help with learning how to do this record extension definition correctly. I've not been able to find it in the documentation. ---Elsa

- Previous by Date: [isabelle] New in the AFP: The Imperative Refinement Framework
- Next by Date: Re: [isabelle] Literature on the type system of Isabelle/HOL; text by Mike Gordon
- Previous by Thread: [isabelle] New in the AFP: The Imperative Refinement Framework
- Next by Thread: Re: [isabelle] qed and done take long for large goal states
- Cl-isabelle-users August 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list