Email Gateway (Aug 22 2022 at 11:02): Email Gateway (Aug 22 2022 at 11:02):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I've created some (very rough) tooling for type classes and automatic
instance resolution for Isabelle/ML. You can find the sources on GitHub:
<https://github.com/larsrh/classy>
This was prompted by my unwillingness to write code like this:
val codec =
Codec.tuple
(Codec.list
(Codec.tuple
Term_Codec.term
Term_Codec.term))
(Codec.tuple
Term_Codec.typ
Term_Codec.typ)
This can now be simply written as
val codec =
@{ML.resolve ‹(term * term) list * (typ * typ)› :: codec}
You can have a look at the files "Classy.thy" and "Examples.thy" to get
an idea of how it can be used.
A word of warning: The resolution algorithm is utterly stupid; it just
performs a naive search of all possible instances. Notably, it is not
even guaranteed to terminate. When declaring instances, there are no
checks whether an instance is wellformed (e.g. according to Haskell98's
or Isabelle's notion of wellformedness). All of this is purely
syntactic, that is, it gets confused when type aliases are involved.
However, the code does support local instances (as long as they don't
override other ones) and observes the usual Isabelle conventions wrt to
local theories.
Parts of the code are lifted from Spec_Check, especially those dealing
with parsing ML types. "classy" is in some sense even more general than
the mechanisms in Spec_Check, because it isn't specialized to random
value generators.
Feedback most welcome.
Cheers
Lars
Last updated: Apr 25 2024 at 16:19 UTC