Mercurial > urweb
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 |