Re: [isabelle] default implementations for type classes



Hi Christian,

> Is there any way to provide default implementations for type class
> functions that may be overwritten by the user?
> 
> 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

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

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.