irvin (May 02 2024 at 04:44): irvin (May 02 2024 at 04:44):Hi would like to ask how to instantiate a type class with a type with multiple of the same type for arity
such as a function mapping to itself 'a => 'a
instantiation "fun" :: (type ,type) instead instantiates for 'a => 'b.
Lukas Stevens (May 02 2024 at 09:16):I think this is not possible. You could define a type for endofunctions (i.e. functions with type 'a => 'a) using typedef and then instantiate your typeclass for this type.
irvin (May 07 2024 at 11:16):Thanks for your reply. I managed to do it manually using ML using Class.instantiation is there any reason for this behavior in the isar cmd?
irvin (May 07 2024 at 18:02):wait nvm i just realized I didnt manage to succeed with doing it in ML :oh_no:
Manuel Eberl (Sep 15 2024 at 10:22):It's just a fundamental restriction of the way type classes work in Isabelle/HOL. If you allow more flexibility in type class instantiations, you can easily get things like overlapping instances and all the checks become much more difficult. If you overdo it, type class inference becomes computationally hard or even undecidable.
Manuel Eberl (Sep 15 2024 at 10:22):This is probably described in the documentation on type classes
irvin (Sep 16 2024 at 12:29):Thanks for your reply i manually worked around the issue using adhoc overloading + locales instead
Last updated: Dec 30 2024 at 16:22 UTC