Abstract and Concrete Type Classes
From Impredicative Wiki
Type classes can be abstract such that new instances may not be added (giving a closed, fixed predicate of general arity over types) or concrete with the possibility of users adding new types to the family (extending the extension of the predicate).
Here is a sample of an abstract type class.
(* * Here is an abstract type class example. We cannot add more instances. *) structure Abstract : sig class abs val speak : t ::: Type -> abs t -> t -> string val abs_int : abs int val abs_float : abs float end = struct class abs t = t -> string fun speak [t ::: Type] (d : abs t) (x : t) = d x fun abs_int (i : int) = "integer noise" fun abs_float (f : float) = "float noise" end open Abstract (* * If we try to make a string speak we will get an error. * There is no instance for string in the class abs. *) (* val s : string = speak "What noise does a string make?" *) (* * We can think of the functions abs_int and abs_float being "evidence" witnessing * the fact that the types int and float belong to the class abs ... if we think * of abs as being a one-place predicate over types then its extension or characteristic * set holds int and float *) fun main () = return <xml> <head> <title>Concrete and Abstract Type Classes in Ur/Web</title> </head> <body> <h1>Concrete and Abstract Type Classes</h1> <p> The Ur/Web type class mechanism allows for both concrete and abstract classes. </p> <h2> An illustracion </h2> <p> Some integer noises speak 3 = {[speak 3]} speak 8 = {[speak 8]} </p> <p> Some float noises speak 5.4 = {[speak 5.4]} speak 3.14 = {[speak 3.14]} </p> </body> </xml>
Here is a sample of a concrete type class.
(* * Extending a concrete type class in Ur/Web *) structure Concrete : sig class conc val speak : t ::: Type -> conc t -> t -> string val mkConc : t ::: Type -> (t -> string) -> conc t val conc_int : conc int val conc_float : conc float end = struct class conc t = t -> string fun speak [t ::: Type] (d : conc t) (x : t) = d x fun mkConc [t ::: Type] (f : t -> string) = f fun conc_int (i : int) = "makes an integer noise" fun conc_float (f : float) = "makes a float noise" end (* * The presence of mkConc among the items exported by the * Concrete module is what makes the conc typeclass concrete. * At the Ur/Web module system or typeclass system there is no * distinction between these cases via different constructs. * Now users may add their own instances. *) open Concrete (* We add a string case *) val conc_string : conc string = mkConc (fn (s : string) => "makes a string noise") fun main () = return <xml> <head> <title>Concrete and Abstract Type Classes in Ur/Web</title> </head> <body> <h1>Concrete and Abstract Type Classes</h1> <p> The Ur/Web type class mechanism allows for both concrete and abstract classes. </p> <h2> An illustracion </h2> <p> Some integer noises speak 3 = {[speak 3]} speak 8 = {[speak 8]} </p> <p> Some float noises speak 5.4 = {[speak 5.4]} speak 3.14 = {[speak 3.14]} </p> <p> Some string noises speak "aaa" = {[speak "aaa"]} speak "foo" = {[speak "foo"]} </p> </body> </xml>