Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Specializing types in locales

view this post on Zulip Email Gateway (Aug 18 2022 at 16:18):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Hello all,

In a locale, when a definition uses a parameter, specialization of one of his
type variables through constrains on an other parameter seems not possible.
However, it is possible with constrains on this parameter.

For example:

locale foo1_loc =
fixes bar :: "'a"
fixes foo :: "'a"
begin
definition "foo' a = foo"
end

locale foo1_nat_loc = foo1_loc +
constrains foo :: "nat"

(*
locale foo1_nat_loc' = foo1_loc +
constrains bar :: "nat"
Error: Failed to meet type constrain
*)

As a result, it seems impossible to specialize a type variable shared by
several parameters used in definitions:

locale foo3_loc =
fixes bar :: "'a"
fixes foo :: "'a"
begin
definition "foobar = (foo, bar)"
end

(*
locale foo3_nat_loc = foo3_loc +
constrains bar :: "nat"
constrains foo :: "nat"
Error: Failed to meet type constrain
*)

See attachment for more examples.

Is this a bug or is there any fundamental reason this doesn't work ?

To solve this problem, a great feature would be to have specializable type
declarations but I've understood it wasn't possible due to the logical
framework (quantification on types) in an email from Makarius:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-July/msg00111.html

I know I could also use AWE, but there is no release for Isabelle 2009-2 (but
I haven't tried the one for Isabelle 2009-2 that could perhaps also work).

Furthermore in an other mail, Makarius said:
Trying a bit harder in the internal structures, one could support type
parameters on the RHS one day.
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-July/msg00033.html

Is this still a possibility ?

Thanks,

Mathieu Giorgino
Type_Specialization_Locales.thy

view this post on Zulip Email Gateway (Aug 18 2022 at 16:18):

From: Brian Huffman <brianh@cs.pdx.edu>
Note that when you have separate "constrains" clauses, they are
applied one at a time. You can't constrain the type of "bar" by
itself, because then it doesn't have the same type as "foo", which the
function "foobar" requires.

However, it works if you declare both type constraints simultaneously.
(I tested this with Isabelle2009-2.)

locale foo3_nat_loc = foo3_loc +
constrains bar :: "nat" and foo :: "nat"

The same trick also works on all the other examples in your file that
I tried it on.

Hope this helps,

view this post on Zulip Email Gateway (Aug 18 2022 at 16:18):

From: Clemens Ballarin <ballarin@in.tum.de>
Dear Mathieu,

Type instances (like other parameter instantiations) should be given
in the locale expression. In your example, use something like

locale foo1_nat_loc' = foo1_loc bar foo for bar :: nat and foo

to instantiate the parameter bar with some bar of type nat, which will
become a parameter of the new locale.

The constrains element stems from times when locale expressions were
based on renaming rather than instantiation. It is deprecated and
will disappear in a future release of Isabelle.

Clemens

Quoting Mathieu Giorgino <mathieu.giorgino@irit.fr>:

view this post on Zulip Email Gateway (Aug 18 2022 at 16:19):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Clemens,

Yes, it still does, at least with the Isabelle versions I tested: Isabelle
repository version 43916ac560a4 and Isabelle 2009-2. Here is a small example:

locale A =
fixes a :: "'b => 'c" ("%_%")

locale B = A begin
term "%undefined%" -- "works fine"
end

locale C =
A a
for a :: "'b => 'c"
begin
term "%undefined%" -- "Gives inner syntax error at %"
end

Andreas

view this post on Zulip Email Gateway (Aug 18 2022 at 16:23):

From: Clemens Ballarin <ballarin@in.tum.de>
Hi Andreas,

Your approach with for would work nicely if it did not erase all
mixfix syntax annotations on the parameters.

Sorry, I had misread your message.

The syntax of a parameter is either given in a fixes element or a
for clause. If no syntax is specified, this means that no syntax is
requested. This is so even in a for clause, because there needs to be
a mechanism to get rid of unwanted syntax when extending a locale.

While replying I though of the syntax of a constant (as introduced
by a definition statement). Those are preserved under changes of the
parameter types.

Clemens

Yes, it still does, at least with the Isabelle versions I tested:
Isabelle repository version 43916ac560a4 and Isabelle 2009-2. Here
is a small example:

locale A =
fixes a :: "'b => 'c" ("%_%")

locale B = A begin
term "%undefined%" -- "works fine"
end

locale C =
A a
for a :: "'b => 'c"
begin
term "%undefined%" -- "Gives inner syntax error at %"
end

Andreas

view this post on Zulip Email Gateway (Aug 18 2022 at 16:28):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Clemens,

When it disappears, please provide a way to simulate the behaviour of
constrains. I use it a lot to undo the havoc that locale inheritance causes on
type variable names. It is no use to have ten type variables 'a to 'j floating
around that get renamed every now and then. Your approach with for would work
nicely if it did not erase all mixfix syntax annotations on the parameters. It
is hard to consistently change mixfix syntax when it is repeated all over the place.

Andreas

view this post on Zulip Email Gateway (Aug 18 2022 at 16:30):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Thanks Brian and Clemens,

The Brian's solution worked well but it was still necessary to contrains all
parameters.

With Clemens' one, it is not any more necessary: the type is constrained once
for all parameters.

However, is there anyone having a clue about my last question?

A great feature would be to have specializable
type declarations but I've understood it wasn't possible due to the
logical framework (quantification on types) in an email from Makarius:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-
July/msg00111.html

I know I could also use AWE, but there is no release for Isabelle 2009-2
(but I haven't tried the one for Isabelle 2009-2 that could perhaps also
work).

Furthermore in an other mail, Makarius said:
Trying a bit harder in the internal structures, one could support type
parameters on the RHS one day.
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-
July/msg00033.html
Is this still a possibility?

Thanks,

Mathieu

view this post on Zulip Email Gateway (Aug 18 2022 at 16:32):

From: Clemens Ballarin <ballarin@in.tum.de>
Hi Andreas,

Your approach with for would work nicely if it did not erase all
mixfix syntax annotations on the parameters.

Does it? I had hoped this was fixed with

changeset: 32985:6c273b0e0e26
user: ballarin
date: Mon Nov 02 21:27:26 2009 +0100
summary: Relax on type agreement with original context when
applying term sy
ntax.

which should keep the syntax provided only the type of the parameter
is changed.

Clemens

Last updated: Nov 21 2024 at 12:39 UTC