Discussion:
[isabelle] difficulties with polymorphic record extension
(too old to reply)
Elsa L. Gunter
2016-07-27 13:44:27 UTC
Permalink
Raw Message
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
Andreas Lochbihler
2016-07-27 14:20:07 UTC
Permalink
Raw Message
Dear Elsa,

The excessive polymorphism is due to the way record extensions are constructed. Input
syntax like (|Instructions = a, Directions = b, edgeTyping = c|) are translated into the
record construction functions XXX_ext, i.e., "generalized_control_flow_graph_context_ext"
and "generalized_control_flow_graph_ext". Each of these takes as the last argument 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 the translation, the connection
between the type variables in generalized_control_flow_graph_context_ext and
generalized_control_flow_graph_ext is lost. So there is no way for the type inference
algorithm to see that you want the type variables to be instantiated to the same. As the
translation happens before type inference, it is not (easily) possible to add sensible
type annotations, either. In summary, you need some sort of external enforcement that will
show up in your input syntax.

I do not know what you came up with, but the simplest thing that comes to my mind is to
use a cast operator as an abbreviation. Here is a small 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 the formulas you write, but it
never shows up in any theorem, so it does not affect your reasoning.

Hope this helps,
Andreas
Post by Elsa L. Gunter
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
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
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
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
Elsa L. Gunter
2016-08-08 19:52:04 UTC
Permalink
Raw Message
Thank you Andreas, both for reminding me of what I should have known
(and probably once did) about record extension, and for the suggested fix.

---Elsa
Post by Andreas Lochbihler
Dear Elsa,
The excessive polymorphism is due to the way record extensions are
constructed. Input syntax like (|Instructions = a, Directions = b,
edgeTyping = c|) are translated into the record construction functions
XXX_ext, i.e., "generalized_control_flow_graph_context_ext" and
"generalized_control_flow_graph_ext". Each of these takes as the last
argument 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 the
translation, the connection between the type variables in
generalized_control_flow_graph_context_ext and
generalized_control_flow_graph_ext is lost. So there is no way for the
type inference algorithm to see that you want the type variables to be
instantiated to the same. As the translation happens before type
inference, it is not (easily) possible to add sensible type
annotations, either. In summary, you need some sort of external
enforcement that will show up in your input syntax.
I do not know what you came up with, but the simplest thing that comes
to my mind is to use a cast operator as an abbreviation. Here is a
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 the
formulas you write, but it never shows up in any theorem, so it does
not affect your reasoning.
Hope this helps,
Andreas
Post by Elsa L. Gunter
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
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
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
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
Loading...