diff tests/type_class.ur @ 674:fab5998b840e

Type class reductions, but no inclusions yet
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Mar 2009 14:37:31 -0400
parents 71bafe66dbe1
children 43430b7190f4
line wrap: on
line diff
--- a/tests/type_class.ur	Tue Mar 24 15:35:46 2009 -0400
+++ b/tests/type_class.ur	Thu Mar 26 14:37:31 2009 -0400
@@ -1,18 +1,48 @@
-class default t = t
+datatype pair a b = Pair of a * b
 
-val string_default : default string = "Hi"
-val int_default : default int = 0
+structure M : sig
+    class default
+    val get : t ::: Type -> default t -> t
 
-val default : t :: Type -> default t -> t =
-        fn t :: Type => fn d : default t => d
-val hi = default [string] _
-val zero = default [int] _
+    val string_default : default string
+    val int_default : default int
 
-val frob : t :: Type -> default t -> t =
-        fn t :: Type => fn _ : default t => default [t] _
-val hi_again = frob [string] _
-val zero_again = frob [int] _
+    val option_default : t ::: Type -> default t -> default (option t)
+    val pair_default : a ::: Type -> b ::: Type -> default a -> default b -> default (pair a b)
+end = struct
+    class default t = t
+    fun get (t ::: Type) (x : t) = x
 
-val main : unit -> page = fn () => <html><body>
-        {cdata hi_again}
-</body></html>
+    val string_default = "Hi"
+    val int_default = 0
+
+    fun option_default (t ::: Type) (x : t) = Some x
+    fun pair_default (a ::: Type) (b ::: Type) (x : a) (y : b) = Pair (x, y)
+end
+
+open M
+
+fun default (t ::: Type) (_ : default t) : t = get
+val hi : string = default
+val zero : int = default
+val some_zero : option int = default
+val hi_zero : pair string int = default
+
+fun frob (t ::: Type) (_ : default t) : t = default
+val hi_again : string = frob
+val zero_again : int = frob
+
+fun show_option (t ::: Type) (_ : show t) : show (option t) =
+    mkShow (fn x =>
+               case x of
+                   None => "None"
+                 | Some y => show y)
+
+fun show_pair (a ::: Type) (b ::: Type) (_ : show a) (_ : show b) : show (pair a b) =
+    mkShow (fn x =>
+               case x of
+                   Pair (y, z) => "(" ^ show y ^ "," ^ show z ^ ")")
+
+fun main () : transaction page = return <xml><body>
+  {[hi_again]}, {[zero_again]}, {[some_zero]}, {[hi_zero]}
+</body></xml>