Stream: Beginner Questions

Topic: Achieving "Generic Type Classes"

view this post on Zulip Alicia (Sep 05 2023 at 20:12):

Hello,

is there a way to achieve "generic type classes" (comparable to generic interfaces in Java)?
I came across a - to me - similar question in the archive that did not get my hopes up. Also, if I understand it correctly, the only type variable allowed in a class definition stands for an instance of the type class (I'm just getting started with type classes and locales).

Still, for lack of words, I'll use type classes for a (non-working) MWE:

class 'param polymorphic_type =
  fixes polymorphic_func :: "'param => 'a => bool"

Here, the 'a in the polymorphic_type stands for instances of the type class while 'param is some generic other type acting as a parameter.
Using this, I want to be able to define parameterized instance types:

datatype 'param instance_type = I1 'param

instantiation "'param instance_type" :: "'param polymorphic_type"
begin
definition
    polymorphic_func_instance_type_def : "polymorphic_func (a::'param) (x::('param instance_type)) = ..."
...
end

Especially, I'd like to be able to have functions of type "'param instance_type => ...", (e.g.) "nat instance_type" as well as "('a::('param polymorphic_type)) => ..."

I'd be very grateful if someone could maybe help me cut short (or abort) my search :-)

Thanks a lot in advance!

Kind regards,
Alicia

view this post on Zulip Wolfgang Jeltsch (Sep 05 2023 at 20:35):

I think that’s not possible. Other languages, most notably Haskell, have far more feature-rich type class systems, but Isabelle’s type class system is in particular restricted to one parameter per type class, because type classes are identified by sorts (the “types of types”): whenever you want to say that a type is an instance of a class, you say that this type is of the corresponding sort (e.g., nat :: ord), and this cannot work if you have several types that are collectively an instance of a class.

view this post on Zulip Mathias Fleury (Sep 06 2023 at 04:45):

That it is impossible over classes is also my understanding. You need to use locales.

view this post on Zulip Wolfgang Jeltsch (Sep 06 2023 at 12:35):

Yes, locales can be parameterized by an arbitrary number of types. They can furthermore have different interpretations for the same bunch of types. The price you pay is that interpretations are not picked automatically.

view this post on Zulip Alicia (Oct 04 2023 at 11:10):

Hello, thanks for your quick answers! I think it's kind of working with the locales (though I'm still not that good at handling them :D ).

Last updated: Apr 28 2024 at 04:17 UTC