[SOLVED] ocaml函数编程代写: Advanced functional programming Exercise 1

# Some standard definitions. Any definition in this file may be used
# in the solution to any question

# The empty type, Zero.
# There is no value of type Zero.
# From a variable of type Zero it is possible to build a term of any type:
# λx:Zero. x [A]
Zero :: *
= ∀α.α;

# The one-element type Unit, and its single inhabitant, unit.
Unit :: *
= ∀A::*.A → A;
unit = ΛA.λa:A.a;

# The two element type Bool, its two inhabitants, ff (false) and tt (true),
# and its destructor, if.
Bool :: * = ∀A::*.A → A → A;
ff : Bool
= ΛA.λf:A.λt:A.f;
tt : Bool
= ΛA.λf:A.λt:A.t;
if : Bool → (∀α.α → α → α)
= λb:Bool.b;

# The type of natural numbers, Nat, along with
# its two constructors zero and succ, and an addition function, add.
Nat :: * =
∀α::*.α → (α → α) → α;
zero : Nat
= Λα::*.λz:α.λs:α → α.z;
succ : Nat → Nat
= λn:Nat.Λα::*.λz:α.λs:α → α.s (n [α] z s);
add : Nat → Nat → Nat
= λm:Nat.λn:Nat.m [Nat] n succ;

# 1(a): (answer on paper)
# 1(b): (answer on paper)
# 1(c): (answer on paper)
# 2(a): (answer on paper)
# 2(b): (answer on paper)

# 3(a)
# (a + b) + c ≃ a + (b + c)
plus_assoc1 : ∀A.∀B.∀C.((A + B) + C) → (A + (B + C))
# = ? [ANSWER]
;
plus_assoc2 : ∀A.∀B.∀C.(A + (B + C)) → ((A + B) + C)
# = ? [ANSWER]
;

# 3(b)
# a(b + c) ≃ ab + ac
distrib1 : ∀A.∀B.∀C.(A×(B + C)) → ((A×B) + (A×C))
# = ? [ANSWER]
;
distrib2 : ∀A.∀B.∀C.((A×B) + (A×C)) → (A×(B + C))
# = ? [ANSWER]
;

# 3(c)
annihil1 : ∀A.(Zero × A) → Zero
# = ? [ANSWER]
;
annihil2 : ∀A. Zero → (Zero × A)
# = ? [ANSWER]
;

# 4(a)

# A definition of the existential quantifier in Fω
Exists :: (* ⇒ *) ⇒ *
# = ? [ANSWER]
;

# pack_ (λα.γ) β M ≡ pack β,M as ∃α.γ
# pack_ : ? = ?; [ANSWER]

# open_ [B] b [A] (Λβ.λb.e) ≡ open b as β, b in e
# open_ : ? = ?; [ANSWER]

# The signature for bools, based on an abstract type β
Bools = λβ.β×β×(β → (∀α.α → α → α));

# An implementation of the Bools signature:
bools = ⟨inr [Unit] unit,
inl [Unit] unit,
λb:Unit+Unit.
Λα.
λr:α.
λs:α.
case b of x.s | y.r ⟩;

# A test case for Exists
Abstract_bools = Exists Bools;

# A test case for pack_ (uncomment once you’ve defined pack_)
# packed_bools = pack_ [Bools] [Unit+Unit] bools;

# An equivalent definition using the builtin ‘pack’.
packed_bools_builtin = pack (Unit+Unit), bools as ∃β.Bools β;

# A test case for open_ (uncomment once you’ve defined open_)
# open_example_ = λp:Exists Bools.
# open_ [Bools] p [Unit]
# (Λβ.λbools:Bools β.
# (@3 bools)
# (@1 bools)
# [Unit]
# unit unit)
# ;

# An equivalent definition using the builtin ‘open’:
open_example_builtin = λp:∃β.Bools β.
open p as β, bools in
(@3 bools) # if
(@1 bools) # true
[Unit]
unit unit
;

# 4(b)

# The Gates signature
Gates =
λT::*⇒*⇒*.
(T (Bool × Bool) Bool) ×
(∀α.T α (α×α)) ×
(∀α.∀β.∀γ.∀δ.T α γ → T β δ → T (α × β) (γ × δ)) ×
(∀α.∀β.∀γ.T α β → T β γ → T α γ);

# Projections from the signature. If you have a value
# g :: Gates G
# then the following expressions access the components of g:
# nor [G] g
# split [G] g
# join [G] g
# plug [G] g

nor : ∀G::*⇒*⇒*.Gates G →
G (Bool×Bool) Bool =
ΛG::*⇒*⇒*.λg:Gates G.@1 g;

split : ∀G::*⇒*⇒*.Gates G →
(∀α.G α (α×α)) =
ΛG::*⇒*⇒*.λg:Gates G.@2 g;

join : ∀G::*⇒*⇒*.Gates G →
(∀α.∀β.∀γ.∀δ.G α γ → G β δ → G (α×β) (γ×δ)) =
ΛG::*⇒*⇒*.λg:Gates G.@3 g;

plug : ∀G::*⇒*⇒*.Gates G →
(∀α.∀β.∀γ.G α β → G β γ → G α γ) =
ΛG::*⇒*⇒*.λg:Gates G.@4 g;

# 4(b)(i)
not : ∀G::*⇒*⇒*.Gates G → G Bool Bool
# = ? [ANSWER]
;

# 4(b)(ii)
and : ∀G::*⇒*⇒*.Gates G → G (Bool×Bool) Bool
# = ? [ANSWER]
;

# 4(b)(iii)
function_gates : Gates (λX::*.λY::*.X → Y)
# = ? [ANSWER]
;

# 4(b)(iv)
count_gates : Gates (λX::*.λY::*.Nat)
# = ? [ANSWER]
;

# 4(b)(v)
# A definition of the 2-parameter existential quantifier in Fω
# Exists2 = ? [ANSWER]

# pack2_ (λα.γ) β M ≡ pack β,M as ∃α.γ
# pack2_ : ? = ? [ANSWER] ;

# open2_ [B] b [A] (Λβ.λb.e) ≡ open b as β, b in e
# open2_ : ? = ? [ANSWER]

# A test case for Exists2 (uncomment once you’ve defined Exists2):
# Abstract_gates = Exists2 Gates;

# Test cases for pack2_ (uncomment once you’ve defined pack2_):
# packed_function_gates : Exists2 Gates =
# pack2_ [Gates] [λX.λY.X → Y] function_gates;
# packed_count_gates : Exists2 Gates =
# pack2_ [Gates] [λX.λY.Nat] count_gates;

# A test case for open2_ (uncomment once you’ve defined open2_)
# opened_gates = λg:Exists2 Gates.
# open2_ [Gates] g [Unit]
# (ΛG::*=>*=>*.λg:Gates G.
# (λg:G Bool Bool.unit)
# (plug [G] g [Bool] [Bool] [Bool] (not [G] g) (not [G] g)))
# ;

# An equivalent definition using the builtin ‘open’
opened_gates_builtin = λg:∃G::*=>*=>*. Gates G.
open g as G, g in
(λg:G Bool Bool.unit)
(plug [G] g [Bool] [Bool] [Bool] (not [G] g) (not [G] g))
;

## Finally, it would be helpful to know how long you spent on this
## exercise. There is no obligation to answer this question if you would
## prefer not to! I plan to use the information provided to improve the
## course, and will not distribute the information further except possibly
## in anonymised form. (E.g. I would like to produce and perhaps share
## aggregate statistics such as the range, median, variance, etc., but
## will not identify any individual student.)
##
## How many hours did you spend on this exercise?
## [ANSWER]

L28: Advanced functional programming Exercise 1 Due on 12th February 2018 Submission instructions Your solutions for this exericse should be handed in to the Graduate Education Office by 4pm on the due date. Additionally, please email the completed text file exercise1.f to [email protected]. Additional instructions This exercise involves the use of the fomega interpreter. Instructions for installing fomega are available on the course webpage: https://www.cl.cam.ac.uk/teaching/1718/L28/materials.html The accompanying file exercise1.f contains a number of definitions, any of which may be used in the solutions to questions 3 and 4. 1 1 Typing derivations For each of the following System Fω terms either give a typing derivation or explain why the term has no typing derivation: (a) Λα::*.λh:α → α.h h (b) λf:(∀α::*.α).(fst (f [(1 → 1) × 1])) (f [1]) (c) λg:(∀φ::* ⇒ *.∀α::*.φ α → α).Λγ.g [λβ.1] [γ] hi (You may assume the existence of the unit type 1 and value hi from Lecture 1) (6 marks) 3 2 Type inference and polymorphism (a) Here are two definitions of the identity function let id = fun x -> x let id2 = id id OCaml gives the first definition a generalized type: val id : ‘a -> ‘a = but gives the second definition a non-generalized type: val id2 : ‘_a -> ‘_a = Consequently, id can be applied to arguments of many different types: ( id 1 , id ” two ” , id false ) ❀ (1 , ” two ” , false ) while id2 can only be applied to arguments of a single type: ( id2 1 , id2 ” two ” , id2 false ) ❀ error! Explain why the type checker treats the two definitions differently. (b) Although the following two programs are very similar, the first program is rejected by OCaml while the second program is accepted. (* rejected by OCaml *) let f x = (x , ( fun y -> x :: y ) ) let g = f [] let i = (1 :: fst g , ” two ” :: fst g ) (* accepted by OCaml *) let f x = (x , ( fun y -> x :: y ) ) let g = fst ( f []) let i = (1 :: g , ” two ” :: g ) Explain briefly why the type checker rejects the first program but accepts the second. (6 marks) 4 3 Arithmetic identities in System Fω A number of equations familiar from high school arithmetic can also be applied to types. For example, in arithmetic the value 1 acts as a right identity for multiplication: For any number a, a × 1 ≡ a and similarly in lambda calculus it is possible to write functions that convert back and forth between the types A × 1 and A: f : ∀A . A×1 → A = ΛA .λp : A×1. f s t p g : ∀A . A → A×1 = ΛA .λx : A .hx ,hii (Furthermore, the composition of f and g corresponds to the identity function. However, to capture this fact in the types we would need to switch from System Fω to a more expressive calculus such as λC.) Write similar pairs of System Fω functions that correspond to each of the following three arithmetic identities: (a) (a + b) + c ≡ a + (b + c) (+ is associative) (b) a × (b + c) ≡ a × b + a × c (× distributes over +) (c) 0 × a ≡ 0 (0 is an annihilator for ×) (6 marks) 5 4 Circuits and abstraction The version of System Fω described in the lectures and implemented in the fomega tool supports several additional constructs besides the basic forms for abstraction and application: pairs, sums, and existential types. Although they are convenient, these additional constructs are not entirely necessary, since they can be encoded in the core of the language. This question investigates encodings of existential types. (a) Define an operation Exists :: (* ⇒ *) ⇒ * representing an existential type, along with operations pack_ : ? open_ : ? for constructing and using existentials. The following test case may be helpful in developing your definitions. Given a signature for booleans Bools = λβ.β × β×(β → (∀α.α → α → α) ) you should be able to construct the type Exists Bools and the terms involving pack_ and open_ on the left hand side below. (The corresponding terms involving the built-in pack and open are shown for reference on the right.) pack_ [ Bools ] [ Unit + Unit ] hinr [ Unit ] unit , i n l [ Unit ] unit , λb : Unit + Unit . Λα. λr :α. λs :α. case b o f x . s | y . r i pack [ Unit + Unit ] , hinr [ Unit ] unit , i n l [ Unit ] unit , λb : Unit + Unit . Λα. λr :α. λs :α. case b o f x . s | y . r i as ∃β. Bools β λp : Exists Bools . open_ [ Bools ] p [ Unit ] (Λβ.λbools : Bools β. ( @2 ( @2 bools ) ) ( @1 bools ) [ Unit ] unit unit ) λp :∃β. Bools β. open p as β, bools in ( @2 ( @2 bools ) ) ( @1 bools ) [ Unit ] unit unit (b) It is often useful to build signatures for modules involving parameterized abstract types. For example, the Queue and Stack mmodules in the standard library both expose an abstract type for the container, paramterized by the type of elements: 6 module Queue : sig type ‘a t val create : unit -> ‘a t (* … *) module Stack : sig type ‘a t val create : unit -> ‘a t (* … *) Here is a System Fω signature involving parametrized abstract types, and exposing operations for building logical circuits with nor gates: Gates = λT ::* ⇒ * ⇒ *. ( T ( Bool × Bool ) Bool ) × # nor (∀α. T α (α × α) ) × # split (∀α.∀β.∀γ.∀δ. T α γ → T β δ → T (α × β) (γ × δ) ) × # join (∀α.∀β.∀γ. T α β → T β γ → T α γ) # plug The signature is parameterized by a type constructor T; in turn, T is parameterised by two types representing the input and output to a circuit. There are four value components. The first, of type T (Bool × Bool) Bool represents a nor gate with the following standard truth table: nor P Q nor P Q F F T F T F T F F T T F The remaining three components correspond to plumbing operations that can be used to pass the same input to multiple components, and to wire circuits together in parallel or series. split join plug Finally, for reference, here is an OCaml version of Gates: module type Gates = sig type (‘i , ‘o ) t val nor : ( bool * bool , bool ) t val split : (‘a , ‘a * ‘a ) t val join : (‘a ,’c ) t -> (‘b ,’d ) t -> (‘a * ‘b , ‘c * ‘d ) t val plug : (‘a ,’b ) t -> (‘b ,’c ) t -> (‘a ,’c ) t end (i) Using the Gates signature, define a function not with the following type and truth table: not : ∀G ::* ⇒ * ⇒ *. Gates G → G Bool Bool P not P F T T F 7 (ii) Using the Gates signature (and, if you like, your definition of not from the previous question, define a function and with the following type and truth table: and : ∀G ::* ⇒ * ⇒ *. Gates G → G ( Bool × Bool ) Bool P Q and P Q F F F F T F T F F T T T (iii) Give an implementation of Gates as a value of the following type: function_gates : Gates (λX ::*.λY ::*. X → Y ) that represents a circuit as a function from input to output. (iv) Give a second implementation of Gates as a value of the following type: count_gates : Gates (λX .λY . Nat ) that represents a circuit as a natural number that corresponds to the number of nor gates in the circuit. (v) Since the type component T of the Gates signature does not have kind *, Gates cannot be used with Exists. Define Exists2, a variant of Exists for binary type operators, along with constructor and deconstructor pack2_ and open2_ that are suitable for use with Gates. You should ensure that the following expressions pass type checking with your definitions: Exists2 Gates pack2_ [ Gates ] [λα.λβ.α → β] function_gates pack2_ [ Gates ] [λα.λβ. Nat ] count_gates λg : Exists2 Gates . open2_ [ Gates ] g [ Unit ] (ΛG ::*⇒ *⇒ *.λg : Gates G . (λg : G Bool Bool . unit ) ( plug [ G ] g [ Bool ] [ Bool ] [ Bool ] ( not [ G ] g ) ( not [ G ] g ) ) ) (12 marks) 8