|
adam@1504
|
1 (* Chapter 2: Type-Level Computation *)
|
|
adam@1504
|
2
|
|
adam@1505
|
3 (* begin hide *)
|
|
adam@1505
|
4 val show_string = mkShow (fn s => "\"" ^ s ^ "\"")
|
|
adam@1505
|
5 (* end *)
|
|
adam@1505
|
6
|
|
adam@1504
|
7 (* This tutorial by <a href="http://adam.chlipala.net/">Adam Chlipala</a> is licensed under a <a href="http://creativecommons.org/licenses/by-nc-nd/3.0/">Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 Unported License</a>. *)
|
|
adam@1504
|
8
|
|
adam@1504
|
9 (* The last chapter reviewed some Ur features imported from ML and Haskell. This chapter explores uncharted territory, introducing the features that make Ur unique. *)
|
|
adam@1504
|
10
|
|
adam@1504
|
11 (* * Names and Records *)
|
|
adam@1504
|
12
|
|
adam@1504
|
13 (* Last chapter, we met Ur's basic record features, including record construction and field projection. *)
|
|
adam@1504
|
14
|
|
adam@1504
|
15 val r = { A = 0, B = 1.2, C = "hi"}
|
|
adam@1504
|
16
|
|
adam@1504
|
17 (* begin eval *)
|
|
adam@1504
|
18 r.B
|
|
adam@1504
|
19 (* end *)
|
|
adam@1504
|
20
|
|
adam@1504
|
21 (* Our first taste of Ur's novel expressive power is with the following function, which implements record field projection in a completely generic way. *)
|
|
adam@1504
|
22
|
|
adam@1504
|
23 fun project [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (r : $([nm = t] ++ ts)) : t = r.nm
|
|
adam@1504
|
24
|
|
adam@1504
|
25 (* begin eval *)
|
|
adam@1504
|
26 project [#B] r
|
|
adam@1504
|
27 (* end *)
|
|
adam@1504
|
28
|
|
adam@1504
|
29 (* This function introduces a slew of essential features. First, we see type parameters with explicit kind annotations. Formal parameter syntax like <tt>[a :: K]</tt> declares an <b>explicit</b> parameter <tt>a</tt> of kind <tt>K</tt>. Explicit parameters must be passed explicitly at call sites. In contrast, implicit parameters, declared like <tt>[a ::: K]</tt>, are inferred in the usual way.<br>
|
|
adam@1504
|
30 <br>
|
|
adam@1504
|
31 Two new kinds appear in this example. We met the basic kind <tt>Type</tt> in a previous example. Here we meet <tt>Name</tt>, the kind of record field names; and <tt>{Type}</tt> the type of finite maps from field names to types, where we'll generally refer to this notion of "finite map" by the name <b>record</b>, as it will be clear from context whether we're discussing type-level or value-level records. That is, in this case, we are referring to names and records <b>at the level of types</b> that <b>exist only at compile time</b>! By the way, the kind <tt>{Type}</tt> is one example of the general <tt>{K}</tt> kind form, which refers to records with fields of kind <tt>K</tt>.<br>
|
|
adam@1504
|
32 <br>
|
|
adam@1504
|
33 The English description of <tt>project</tt> is that it projects a field with name <tt>nm</tt> and type <tt>t</tt> out of a record <tt>r</tt> whose other fields are described by type-level record <tt>ts</tt>. We make all this formal by assigning <tt>r</tt> a type that first builds the singleton record <tt>[nm = t]</tt> that maps <tt>nm</tt> to <tt>t</tt>, and then concatenating this record with the remaining field information in <tt>ts</tt>. The <tt>$</tt> operator translates a type-level record (of kind <tt>{Type}</tt>) into a record type (of kind <tt>Type</tt>).<br>
|
|
adam@1504
|
34 <br>
|
|
adam@1504
|
35 The type annotation on <tt>r</tt> uses the record concatenation operator <tt>++</tt>. Ur enforces that any concatenation happens between records that share no field names. Otherwise, we'd need to resolve field name ambiguity in some predictable way, which would force us to treat <tt>++</tt> as non-commutative, if we are to maintain the nice modularity properties of polymorphism. However, treating <tt>++</tt> as commutative, and treating records as equal up to field permutation in general, are very convenient for type inference and general programmer experience. Thus, we enforce disjointness to keep things simple.<br>
|
|
adam@1504
|
36 <br>
|
|
adam@1504
|
37 For a polymorphic function like <tt>project</tt>, the compiler doesn't know which fields a type-level record variable like <tt>ts</tt> contains. To enable self-contained type-checking, we need to declare some constraints about field disjointness. That's exactly the meaning of syntax like <tt>[r1 ~ r2]</tt>, which asserts disjointness of two type-level records. The disjointness clause for <tt>project</tt> asserts that the name <tt>nm</tt> is not used by <tt>ts</tt>. The syntax <tt>[nm]</tt> is shorthand for <tt>[nm = ()]</tt>, which defines a singleton record of kind <tt>{Unit}</tt>, where <tt>Unit</tt> is the degenerate kind inhabited only by the constructor <tt>()</tt>.<br>
|
|
adam@1504
|
38 <br>
|
|
adam@1504
|
39 The last piece of this puzzle is the easiest. In the example call to <tt>project</tt>, we see that the only parameters passed are the one explicit constructor parameter <tt>nm</tt> and the value-level parameter <tt>r</tt>. The rest are inferred, and the disjointness proof obligation is discharged automatically. The syntax <tt>#A</tt> denotes the constructor standing for first-class field name <tt>A</tt>, and we pass all constructor parameters to value-level functions within square brackets (which bear no formal relation to the syntax for type-level record literals <tt>[A = c, ..., A = c]</tt>). *)
|
|
adam@1505
|
40
|
|
adam@1505
|
41
|
|
adam@1505
|
42 (* * Basic Type-Level Programming *)
|
|
adam@1505
|
43
|
|
adam@1505
|
44 (* To help us express more interesting operations over records, we will need to do some type-level programming. Ur makes that fairly congenial, since Ur's constructor level includes an embedded copy of the simply-typed lambda calculus. Here are a few examples. *)
|
|
adam@1505
|
45
|
|
adam@1505
|
46 con id = fn t :: Type => t
|
|
adam@1505
|
47
|
|
adam@1505
|
48 val x : id int = 0
|
|
adam@1505
|
49 val x : id float = 1.2
|
|
adam@1505
|
50
|
|
adam@1505
|
51 con pair = fn t :: Type => t * t
|
|
adam@1505
|
52
|
|
adam@1505
|
53 val x : pair int = (0, 1)
|
|
adam@1505
|
54 val x : pair float = (1.2, 2.3)
|
|
adam@1505
|
55
|
|
adam@1505
|
56 con compose = fn (f :: Type -> Type) (g :: Type -> Type) (t :: Type) => f (g t)
|
|
adam@1505
|
57
|
|
adam@1505
|
58 val x : compose pair pair int = ((0, 1), (2, 3))
|
|
adam@1505
|
59
|
|
adam@1505
|
60 con fst = fn t :: (Type * Type) => t.1
|
|
adam@1505
|
61 con snd = fn t :: (Type * Type) => t.2
|
|
adam@1505
|
62
|
|
adam@1505
|
63 con p = (int, float)
|
|
adam@1505
|
64 val x : fst p = 0
|
|
adam@1505
|
65 val x : snd p = 1.2
|
|
adam@1505
|
66
|
|
adam@1505
|
67 con mp = fn (f :: Type -> Type) (t1 :: Type, t2 :: Type) => (f t1, f t2)
|
|
adam@1505
|
68
|
|
adam@1505
|
69 val x : fst (mp pair p) = (1, 2)
|
|
adam@1505
|
70
|
|
adam@1505
|
71 (* Actually, Ur's constructor level goes further than merely including a copy of the simply-typed lambda calculus with tuples. We also effectively import classic <b>let-polymorphism</b>, via <b>kind polymorphism</b>, which we can use to make some of the definitions above more generic. *)
|
|
adam@1505
|
72
|
|
adam@1505
|
73 con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1
|
|
adam@1505
|
74 con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2
|
|
adam@1505
|
75
|
|
adam@1505
|
76 con twoFuncs :: ((Type -> Type) * (Type -> Type)) = (id, compose pair pair)
|
|
adam@1505
|
77
|
|
adam@1505
|
78 val x : fst twoFuncs int = 0
|
|
adam@1505
|
79 val x : snd twoFuncs int = ((1, 2), (3, 4))
|
|
adam@1505
|
80
|
|
adam@1505
|
81
|
|
adam@1505
|
82 (* * Type-Level Map *)
|
|
adam@1505
|
83
|
|
adam@1505
|
84 (* The examples from the same section may seem cute but not especially useful. In this section, we meet <tt>map</tt>, the real workhorse of Ur's type-level computation. We'll use it to type some useful operations over value-level records. A few more pieces will be necessary before getting there, so we'll start just by showing how interesting type-level operations on records may be built from <tt>map</tt>. *)
|
|
adam@1505
|
85
|
|
adam@1505
|
86 con r = [A = int, B = float, C = string]
|
|
adam@1505
|
87
|
|
adam@1505
|
88 con optionify = map option
|
|
adam@1505
|
89 val x : $(optionify r) = {A = Some 1, B = None, C = Some "hi"}
|
|
adam@1505
|
90
|
|
adam@1505
|
91 con pairify = map pair
|
|
adam@1505
|
92 val x : $(pairify r) = {A = (1, 2), B = (3.0, 4.0), C = ("5", "6")}
|
|
adam@1505
|
93
|
|
adam@1505
|
94 con stringify = map (fn _ => string)
|
|
adam@1505
|
95 val x : $(stringify r) = {A = "1", B = "2", C = "3"}
|
|
adam@1505
|
96
|
|
adam@1505
|
97 (* We'll also give our first hint at the cleverness within Ur's type inference engine. The following definition type-checks, despite the fact that doing so requires applying several algebraic identities about <tt>map</tt> and <tt>++</tt>. This is the first point where we see a clear advantage of Ur over the type-level computation facilities that have become popular in GHC Haskell. *)
|
|
adam@1505
|
98
|
|
adam@1505
|
99 fun concat [f :: Type -> Type] [r1 :: {Type}] [r2 :: {Type}] [r1 ~ r2]
|
|
adam@1505
|
100 (r1 : $(map f r1)) (r2 : $(map f r2)) : $(map f (r1 ++ r2)) = r1 ++ r2
|
|
adam@1505
|
101
|
|
adam@1505
|
102
|
|
adam@1505
|
103 (* * First-Class Polymorphism *)
|
|
adam@1505
|
104
|
|
adam@1505
|
105 (* The idea of <b>first-class polymorphism</b> or <b>impredicative polymorphism</b> has also become popular in GHC Haskell. This feature, which has a long history in type theory, is also central to Ur's metaprogramming facilities. First-class polymorphism goes beyond Hindley-Milner's let-polymorphism to allow arguments to functions to themselves be polymorphic. Among other things, this enables the classic example of Church encodings, as for the natural numbers in this example. *)
|
|
adam@1505
|
106
|
|
adam@1505
|
107 type nat = t :: Type -> t -> (t -> t) -> t
|
|
adam@1505
|
108 val zero : nat = fn [t :: Type] (z : t) (s : t -> t) => z
|
|
adam@1505
|
109 fun succ (n : nat) : nat = fn [t :: Type] (z : t) (s : t -> t) => s (n [t] z s)
|
|
adam@1505
|
110
|
|
adam@1505
|
111 val one = succ zero
|
|
adam@1505
|
112 val two = succ one
|
|
adam@1505
|
113 val three = succ two
|
|
adam@1505
|
114
|
|
adam@1505
|
115 (* begin eval *)
|
|
adam@1505
|
116 three [int] 0 (plus 1)
|
|
adam@1505
|
117 (* end *)
|
|
adam@1505
|
118
|
|
adam@1505
|
119 (* begin eval *)
|
|
adam@1505
|
120 three [string] "" (strcat "!")
|
|
adam@1505
|
121 (* end *)
|
