Stream: Beginner Questions

Topic: Locale with type parameter


view this post on Zulip Bob Rubbens (May 06 2023 at 09:45):

Good morning, I would like to make a series of functions all depend on one datatype/type parameter. I figured maybe locales could help me as follows:

theory Scratch
 imports Main
begin

locale Foo =
  fixes proxy_to_get_type_var :: 'element_type
begin

datatype Inner = Inner 'element_type

end

end

Note that I don't plan on using proxy_to_get_type_var; I figured I needed a way to indicate to the locale that I want at least one type parameter, and this seems to be the only way of doing it. In a way I'm trying to declare a type parameter.

Unfortunately Isabelle gives an error saying, at declaration of Inner, there is a free type variable on the right hand side. Instead, I would like it to use the 'element_type type parameter from the locale. I want this because then the subsequent datatypes don't need an extra type parameter, and this makes all function types a bit shorter.

I could add this type parameter everywhere to avoid using a locale. But I feel like it would be more readable like this. Am I doing something wrong or is there maybe some different construct I can use to emulate this?

view this post on Zulip Lukas Stevens (May 08 2023 at 08:48):

Unfortunately, Isabelle/HOL does not have dependent types. This means that the type parameters can't depend on the local context (the locale in this case).


Last updated: Feb 27 2024 at 08:17 UTC