Patrick Nicodemus (Oct 29 2023 at 23:58): Patrick Nicodemus (Oct 29 2023 at 23:58):Say I have a locale with like a dozen different declarations and four polymorphic types. The different declarations are all functions between the four polymorphic types. How can I bundle all this data into one thing like a record type? It's my understanding that records can only be polymorphic in a single variable. What's the closest thing I can get to a record that allows me to have polymorphism in multiple type variables?
Patrick Nicodemus (Oct 30 2023 at 00:27):Here's one way to get record types with multiple polymorphism.
locale precategory =
fixes precategory :: "('a set) × ('a ⇒ 'a ⇒ 'b set) × ('a ⇒ 'b) × ('a ⇒ 'a ⇒ 'a ⇒ 'b ⇒ 'b ⇒ 'b)"
definition (in precategory) obj where "obj = fst precategory"
definition (in precategory) hom where "hom = fst (snd precategory)"
definition (in precategory) id where "id = fst (snd (snd precategory))"
definition (in precategory) comp where "comp = snd (snd (snd precategory))"
locale category =
C : precategory precategory for precategory +
assumes id_def : "x ∈ C.obj ⟹ (C.id x) ∈ (C.hom x x)"
and comp_def :
"⟦ x ∈ C.obj ; y ∈ C.obj ; z ∈ C.obj ;
f ∈ (C.hom x y); g ∈ (C.hom y z) ⟧ ⟹ (C.comp x y z f g) ∈ (C.hom x z)" and
id_left : "⟦ x ∈ C.obj ; y ∈ C.obj ; f ∈ C.hom x y ⟧ ⟹
(C.comp x x y (C.id x) f ) =f" and
id_right : "⟦ x ∈ obj ; y ∈ obj ; f ∈ hom x y ⟧ ⟹
(C.comp x y y f (C.id y)) = f" and
assoc : "⟦ w ∈ C.obj; x ∈ C.obj; y ∈ C.obj; z ∈ C.obj ;
f ∈ hom w x; g ∈ hom x y; h ∈ hom y z ⟧ ⟹
C.comp w y z (C.comp w x y f g) h =
C.comp w x z f (C.comp x y z g h)"
Is there a more elegant way? What's idiomatic
Patrick Nicodemus (Oct 30 2023 at 00:51):Never mind! I am being silly!
I did not realize that you could have record types with polymorphism across multiple type variables!
I typed record 'a 'b and saw that this was a syntax error and couldn't find any reference to record polymorphism in multiple variables.
Last updated: Apr 28 2024 at 04:17 UTC