Polymorphic Variants Usage Example
From Impredicative Wiki
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>