Stream: Beginner Questions

Topic: ✔ Use type in class declaration

Jan van Brügge (Jun 30 2022 at 12:56):

Is there a way to refer to the type that implements the type class? For example given a class like this:

class foo = assumes "P UNIV"

how can I ensure that an instance declaration uses the correct UNIV?

instantiation nat :: foo begin
instance apply standard
(* How do I make sure that the goal is "P (UNIV :: nat set)" here? *)

Mathias Fleury (Jun 30 2022 at 13:05):

IsaFoR uses a type_fixer parameter for such case:

class foo = fixes type_fixer :: "'a"  assumes "P (UNIV :: 'a set)"

instantiation nat :: foo
begin

definition type_fixer_nat :: ‹nat itself› where
  ‹type_fixer_nat ≡ TYPE(nat)›

instance apply standard
  sorry

Jan van Brügge (Jun 30 2022 at 13:06):

thought about something like that, but nothing would prevent me to use TYPE(unit) there, wouldn't it?

Mathias Fleury (Jun 30 2022 at 13:10):

No.

Jan van Brügge (Jun 30 2022 at 13:15):

I guess it just has to be documented that it needs to be the same type as the type that the class is defined for. Weird that there is no syntax for this, in Haskell it would be easy:

class Foo a where x :: P (UNIV a)

Jan van Brügge (Jun 30 2022 at 13:15):

in isabelle this could look similar:

class 'a foo = (* ... *)

Mathias Fleury (Jun 30 2022 at 13:22):

wait

class foo =
  assumes finite_UNIV: "P (UNIV :: 'a set)"
begin
end

instantiation nat :: foo
begin
instance
  supply [[show_sorts, show_types]]
  apply standard

does what you want right?

Mathias Fleury (Jun 30 2022 at 13:23):

I checked how finite does it

Jan van Brügge (Jun 30 2022 at 13:38):

ehh, what should I see? It does not show me the type of UNIV

Mathias Fleury (Jun 30 2022 at 13:39):

no but of P

Mathias Fleury (Jun 30 2022 at 13:39):

and P has the right type

Jan van Brügge (Jun 30 2022 at 13:43):

is there a way to get isabelle to show the types of constants e.g. on ctrl+hover?

Mathias Fleury (Jun 30 2022 at 13:46):

I don't know any

Jan van Brügge (Jun 30 2022 at 13:55):

apply (tactic ‹SUBGOAL (fn (t, _) =>
    let val _ = @{print} t
    in all_tac end) 1
  ›)

works and it confirms that it has the correct type. Interesting

Notification Bot (Jun 30 2022 at 13:55):

Jan van Brügge has marked this topic as resolved.

Manuel Eberl (Jul 01 2022 at 10:49):

Just to confirm, in the context of a type class, the type that you're talking about is always 'a.

Last updated: Apr 20 2024 at 08:16 UTC