Stream: General

Topic: Hiding type class instances


view this post on Zulip Lukas Stevens (Aug 11 2020 at 13:05):

In HOL-Library, there are two different instantiations of prod :: (ord, ord) ord. If I import one of them, is everyone who in turn imports my theory forced to use the instance I chose or is there a way to hide those instances?

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:06):

No, type class instances are forever. One of the reasons why Isabelle's type classes are… not great.

view this post on Zulip Lukas Stevens (Aug 11 2020 at 13:06):

Hm, that is quite unfortunate.

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:07):

When you instantiate a type class, you're adding a definition for all the overloaded constants that it contains. You cannot have two different definitions for the same thing and you cannot "delete" definitions, so this cannot work.

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:08):

To support something like this, I think one would have to overhaul the entire type class system from ground up.

view this post on Zulip Lukas Stevens (Aug 11 2020 at 13:10):

Ok, what would be the canonical way to customize the comparison operator in linorder.sorted_list_of_set?

view this post on Zulip Lukas Stevens (Aug 11 2020 at 13:14):

I just now noticed that the type class instance I had in mind would not work anyways...

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:27):

I don't think you can simply "customise" it. You can of course make a type copy of whatever your type is, do the ord instance in whichever way you want it to be, and then convert back and forth

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:29):

fwiw I defined a sorted_wrt_list_of_set function in the AFP, in Comparison_Sort_Lower_Bound.Linorder_Relations, along with some other operations on orderings that take the ordering as an explicit relation instead of from the typeclass.

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:29):

definition sorted_wrt_list_of_set where
  "sorted_wrt_list_of_set R A =
     (if finite A then (THE xs. set xs = A ∧ distinct xs ∧sorted_wrt R xs) else [])"

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:29):

If your ordering isn't linear, you'll have to switch the THE to a SOME.

view this post on Zulip Lukas Stevens (Aug 11 2020 at 13:34):

Concerning the sorted_wrt_list_of_set: I only need sorted_key_list_of_set f ≡ folding.F (insort_key f) []. But then I need to reprove the lemmas that exist about sorted_list_of_set.

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:35):

Yeah if you really care about getting around that, you might have to do the typedef trick I told you about

view this post on Zulip Lukas Stevens (Aug 11 2020 at 13:36):

The problem is that antisymmetry does not hold if f = fst.

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:38):

yeah the whole point of sorted_list_of_set is that it is unique

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:38):

Otherwise you can just do "sort (list_of_set …)".

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:38):

That's not computable though, for obvious reasons.

view this post on Zulip Lukas Stevens (Aug 11 2020 at 13:42):

One would need some distinctness condition w.r.t. f

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:50):

How would distinctness be enough? What kind of ordering do you have?

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:50):

Ah you have a linear order on the keys, I see. Yeah.

view this post on Zulip Lukas Stevens (Aug 11 2020 at 13:52):

Yes, my goal is to define a fold operation on Mappings. For this I first need an ordered_entries operation (which orders the entries by the first component).

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:55):

I think something like this already exists as long as the operation with which you fold is order-independent

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:56):

at least I vaguely remember having done such a thing for PMFs in HOL-Probability

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:56):

they are implemented as mappings, and when you want to implement monadic bind/join, you need to fold over that mapping and sum up some values

view this post on Zulip Manuel Eberl (Aug 11 2020 at 13:57):

Did you look at Mapping.combine?

view this post on Zulip Lukas Stevens (Aug 11 2020 at 13:58):

Yes, unfortunately this does not help me since my operation depends on both 'a and 'b

view this post on Zulip Lukas Stevens (Aug 11 2020 at 14:00):

More specifically, I need a nested fold where I combine all 'a with each other.

view this post on Zulip Lukas Stevens (Aug 11 2020 at 14:04):

I am thinking about going the less beautiful route and just using RBTs directly.

view this post on Zulip Lukas Stevens (Aug 11 2020 at 16:03):

Manuel Eberl said:

at least I vaguely remember having done such a thing for PMFs in HOL-Probability

Do you know where exactly? Grepping in src/HOL/Probability didn't yield anything for me.

view this post on Zulip Lukas Stevens (Aug 11 2020 at 16:08):

Ah maybe fold_combine_plus?

view this post on Zulip Manuel Eberl (Aug 11 2020 at 16:42):

Yes, but I think that used Mapping.cobmine.


Last updated: Aug 15 2022 at 02:13 UTC