comparison tests/type_class.ur @ 677:81573f62d6c3

Enforce termination of type class instances
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Mar 2009 15:54:04 -0400
parents 43430b7190f4
children
comparison
equal deleted inserted replaced
676:e0c186464612 677:81573f62d6c3
8 val int_default : default int 8 val int_default : default int
9 9
10 val option_default : t ::: Type -> default t -> default (option t) 10 val option_default : t ::: Type -> default t -> default (option t)
11 val pair_default : a ::: Type -> b ::: Type -> default a -> default b -> default (pair a b) 11 val pair_default : a ::: Type -> b ::: Type -> default a -> default b -> default (pair a b)
12 12
13 (*val uh_oh : t ::: Type -> default t -> default t*)
14
13 class awesome 15 class awesome
14 val awesome_default : t ::: Type -> awesome t -> default t 16 val awesome_default : t ::: Type -> awesome t -> default t
15 17
16 val float_awesome : awesome float 18 val float_awesome : awesome float
19
20 val oh_my : t ::: Type -> awesome (option t) -> awesome (option t)
21
22 val awesome : t ::: Type -> awesome t -> t
17 end = struct 23 end = struct
18 class default t = t 24 class default t = t
19 fun get (t ::: Type) (x : t) = x 25 fun get (t ::: Type) (x : t) = x
20 26
21 val string_default = "Hi" 27 val string_default = "Hi"
22 val int_default = 0 28 val int_default = 0
23 29
24 fun option_default (t ::: Type) (x : t) = Some x 30 fun option_default (t ::: Type) (x : t) = Some x
25 fun pair_default (a ::: Type) (b ::: Type) (x : a) (y : b) = Pair (x, y) 31 fun pair_default (a ::: Type) (b ::: Type) (x : a) (y : b) = Pair (x, y)
26 32
33 (*fun uh_oh (t ::: Type) (x : t) = x*)
34
27 class awesome t = t 35 class awesome t = t
28 fun awesome_default (t ::: Type) (x : t) = x 36 fun awesome_default (t ::: Type) (x : t) = x
29 37
30 val float_awesome = 1.23 38 val float_awesome = 1.23
39
40 fun oh_my (t ::: Type) (x : option t) = x
41
42 fun awesome (t ::: Type) (x : t) = x
31 end 43 end
32 44
33 open M 45 open M
34 46
35 fun default (t ::: Type) (_ : default t) : t = get 47 fun default (t ::: Type) (_ : default t) : t = get
47 mkShow (fn x => 59 mkShow (fn x =>
48 case x of 60 case x of
49 None => "None" 61 None => "None"
50 | Some y => show y) 62 | Some y => show y)
51 63
64 (*val x : option float = awesome*)
65
52 fun show_pair (a ::: Type) (b ::: Type) (_ : show a) (_ : show b) : show (pair a b) = 66 fun show_pair (a ::: Type) (b ::: Type) (_ : show a) (_ : show b) : show (pair a b) =
53 mkShow (fn x => 67 mkShow (fn x =>
54 case x of 68 case x of
55 Pair (y, z) => "(" ^ show y ^ "," ^ show z ^ ")") 69 Pair (y, z) => "(" ^ show y ^ "," ^ show z ^ ")")
56 70