Hi all! Is it possible to have parametrically polymorphic terms and types in locale contexts? A minimal example would be capturing the specification of a set container as a locale.
Not sure what you mean? something like
locale foo
fixes mylist::"'a list"
assumes "length mylist > 0"
begin
....
end
Let's take the specification of a polymorphic sorting function as an example. If one writes
locale sorting_function
fixes sort_func :: "'a::{ord} list => 'a list"
...
then it's my understanding that this will fix the type parameter 'a
at time of locale instantiation. In other words, the locale captures sorting functions for a specific type. What I want is a locale capturing polymorphic sorting functions.
I don't think that this is possible due to Isabelle's rank 1 polymorphism. You need to instantiate the locale for each type
Or use sorting_function.sort_func
to delay typing
The example I alluded to originally is that of a locale capturing a set container, where the parametric container type should be part of the locale. So, in an ideal world, I'd like to be able to write something like
locale set_abstraction
"fix_polymorphic_type container : (eq) type"
fixes new_container :: "'a container"
fixes add_element :: "'a => 'a container => 'a container"
fixes remove_element ...
I assume that the answer here, too, is "not possible in Isabelle" -- but do you have ideas for workarounds?
I have no idea, sorry
I don't even know why you would want to do so (but I am not an haskell programmer)
Please feel free to point out my misconception, but isn't this a fairly natural thing to do? You have some code which needs a set container with varying element types, but you don't want to bake a specific choice into the implementation because it is irrelevant. A 'parametric' locale would allow you to do that.
Wouldn't the one parameter locale you showed still work for the example that you are suggesting? You can always instantiate it to a product type 'a1 × 'a2 × ... × 'an
, to a function type or to a record.
I am thinking of something like:
locale container =
fixes is_element :: "'container_type ⇒ 'element_type ⇒ bool"
and add_element :: "'element_type ⇒ 'container_type ⇒ 'container_type"
and remove_element :: "'element_type ⇒ 'container_type ⇒ 'container_type"
and new_container :: "'io_type ⇒ 'container_type"
@Jonathan Julian Huerta y Munive Thanks for chiming in! In your locale, the element_type
is fixed per instantiation, though, isn't it?
Yes, it is fixed. I do not know what you intend to model and for what purpose, but I think you can still do it with Isabelle, albeit with some work. For instance, if you are thinking of containers of strings, nats and ints, you can always do:
locale container =
fixes is_element :: "'container_type ⇒ 'element_type ⇒ bool"
and add_element :: "'element_type ⇒ 'container_type ⇒ 'container_type"
and remove_element :: "'element_type ⇒ 'container_type ⇒ 'container_type"
and new_container :: "'io_type ⇒ 'container_type"
and map2set :: "'container_type ⇒ 'element_type set"
assumes maps2set: "is_element X x ⟷ x ∈ map2set X"
datatype some_types = tString "string" | tInt "int" | tNat "nat"
interpretation some_types_set_is_container: container "λX (x::some_types). x ∈ X"
insert "λx X. X - {x}" "λio. {}" id
by unfold_locales
auto
find_theorems name: some_types_set_is_container
Last updated: Dec 07 2024 at 16:22 UTC