Stream: Beginner Questions

Topic: Parametric polymorphism in locales

Hanno Becker (Dec 05 2022 at 14:27):

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.

Julian (Dec 05 2022 at 15:51):

Not sure what you mean? something like
locale foo
fixes mylist::"'a list"
assumes "length mylist > 0"
begin
....
end

Hanno Becker (Dec 05 2022 at 16:09):

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.

Mathias Fleury (Dec 05 2022 at 16:15):

I don't think that this is possible due to Isabelle's rank 1 polymorphism. You need to instantiate the locale for each type

Mathias Fleury (Dec 05 2022 at 16:15):

Or use sorting_function.sort_functo delay typing

Hanno Becker (Dec 05 2022 at 17:21):

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?

Mathias Fleury (Dec 05 2022 at 18:01):

I have no idea, sorry

Mathias Fleury (Dec 05 2022 at 18:02):

I don't even know why you would want to do so (but I am not an haskell programmer)

Hanno Becker (Dec 05 2022 at 19:17):

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.

Jonathan Julian Huerta y Munive (Dec 05 2022 at 19:25):

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.

Jonathan Julian Huerta y Munive (Dec 05 2022 at 19:34):

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"

Hanno Becker (Dec 07 2022 at 09:38):

@Jonathan Julian Huerta y Munive Thanks for chiming in! In your locale, the element_type is fixed per instantiation, though, isn't it?

Jonathan Julian Huerta y Munive (Dec 07 2022 at 10:00):

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: Apr 25 2024 at 08:20 UTC