Abstract and Concrete Type Classes

From Impredicative Wiki
Revision as of 17:29, 13 December 2010 by Karn Kallio (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

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