Basic Examples of the Type Class Mechanism in Ur/Web
From Impredicative Wiki
(Difference between revisions)
Karn Kallio (Talk | contribs) (Simple usage example of the type class facility) |
Karn Kallio (Talk | contribs) (Clarification between constraint and polymorphism) |
Latest revision as of 12:48, 12 December 2010
Ur/Web permits regulated ad hoc polymorphism via a type class mechanism. Here are some simple example usages.
(* * Here is some simple examples of the typeclass facility in Ur/Web. * Note that classes are not available in the module which defines them, * so to make the examples work they may not be at the top level. *) structure Measurable : sig class measurable val length : t ::: Type -> measurable t -> t -> int val measurable_string : measurable string val measurable_list : t ::: Type -> measurable t -> measurable (list t) end = struct class measurable :: Type -> Type = fn (t :: Type) => t -> int val length : t ::: Type -> measurable t -> t -> int = fn [t ::: Type] (m : measurable t) => m val measurable_string : measurable string = strlen (* Here we copy listlength for sake of a self-contained example, but it is in the * library as List.length; you can get it by $/list *) val listlength = fn [a] => let fun length' acc (ls : list a) = case ls of [] => acc | _ :: ls => length' (acc + 1) ls in length' 0 end val measurable_list : t ::: Type -> measurable t -> measurable (list t) = fn [t ::: Type] (m : measurable t) => listlength end open Measurable (* * These will not compile because there is no instance for these types in the class *) (* val i : int = length 7 val i : int = length (1 :: 3 :: 9 :: []) *) fun main () = return <xml> <head> <title>Type Classes in Ur/Web</title> </head> <body> <h1>Type Classes</h1> <p> Ur/Web includes a type class mechanism for controlling ad hoc polymorphism. </p> <h2> An illustracion of the Measurable class on strings and lists. </h2> <p> Here we see length "Ur/Web" = {[length "Ur/Web"]} </p> <p> Here we see length ("a" :: "b" :: "C" :: []) = {[length ("a" :: "b" :: "C" :: [])]} </p> </body> </xml>
We can have instances polymorphic over the type held in our lists.
(* * Type class polymorphic over type of list *) structure Measurable : sig class measurable val length : t ::: Type -> measurable t -> t -> int val measurable_list : t ::: Type -> measurable (list t) end = struct class measurable t = t -> int val length : t ::: Type -> measurable t -> t -> int = fn [t ::: Type] (m : measurable t) => m (* * Here we copy listlength for sake of a self-contained example, but it is in the * library as List.length; you can get it by $/list *) val listlength = fn [a] => let fun length' acc (ls : list a) = case ls of [] => acc | _ :: ls => length' (acc + 1) ls in length' 0 end val measurable_list : t ::: Type -> measurable (list t) = fn [t ::: Type] => listlength end open Measurable fun main () = return <xml> <head> <title>Type Classes in Ur/Web</title> </head> <body> <h1>Type Classes</h1> <p> Ur/Web includes a type class mechanism for controlling ad hoc polymorphism. </p> <h2> An illustracion of the Measurable class polymorphic over lists. </h2> <p> Here we see length ("a" :: "b" :: "C" :: []) = {[length ("a" :: "b" :: "C" :: [])]} </p> <p> Here we see length (1 :: 2 :: 8 :: 2 :: []) = {[length (1 :: 2 :: 8 :: 2 :: [])]} </p> </body> </xml>