Email Gateway (Aug 18 2022 at 14:10): Email Gateway (Aug 18 2022 at 14:10):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi!
Is there any way to provide default implementations for type class
functions that may be overwritten by the user?
I'm thinking of something like the Haskell Show class, i.e.,
types "shows" = "string => string"
class "show" =
fixes "show" :: "'a => string"
and shows_prec :: "nat => 'a => shows"
and shows_list :: "'a list => shows"
together with the functions
definition "shows" :: "'a::show => shows"
where "shows = shows_prec (0::nat)"
fun showl :: "('a ⇒ shows) ⇒ string ⇒ 'a list ⇒ string"
where "showl showx s [] = CHR '']'' # s"
| "showl showx s (x#xs) = CHR '','' # showx x (showl showx s xs)"
fun shows_list_aux :: "('a ⇒ shows) ⇒ 'a list ⇒ shows"
where "shows_list_aux _ [] s = ''[]'' @ s"
| "shows_list_aux showx (x#xs) s =
(CHR ''['') # showx x (showl showx s xs)"
hide const showl
where the default implementations could be
show x = shows_prec 0 x ''''
shows_prec d x s = show x @ s
shows_list xs s = show_list_aux shows xs s
Any ideas?
cheers
christian
Email Gateway (Aug 18 2022 at 14:10):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
there is no such mechanism in Isabelle. You can simulate something
similar by adding shows and showl together with their simplifications
rules to the class specification; of course this does not release you
from the burden to instantiate all those parameters explicitly for each
desired type.
Hope this helps
Florian
signature.asc
Last updated: Apr 20 2024 at 08:16 UTC