Basic Examples of the Type Class Mechanism in Ur/Web

From Impredicative Wiki
Jump to: navigation, search

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>
Personal tools