Polymorphic Variants Usage Example

From Impredicative Wiki
Jump to: navigation, search

The Ur/Web record calculus contains polymorphic variants. Below is a small example of usage of make and match, as well as a little discussion.

(* Given a row type there are two associated types: record types and variant types. *)

(* Starting with the row type rr *)

con rr :: {Type} = [Foo = int, Bar = string]

(* we can make a record type codatarr (using $) or a variant type datarr (using variant) *)

con codatarr :: Type = $rr
con datarr :: Type = variant rr

(* The record type codatarr describes codata; values of type $rr can be broken down into
 * their components.  Each value of type codatarr must accept both the destructors
 * Foo and Bar, returning values that are ints or strings respectively.
 *
 * The variant type datarr describes data; values of type variant rr can be built from
 * components.  Each value of type datarr has been made by applying either the Foo or Bar
 * constructor to an int or string respectively.
 *)

(* Ur/Web also permits the construction of data types via the datatype declaration.
 * Here is a sample showing usage of variants with the algebraic datatype parallel.
 *)

(* Let us make a variant type of playing card suits. *)

con cardsuits :: {Unit} = [Club, Diamond, Heart, Spade]
con cardsuit :: Type = variant (mapU unit cardsuits)

(* We can make the parallel algebraic datatype *)

datatype cardsuitalg = Club | Diamond | Heart | Spade

(* Here is a diamond *)

val diamond = make [#Diamond] ()
val diamond' = Diamond

(* Here is how to match by cases on a variant *)

val namecase = {Club = (fn (_ : unit) => "club"),
                Diamond = (fn (_ : unit) => "diamond"),
                Heart = (fn (_ : unit) => "heart"),
                Spade = (fn (_ : unit) => "spade")}

val diamondname = match diamond namecase

(* The algebraic version could be like this *)

fun cardname card =
    case card of
        Club => "club"
      | Diamond => "diamond"
      | Heart => "heart"
      | Spade => "spade"

val diamondname' = cardname diamond'

(* Now let us show polymorphism. We make two variant types sharing a constructor Medium *)

con temps :: {Unit} = [Hot, Medium, Cold]
con temp :: Type = variant (mapU unit temps)

con sizes :: {Unit} = [Large, Medium, Small]
con size :: Type = variant (mapU unit sizes)

val tempcase = {Hot = (fn (_ : unit) => 10),
                Medium = (fn (_ : unit) => 5),
                Cold = (fn (_ : unit) => 1)}

val sizecase = {Large = (fn (_ : unit) => 8),
                Medium = (fn (_ : unit) => 4),
                Small = (fn (_ : unit) => 2)}

(* Here medium1 and medium2 have undetermined types; polymorphic variants mean the types will
 * be determined according to the usage *)

val medium1 = make [#Medium] ()
val medium2 = make [#Medium] ()

(* This usage allows type unification *)

val mediumtemp = match medium1 tempcase
val mediumsize = match medium2 sizecase

(* Now let us try via datatype declaration.  Here are two algebraic datatypes sharing the Medium constructor *)

datatype temp = Hot | Medium | Cold
datatype size = Large | Medium | Small

(* What type will the values constructed by Medium have? *)

(* The commented out functions below do not compile .. the Medium constructor is not polymorphic;
 * it must "decide" on one of temp or size type
 *)

(*
fun tempvalue temp =
    case temp of
        Hot => 10
      | Medium => 5
      | Cold => 1

fun sizevalue size =
    case size of
        Large => 8
      | Medium => 4
      | Small => 2
*)

(* The novelty of polymorphic variants over algebraic datatypes is that with polymorphic variants
 * it is possible to express values with partial types *)

fun main () = return <xml>
  <head>
    <title>Variant types</title>
  </head>
  <body>
    <h1>Variant Types</h1>
    <p>
      The Ur/Web record calculus includes variant types.
    </p>
    <p>
      diamondname = {[diamondname]} <br/>
      diamondname' = {[diamondname']} <br/>
      mediumtemp = {[mediumtemp]} <br/>
      mediumsize = {[mediumsize]}
    </p>
  </body>
</xml>
Personal tools