Additional Exercises for Practical Foundations for Programming Languages (Second Edition) Robert Harper Carnegie Mellon University May 11, 2020
1
System T
The use of the recursor, rather than the iterator, as the elimination form for the type nat is necessary, for practical reasons, but unfortunate because it is essentially an ad hoc use of product types.
Exercises 1. Give the statics and dynamics of the iteration construct for T. 2. Define the predecessor operation on natural numbers using only iteration. (The predecessor of z is z, and of s( e ) is e.)
Solutions 1.
Γ ` e : nat Γ ` e0 : τ Γ x : τ ` e : τ Γ ` iter e {z ,→ e0 | s( x ) ,→ e1 } : τ iter z {z ,→ e0 | s( x ) ,→ e1 } 7−→ e0
(1) (2)
iter s( e ) {z ,→ e0 | s( x ) ,→ e1 } 7−→ [iter e {z ,→ e0 | s( x ) ,→ e1 }/x ]e1 e 7−→ e0 iter e {z ,→ e0 | s( x ) ,→ e1 } 7−→ iter e0 {z ,→ e0 | s( x ) ,→ e1 } 1
(3) (4)
2. It is not directly definable using only the iterator, because it does not provide access to the predecessor. The simplest solution seems to be to define a pairing function on the natural numbers with which one can simulate the solution using products. (Whether it is possible to define pairing using only iteration needs to be checked; it involves defining basic arithmetic operations that plausibly need only iteration.)
2
Sums and Products
2.1
Algebraic Structure
There is a rich algebraic structure given by type isomorphisms involving sum and product types. At this early stage it is not possible to prove these results rigorously, but informally one may show that sum and product types each form a commutative monoid (up to isomorphism), and that the product distributes over sum. Using suggestive notations such as n for the n-fold sum of the type 1 with itself, one can show that the rules of grade school algebra hold as isomorphisms of types. Type constructors have a functorial action on maps, which is explored in the following questions.
Exercises 1. For f 1 : σ1 → τ1 and f 2 : σ2 → τ2 , define the following functions: (a) 1 : 1 → 1. (b) f 1 × f 2 : ( σ1 × σ2 ) → ( τ1 × τ2 ). 2. For f 1 : σ1 → τ1 and f 2 : σ2 → τ2 , define the following functions: (a) 0 : 0 → 0. (b) f 1 + f 2 : ( σ1 + σ2 ) → ( τ1 + τ2 ).
Solutions 1.
(a) 1 , λ ( : 1 ) hi. (b) f 1 × f 2 , λ ( x : σ1 × σ2 ) h f 1 ( x · l ), f 2 ( x · r )i.
2.
(a) 0 , λ ( x : 0 ) case x { }. (b) f 1 + f 2 , λ ( x : σ1 + σ2 ) case x {l · x1 ,→ l · f 1 ( x1 ) | r · x2 ,→ r · f 2 ( x2 )}.
Define σ ∼ = τ to mean there exists f : σ → τ and g : τ → σ that are, informally, mutually inverses. Argue that the following congruences are valid in the extension of T with nullary and binary products and sums. 2
Exercises 1.
(a) σ ∼ = σ. (b) If σ ∼ = τ, then τ ∼ = σ. ∼ ∼ (c) If ρ = σ and σ = τ, then ρ ∼ = τ. ∼ (d) σ × τ = τ × σ. (e) ρ × ( σ × τ ) ∼ = ( ρ × σ ) × τ. ∼ (f) σ + τ = τ + σ. (g) ρ + ( σ + τ ) ∼ = ( ρ + σ ) + τ. ∼ (h) 1 × τ = τ. (i) 0 + τ ∼ = τ. (j) ρ × ( σ + τ ) ∼ = ( ρ × σ ) + ( ρ × τ ).
2.
(a) If σ1 ∼ = τ1 and σ1 ∼ (b) If σ1 = τ1 and σ1 (c) If σ1 ∼ = τ1 and σ1
3.
(a) σ → ( τ1 × τ2 ) ∼ = ( σ → τ1 ) × ( σ → τ2 ). (b) ( σ1 + σ2 ) → τ ∼ = ( σ1 → τ ) × ( σ2 → τ ).
∼ = τ2 , then σ1 × σ2 ∼ = τ1 × τ2 . ∼ = τ2 , then σ1 + σ2 ∼ = τ1 + τ2 . ∼ = τ2 , then σ1 → σ2 ∼ = τ1 → τ2 .
(c) σ → 1 ∼ = 1. (d) σ → 0 ∼ = 0, provided that σ is inhabited. (e) 0 → τ ∼ = 1. (f) 1 → τ ∼ = τ. 4.
(a) Define 2 to be 1 + 1. Show that 2 × τ ∼ = τ + τ. More generally, defining n to be the n-fold sum of 1, show by induction on n that n×τ ∼ + . . . + τ. =τ | {z } n
(b) Define to be τ × τ. Show that τ 2 ∼ = 2 → τ. More generally, show n ∼ that τ = n → τ, where n is the n-fold sum of 1 as defined above. In particular, τ 0 ∼ = 1. ∼ τ 2 + 2 × τ + 1. In other words, τ opt ∼ (c) Show that ( τ + 1 )2 = = √ 2 τ + 2 × τ + 1. τ2
Solutions 1.
(a) Form the pair hλ ( x : σ ) x, λ ( x : σ ) x i. (b) Given h f , gi : σ ∼ = τ, form h g, f i : τ ∼ = σ. (c) Given h f , gi : ρ ∼ = σ and hh, i i : σ ∼ = ρ, form hh ◦ f , i ◦ gi : ρ ∼ = τ. 3
(d) Form the pair hλ ( h x, yi . hy, x i ), λ ( hy, x i . h x, yi )i : σ × τ ∼ = τ × σ. (e) Form the pair hλ ( h x, hy, zii . hh x, yi, zi ), λ ( hh x, yi, zi . h x, hy, zii )i. (f) Form the pair h f , gi, where i. f , λ ( x : σ + τ ) case x {l · x1 ,→ r · x1 | r · x2 ,→ l · x2 }, and ii. g , λ ( x : τ + σ ) case y {l · y1 ,→ r · y1 | r · y2 ,→ l · y2 }. (g) Perform a nested case analysis, and reconstruct using the re-organized injections. (h) Form the pair hλ ( hhi, x i . x ), λ ( x : τ ) hhi, x ii. (i) Form the pair
hλ ( 0 + τ : x ) case x {l · x1 ,→ case x1 { } | r · x2 ,→ x2 }, λ ( x : τ ) r · x i. (j) Form the pair h f , gi, where i. f , λ ( h x, yi . case y {l · y1 ,→ l · h x, y1 i | r · y2 ,→ r · h x, y2 i} ), and ii. g , λ ( z : ( ρ × σ ) + ( ρ × τ ) ) case z {l · h x, yi ,→ h x, l · yi | r · h x, zi ,→ h x, r · zi}. 2.
(a) Given h f 1 , g1 i : σ1 ∼ = τ1 and h f 2 , g2 i : σ2 ∼ = τ2 , form h f 1 × f 2 , g1 × g2 i, and check that it is an isomorphism pair. (b) Given h f 1 , g1 i : σ1 ∼ = τ1 and h f 2 , g2 i : σ2 ∼ = τ2 , form h f 1 + f 2 , g1 + g2 i, and check that it is an isomorphism pair. (c) Given h f 1 , g1 i : σ1 ∼ = τ1 and h f 2 , g2 i : σ2 ∼ = τ2 , form h f 1 → f 2 , g1 → g2 i, and check that it is an isomorphism pair.
3.
(a) Form the pair h f , gi, where i. f , λ ( x : σ → ( τ1 × τ2 ) ) hλ ( x : σ ) x · l, λ ( x : σ ) x · ri. ii. g , λ ( hz1 , z2 i . λ ( x : σ ) hz1 ( x ), z2 ( x )i ). (b) Form the pair h f , gi, where i. f , λ ( x : ( σ1 + σ2 ) → τ ) hλ ( x1 : σ1 ) x ( l · x1 ), λ ( x2 : σ2 ) x ( r · x2 )i. ii. g , λ ( hz1 , z2 i . λ ( x : σ1 + σ2 ) case x {l · x1 ,→ z · l( x1 ) | r · x2 ,→ z · r( x2 )} ). (c) Form the pair hλ ( z : σ → 1 ) hi, λ ( : 1 ) λ ( : σ ) hii. (d) Form the pair hλ ( z : σ → 0 ) z( eσ ), λ ( z : 0 ) case z { }i, where eσ : σ. (e) Form the pair hλ ( z : 0 → τ ) hi, λ ( z : 1 ) λ ( x : 0 ) case x { }i. (f) Form the pair hλ ( z : 1 → τ ) z( hi ), λ ( x : 1 ) λ ( y : 1 ) x i.
4.
(a) Using the foregoing isomorphisms, show that 2 × τ ∼ = τ + τ: 2×τ ∼ = (1+1)×τ ∼ = (1×τ)+(1×τ) ∼ = τ + τ. 4
(b) Using the foregoing isomorphisms, show that τ 2 ∼ = 2 → τ: 2→τ∼ = (1+1) → τ
∼ = (1 → τ)×(1 → τ) ∼ = τ×τ = τ2 . (c) Using the foregoing isomorphisms, show that τ opt ∼ =
√
τ 2 + 2 × τ + 1:
( τ opt )2 = ( τ + 1 )2 ∼ = (τ +1)×(τ +1) ∼ = ((τ +1)×τ)+((τ +1)×1) ∼ = ((τ ×τ)+(1×τ))+((1×τ)+(1×1)) ∼ = τ2 + ( τ + τ ) + 1 ∼ = τ2 + 2 × τ + 1
Classification Sums are used to classify the values of a type. For example, a complex number may be classified as either cartesian or polar, according to whether it is given by its ( x, y)-coordinates or its (ρ, θ )-coordinates. These two representations should not be confused; the cartesian and the polar are two classes of the type of complex numbers. Classes should not be confused with types, as is invariably done in object-oriented languages. First, let us define the types of complex numbers and of the operations on them. τ cplx = [ cart ,→ τ cart , pol ,→ τ pol ] τ cart = hx ,→ float, y ,→ floati τ pol = hr ,→ float, t ,→ floati ρopns = hquad ,→ ρquad , dist ,→ ρdist i ρquad = [ I, II, III, IV ] ρdist = float Thus, a complex number is either cartesian or polar, from which its squared distance from the origin or the quadrant may be determined. Let us analyze the essential structure of functions of type τ cplx → ρopns , which compute the operations on a complex number. The plan is to mimic the situation in linear algebra in which a linear transformation between vector spaces can be represented as a matrix. The algebra of products and sums allows us to formulate the foregoing function type as a matrix in two equivalent ways, isolating the essential content of such a mapping. Because the domain is a sum and the range is a product, the function type may be decomposed into a matrix in either row-major or column-major order. 5
Exercises 1. Give the class-first decomposition of the type τ cplx → ρopns as a product type: τ cplx → ρopns ∼ = ... 2. Give the operations-first decomposition of the type τ cplx → ρopns as a product type: τ cplx → ρopns ∼ = ...
Solutions 1. Give the class-first decomposition of the type τ cplx → ρopns as a product type: τ cplx → ρopns ∼ = hcart ,→ τ cart → ρopns , pol ,→ τ pol → ρopns i 2. Give the operations-first decomposition of the type τ cplx → ρopns as a product type: τ cplx → ρopns ∼ = hquad ,→ τ cplx → ρquad , dist ,→ τ cplx → ρdist i These decompositions involve four different function types to which the same decompositions may be applied to obtain product types:
Exercises 1. Give the product decomposition of the class-first component types: τ cart → ρopns ∼ = hquad ,→ τ cart → ρquad , dist ,→ τ cart → ρdist i τ pol → ρopns ∼ = hquad ,→ τ pol → ρquad , dist ,→ τ pol → ρdist i 2. Give the product decomposition of the operation-first component types: τ cplx → ρquad ∼ = hcart ,→ τ cart → ρquad , pol ,→ τ pol → ρquad i τ cplx → ρdist ∼ = hcart ,→ τ cart → ρdist , pol ,→ τ pol → ρdist i Combining these decompositions two different two-by-two matrix representations of the function type τ cplx → ρopns may be obtained. Neither organization is preferable or superior to the other; in fact, they are both isomorphic to the function type. 6
3
Generic Programming
The addition of variable types allows the formulation of type polynomials that obey many of the rules of algebra in the sense of type isomorphism. Type polynomials are central to the concept of generic, or type-directed, programming, which is induced by the functorial action of type constructors on mappings. The generic extension of a map along a polynomial type operator can be neatly expressed using the action of type constructors on maps. It is helpful to use the “curried” form of generic extension, map{t . τ }( x . e ), of type [ρ/t]τ → [σ/t]τ, where x : ρ ` e : σ.
Exercises 1. Define the generic extension along product types: map{t . τ1 × τ2 }( x . e ) 7−→ . . . map{t . 1}( x . e ) 7−→ . . . 2. Define the generic extension along sum types: map{t . τ1 + τ2 }( x . e ) 7−→ . . . map{t . 0}( x . e ) 7−→ . . .
Solutions 1. Define the generic extension along product types: map{t . τ1 × τ2 }( x . e ) 7−→ map{t . τ1 }( x . e ) × map{t . τ }( x . e ) map{t . 1}( x . e ) 7−→ 1 2. Define the generic extension along sum types: map{t . τ1 + τ2 }( x . e ) 7−→ map{t . τ1 }( x . e ) + map{t . τ2 }( x . e ) map{t . 0}( x . e ) 7−→ 0
4
Inductive and Coinductive Types
Generic programming is key to giving a general account of inductive (finitary) and coinductive (infinitary) types. Traditional “box and pointer” diagrams 7
make sense only for a limited case of inductive types (those with eager constructors), and are completely useless for dealing with laziness, coinductive types, or functions. It is important to expose students to the far richer world of types and their programs considered here. The definitions of inductive and coinductive types makes use of generic extension. Having defined these, it is then a interesting exercise to extend generic extension to account for inductive and coinductive types. The interesting part of the problem is to ensure that the generic extension is well-defined. In the case of a polynomial type operator this is ensured by induction on the structure of types. But when extending to inductive and coinductive types the justification is not so straightforward, essentially because it must appeal to the generic extension to the “unrolling” of the inductive or coinductive type, which is larger than the inductive or coinductive type itself. The trick is to ensure that the generic extension operation satisfies a regularity condition stating that it acts as the identity on constant families, specified as follows: map {t . τ }( x . e0 )( e ) 7−→ e (t ∈ / τ) In other words the generic extension of a function to a constant type family is the identity.
Exercises 1. Define the generic extension for inductive and coinductive types by giving the following transition rules: map {t . µ( u . τtu )}( x . e0 )( e ) 7−→ . . . map {t . ν( u . τtu )}( x . e0 )( e ) 7−→ . . .
2. Why is your solution well-defined? What justifies the validity of your definition? 3. Prove the type preservation property for your stated transition rules, assuming that it holds for the other cases of generic extension given in the main text.
Solutions µ
1. Let τtu be a polynomial type in two variables, t and u, and write τρ for the substitution instance [ρ, µ/t, u]τ. Let φt be the type operator u . τtu , and µ write φρ for [ρ/t]φt . This expands to u . τρu , and so write φρ (µ) for τρ . Let µt be the type µ( u . φt (u) ), and let νt be the type ν( u . φt (u) ), so that the type µρ is µ( u . φρ (u) ) and νρ is ν( u . φρ (u) ). 8
Suppose that x : σ ` e0 : σ0 . The generic extension for inductive and coinductive types is defined by the following transitions: map {t . µ( u . φt (u) )}( x . e0 )( e ) 7−→ rec{u . φσ (u)}( y . fold{u . φσ0 (u)}( map {t . φt (µσ0 )}( x . e0 )( y ) ); e ) map {t . ν( u . φt (u) )}( x . e0 )( e ) 7−→ gen{u . φσ0 (u)}( y . map {t . φt (νσ )}( x . e0 )( unfold{u . φσ (u)}( y ) ); e ) 2. The regularity requirement saves the day: the use of generic extension on the right is “larger” than on the left only insofar as occurrences of the type variable u have been replaced by the inductive or coinductive type itself. But a careful inspection of the code reveals that these are closed types, and hence cannot involve the distinguished type variable t. Consequently, regularity ensures that the generic extension to closed types is immaterial, thereby ensuring that the extension is well-defined. 3. Suppose that x : σ ` e0 : σ0 is the map to be extended. In the inductive case suppose that e : µσ , and show that the right-hand side has type µσ0 . Check that y : φσ (µσ0 ) ` map {t . φt (µσ0 )}( x . e0 )( y ) : φσ0 (µσ0 ), and so y : φσ (µσ0 ) ` fold{u . φσ0 (u)}( map {t . φt (µσ0 )}( x . e0 )( y ) ) : µσ0 , and so the recursor has the required type, µσ0 . A similar analysis justifies the coinductive case.
5
Distributed Algol
The distributed programming language DA considered in Chapter 41 uses situated, or site-specific, types to ensure that the expression typing judgment, e : τ, is global, or unsituated. For example, the type τ cmd[ w ] classifies expressions that evaluate to encapsulated commands suitable for execution at site w, and the type τ event[ w ] is the type of events that may arise at site w, because of sends or receives along channels allocated at w. Although the expression typing judgment is site-independent, the command typing judgment is not: the ·· τ @ w states that m is a command returning a value of (situatd) judgment m ∼ type τ suitable for execution at world w. An alternative is to consider global, or unsituated types, which do not tie commands, channels, or events to particular sites, but a local, or situated, typing judgments e : τ @ w, which state that e is an expression of type τ that may sensibly be evaluated and used at site w. For example, if m is a command 9
that, say, sends along a channel a located at site w, then the the judgment cmd( m ) : cmd( τ ) @ w expresses this fact by putting the site w into the judgment, rather than into the type itself. Typing contexts are similarly relativized to a site, written Γ = x1 : τ1 @ w1 , . . . , xn : τn @ wn , to specify the type, as well as site, of the variables x1 , . . . , xn . Substitution is constrained to allow xi to be replaced by ei only if e1 : τi @ w. The two formulations, which will be explored further below, are linked by the operation τ ↓ w, which restores . . . To make this precise define τ ↓ w to be the absolute type determined by instantiating the situated type τ at site w. It is defined by the following illustrative equations: nat ↓ w , nat unit ↓ w , unit
(τ1 × τ2 ) ↓ w , τ1 ↓ w × τ2 ↓ w (τ1 → τ2 ) ↓ w , τ1 ↓ w → τ2 ↓ w τ chan ↓ w , (τ ↓ w) chan[ w ] τ event ↓ w , (τ ↓ w) event[ w ] τ cmd ↓ w , (τ ↓ w) cmd[ w ] Instantiation situates an unsituated type at a given site. This operation is extended to situated typing contexts Ψ = x1 : τ1 @ w1 , . . . , xn : τn @ wn by defining the unsituated context ↓ Ψ by the equation
↓ ( x1 : τ1 @ w1 , . . . , xn : τn @ wn ) , x1 : τ1 ↓ w1 , . . . , xn : τn ↓ wn . Some types, such as nat, have site-insensitive meaning in that they have the same values regardless of site. (Contrast types such as τ cmd which classifies commands that may make sense only at a particular site.) An unsituated type, τ, is mobile iff for every w and w0 the equation τ ↓ w = τ ↓ w0 holds: no matter where it is situated, the result is the same. Such types are important when formulating the statics of DA using unsituated types. The following two exercises must be done together, because each requires the solution to the other. But it is useful nonetheless to separate concerns to the large extent possible.
Exercises 1. Formulate the statics of expressions in DA using only unsituated types, but situated typing judgments, such that the following correctness property holds: 10
If Ψ ` e : τ @ w, then ↓ Ψ ` e : τ ↓ w. 2. Reformulate the statics of commands in DA using only unsituated types, but situated typing judgments, such that the following static correctness property holds:
·· τ @ w, then ↓ Ψ ` m ∼·· τ ↓ w @ w. If Ψ ` m ∼
Solutions 1. Ψx:τ@w ` x:τ@w ·· τ @ w Ψ`m∼ Ψ ` cmd( m ) : cmd( τ ) @ w 2.
Ψ ` e:τ@w ·· τ @ w Ψ ` ret( e ) ∼
·· τ 0 @ w Ψ, x : τ @ w ` m ∼ 0 ·· τ @ w Ψ ` bnd( e; x . m ) ∼
Ψ ` e : cmd( τ ) @ w
·· τ 0 @ w0 Ψ ` m0 ∼
τ 0 mobile
·· τ 0 @ w Ψ ` at[ w0 ]( m0 ) ∼
(5a) (5b)
(6a) (6b) (6c)
The requirement that the type τ 0 in Rule (6c) be mobile is of the essence! It ensures that τ 0 ↓ w0 = τ 0 ↓ w, which is required for the returned value to make sense at the originating site.
11
