adam@1504: (* Chapter 2: Type-Level Computation *)
adam@1504:
adam@1505: (* begin hide *)
adam@1505: val show_string = mkShow (fn s => "\"" ^ s ^ "\"")
adam@1505: (* end *)
adam@1505:
adam@1504: (* This tutorial by Adam Chlipala is licensed under a Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 Unported License. *)
adam@1504:
adam@1504: (* 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:
adam@1504: (* * Names and Records *)
adam@1504:
adam@1504: (* Last chapter, we met Ur's basic record features, including record construction and field projection. *)
adam@1504:
adam@1504: val r = { A = 0, B = 1.2, C = "hi"}
adam@1504:
adam@1504: (* begin eval *)
adam@1504: r.B
adam@1504: (* end *)
adam@1504:
adam@1504: (* 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:
adam@1504: fun project [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (r : $([nm = t] ++ ts)) : t = r.nm
adam@1504:
adam@1504: (* begin eval *)
adam@1504: project [#B] r
adam@1504: (* end *)
adam@1504:
adam@1504: (* This function introduces a slew of essential features. First, we see type parameters with explicit kind annotations. Formal parameter syntax like [a :: K] declares an explicit parameter a of kind K. Explicit parameters must be passed explicitly at call sites. In contrast, implicit parameters, declared like [a ::: K], are inferred in the usual way.
adam@1504:
adam@1504: Two new kinds appear in this example. We met the basic kind Type in a previous example. Here we meet Name, the kind of record field names; and {Type} the type of finite maps from field names to types, where we'll generally refer to this notion of "finite map" by the name record, 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 at the level of types that exist only at compile time! By the way, the kind {Type} is one example of the general {K} kind form, which refers to records with fields of kind K.
adam@1504:
adam@1504: The English description of project is that it projects a field with name nm and type t out of a record r whose other fields are described by type-level record ts. We make all this formal by assigning r a type that first builds the singleton record [nm = t] that maps nm to t, and then concatenating this record with the remaining field information in ts. The $ operator translates a type-level record (of kind {Type}) into a record type (of kind Type).
adam@1504:
adam@1504: The type annotation on r uses the record concatenation operator ++. 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 ++ as non-commutative, if we are to maintain the nice modularity properties of polymorphism. However, treating ++ 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.
adam@1504:
adam@1504: For a polymorphic function like project, the compiler doesn't know which fields a type-level record variable like ts contains. To enable self-contained type-checking, we need to declare some constraints about field disjointness. That's exactly the meaning of syntax like [r1 ~ r2], which asserts disjointness of two type-level records. The disjointness clause for project asserts that the name nm is not used by ts. The syntax [nm] is shorthand for [nm = ()], which defines a singleton record of kind {Unit}, where Unit is the degenerate kind inhabited only by the constructor ().
adam@1504:
adam@1504: The last piece of this puzzle is the easiest. In the example call to project, we see that the only parameters passed are the one explicit constructor parameter nm and the value-level parameter r. The rest are inferred, and the disjointness proof obligation is discharged automatically. The syntax #A denotes the constructor standing for first-class field name A, 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 [A = c, ..., A = c]). *)
adam@1505:
adam@1505:
adam@1505: (* * Basic Type-Level Programming *)
adam@1505:
adam@1505: (* 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:
adam@1505: con id = fn t :: Type => t
adam@1505:
adam@1505: val x : id int = 0
adam@1505: val x : id float = 1.2
adam@1505:
adam@1505: con pair = fn t :: Type => t * t
adam@1505:
adam@1505: val x : pair int = (0, 1)
adam@1505: val x : pair float = (1.2, 2.3)
adam@1505:
adam@1505: con compose = fn (f :: Type -> Type) (g :: Type -> Type) (t :: Type) => f (g t)
adam@1505:
adam@1505: val x : compose pair pair int = ((0, 1), (2, 3))
adam@1505:
adam@1505: con fst = fn t :: (Type * Type) => t.1
adam@1505: con snd = fn t :: (Type * Type) => t.2
adam@1505:
adam@1505: con p = (int, float)
adam@1505: val x : fst p = 0
adam@1505: val x : snd p = 1.2
adam@1505:
adam@1505: con mp = fn (f :: Type -> Type) (t1 :: Type, t2 :: Type) => (f t1, f t2)
adam@1505:
adam@1505: val x : fst (mp pair p) = (1, 2)
adam@1505:
adam@1505: (* 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 let-polymorphism, via kind polymorphism, which we can use to make some of the definitions above more generic. *)
adam@1505:
adam@1505: con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1
adam@1505: con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2
adam@1505:
adam@1505: con twoFuncs :: ((Type -> Type) * (Type -> Type)) = (id, compose pair pair)
adam@1505:
adam@1505: val x : fst twoFuncs int = 0
adam@1505: val x : snd twoFuncs int = ((1, 2), (3, 4))
adam@1505:
adam@1505:
adam@1505: (* * Type-Level Map *)
adam@1505:
adam@1505: (* The examples from the same section may seem cute but not especially useful. In this section, we meet map, 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 map. *)
adam@1505:
adam@1505: con r = [A = int, B = float, C = string]
adam@1505:
adam@1505: con optionify = map option
adam@1505: val x : $(optionify r) = {A = Some 1, B = None, C = Some "hi"}
adam@1505:
adam@1505: con pairify = map pair
adam@1505: val x : $(pairify r) = {A = (1, 2), B = (3.0, 4.0), C = ("5", "6")}
adam@1505:
adam@1505: con stringify = map (fn _ => string)
adam@1505: val x : $(stringify r) = {A = "1", B = "2", C = "3"}
adam@1505:
adam@1505: (* 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 map and ++. 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:
adam@1505: fun concat [f :: Type -> Type] [r1 :: {Type}] [r2 :: {Type}] [r1 ~ r2]
adam@1505: (r1 : $(map f r1)) (r2 : $(map f r2)) : $(map f (r1 ++ r2)) = r1 ++ r2
adam@1505:
adam@1505:
adam@1505: (* * First-Class Polymorphism *)
adam@1505:
adam@1505: (* The idea of first-class polymorphism or impredicative polymorphism 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:
adam@1505: type nat = t :: Type -> t -> (t -> t) -> t
adam@1505: val zero : nat = fn [t :: Type] (z : t) (s : t -> t) => z
adam@1505: fun succ (n : nat) : nat = fn [t :: Type] (z : t) (s : t -> t) => s (n [t] z s)
adam@1505:
adam@1505: val one = succ zero
adam@1505: val two = succ one
adam@1505: val three = succ two
adam@1505:
adam@1505: (* begin eval *)
adam@1505: three [int] 0 (plus 1)
adam@1505: (* end *)
adam@1505:
adam@1505: (* begin eval *)
adam@1505: three [string] "" (strcat "!")
adam@1505: (* end *)