4. (3 Marks) Is the type of getChargetChar below a pure function? Why or why not? getChar :: 𝙸𝙾 𝙲𝚑𝚊𝚛
getChar :: IO Char
5. (3 Marks) What is a functional correctness specification?
6. (3 Marks) Under what circumstances is performance important for an abstract model?
7. (3 Marks) What is the relevance of termination for the Curry-Howard correspondence?
8. (4 Marks) Imagine you are working on some price tracking software for some company stocks. You have already got a list of stocks to track pre-defined.
data Stock = 𝖦𝖮𝖮𝖦 | 𝖬𝖲𝖥𝖳 | 𝖠𝖯𝖯𝖫 stocks = [𝖦𝖮𝖮𝖦, 𝖬𝖲𝖥𝖳, 𝖠𝖯𝖯𝖫]
data Stock = GOOG | MSFT | APPL stocks = [GOOG, MSFT, APPL]
Your software is required to produce regular reports of the stock prices of these companies. Your co-worker proposes modelling reports simply as a list of prices:
type Report = [Price] type Report = [Price]
Where each price in the list is the stock price of the company in the corresponding position of the stocks list. How is this approach potentially unsafe? What would be a safer representation?
Part B (25 Marks)
The following questions pertain to the given Haskell code:
foldr :: (a → b → b) → b → [a] → b
foldrf z(x : xs) = f x(foldrf zxs) — (𝟣) foldrfz[] = z — (𝟤)
foldr::(a → b → b) → b → [a] → b foldrfz(x:xs) = fx(foldrfzxs) — (1) foldrfz[] = z — (2)
1. (3 Marks) State the type, if one exists, of the expression foldr (:) ([] :: [𝖡𝗈𝗈𝗅]) foldr ( : ) ([] :: [Bool]).
2. (4 Marks) Show the evaluation of foldr (:) [] [1, 2]foldr ( : ) [] [1, 2] via equational reasoning.
3. (2 Marks) In your own words, describe what the function foldr (:) [] foldr ( : ) [] does.
4. (12 Marks) We shall prove by induction on lists that, for all lists xsxs and ysys: foldr(:)xsys = ys++xs
foldr(:)xsys = ys++xs
i. (3 Marks) First show this for the base case where ys = []ys = [] using equational
reasoning. You may assume the left identity property for ++++, that is, for all lsls: ls = []++ls
ls = []++ls
ii. (9 Marks) Next, we have the case where ys = (k : ks)ys = (k : ks) for some item kk and list ksks.
a. (3 Marks) What is the inductive hypothesis about ksks?
b. (6 Marks) Using this inductive hypothesis, prove the above theorem for the inductive case using equational reasoning.
5. (2 Marks) What is the time complexity of the function call foldr (:) [] xsfoldr ( : ) [] xs, where xsxs is of size nn?
6. (2 Marks) What is the time complexity of the function call
foldr (λa as → as ++ [a]) [] xsfoldr (λa as → as ++ [a]) [] xs, where xsxs is of size nn
Part C (25 Marks)
A sparse vector is a vector where a lot of the values in the vector are zero. We represent a sparse vector as a list of position-value pairs, as well as an 𝙸𝚗𝚝Int to represent the overall length of the vector:
data SVec = 𝖲𝖵 𝖨𝗇𝗍 [(𝖨𝗇𝗍, 𝖥𝗅𝗈𝖺𝗍)] data SVec = SV Int [(Int, Float)]
We can convert a sparse vector back into a dense representation with this expandexpand function:
expand :: SVec → [𝖥𝗅𝗈𝖺𝗍] expand(𝖲𝖵nvs) = mapcheck[0..n−1]
where
check x = case lookup x vs of
𝖭𝗈𝗍𝗁𝗂𝗇𝗀 → 0 𝖩𝗎𝗌𝗍 v → v
expand::SVec → [Float] expand(SVnvs) = mapcheck[0..n−1]
where
check x = case lookup x vs of
Nothing → 0 Just v → v
For example, the SVecSVec value 𝖲𝖵 5 [(0, 2.1), (4, 10.2)]SV 5 [(0, 2.1), (4, 10.2)] is
expanded into [2.1, 0, 0, 0, 10.2][2.1, 0, 0, 0, 10.2]
1. (16 Marks) There are a number of SVecSVec values that do not correspond to a
meaningful vector – they are invalid.
i. (6 Marks) Which two data invariants must be maintained to ensure validity of an
SVecSVec value? Describe the invariants in informal English.
ii. (4 Marks) Give two examples of SVecSVec values which violate these invariants.
iii. (6 Marks) Define a Haskell function wellformed :: SVec → Bool wellformed::SVec → Bool which returns 𝚃𝚛𝚞𝚎True iff the data invariants hold for the input SVecvalueSVecvalue. Your Haskell doesn’t have to be syntactically perfect, so long as the intention is clear.
You may find the function nub :: (𝖤𝗊 a) ⇒ [a] → [a]nub:: (Eq a) ⇒ [a] → [a] useful, which removes duplicates from a list.
2. (9 Marks) Here is a function to multiply a SVecSVec vector by a scalar: vsm :: SVec → Float → SVec
vsm(𝖲𝖵nvs)s = 𝖲𝖵n(map(λ(p,v) → (p,v∗s))vs) vsm::SVec → Float → SVec
vsm(SVnvs)s = SVn(map(λ(p,v) → (p,v∗s))vs)
i. (3 Marks) Define a function vsmAvsmA that performs the same operation, but for
dense vectors (i.e. lists of 𝖥𝗅𝗈𝖺𝗍Float).
ii. (6 Marks) Write a set of properties to specify functional correctness of this function. Hint: All the other functions you need to define the properties have already been mentioned in this part. It should maintain data invariants as well as refinement from the abstract model.
Part D (25 Marks)
1. (10 Marks) Imagine you are working for a company that maintains this library for a database of personal records, about their customers, their staff, and their suppliers.
newtype Person = …
name :: Person → String
salary :: Person → 𝖬𝖺𝗒𝖻𝖾 String fire :: Person → 𝖨𝖮 ()
company :: Person → 𝖬𝖺𝗒𝖻𝖾 String
newtype Person = …
name::Person → String
salary :: Person → Maybe String fire :: Person → IO ()
company :: Person → Maybe String
The salarysalary function returns 𝖭𝗈𝗍𝗁𝗂𝗇𝗀Nothing if given a person who is not a member of company staff. The firefire function will also perform no-op unless the given person is a member of company staff. The companycompany function will return 𝖭𝗈𝗍𝗁𝗂𝗇𝗀Nothing unless the given person is a supplier.
Rewrite the above type signatures to enforce the distinction between the different types of person statically, within Haskell’s type system. The function namename must work with all kinds of people as input.
Hint: Attach phantom type parameters to the PersonPerson type.
2. (15 Marks) Consider the following two types in Haskell:
data List a where
𝖭𝗂𝗅 :: Lista
𝖢𝗈𝗇𝗌 :: a → Lista → Lista
dataNat = 𝖹|𝖲Nat data Vec (n :: Nat) a where
𝖵𝖭𝗂𝗅 :: Vec 𝖹 a
𝖵𝖢𝗈𝗇𝗌 :: a → Vecna → Vec(𝖲n)a
data List a where
Nil :: Lista
Cons :: a → Lista → Lista
dataNat = Z | SNat data Vec (n::Nat) a where
VNil :: Vec Z a
VCons :: a → Vecna → Vec(Sn)a
What is the difference between these types? In which circumstances would VecVec be the better choice, and in which ListList?
i. (5 Marks)
ii. (5 Marks) Here is a simple list function:
zip :: Lista → Listb → List(a,b)
zip 𝖭𝗂𝗅
zip xs
zip (𝖢𝗈𝗇𝗌 x xs)
ys = 𝖭𝗂𝗅
𝖭𝗂𝗅 = 𝖭𝗂𝗅
(𝖢𝗈𝗇𝗌 y ys) = 𝖢𝗈𝗇𝗌 (x, y) (zip xs ys)
zip::List a → List b → List (a, b)
zip Nil
zip xs
zip (Cons x xs)
ys
Nil
(Cons y ys)
= Nil
= Nil
= Cons (x, y) (zip xs ys)
Define a new version of zipzip which operates on VecVec instead of ListList wherever possible. You can constrain the lengths of the input.
iii. (5 Marks) Here is another list function:
filter :: (a → 𝖡𝗈𝗈𝗅) → Lista → Lista filter p 𝖭𝗂𝗅 = 𝖭𝗂𝗅
filter p (𝖢𝗈𝗇𝗌 x xs)
|px = 𝖢𝗈𝗇𝗌x(filterpxs) | otherwise = filter p xs
filter:: (a → Bool) → List a → List a filter p Nil = Nil
filter p (Cons x xs)
| px = Consx(filterpxs) | otherwise = filter p xs
Define a new version of filterfilter which operates on VecVec instead of ListList wherever possible.
Part E (25 Marks)
1. (10 Marks) An applicative functor is called commutative iff the order in which actions are sequenced does not matter. In addition to the normal applicative laws, a commutative applicative functor satisfies:
f ⟨$⟩u⟨∗⟩v = flipf ⟨$⟩v⟨∗⟩u f⟨$⟩u⟨∗⟩v = flipf⟨$⟩v⟨∗⟩u
i. (2 Marks) Is the 𝙼𝚊𝚢𝚋𝚎Maybe Applicative instance commutative? Explain your answer.
ii. (3 Marks) We have seen two different 𝙰𝚙𝚙𝚕𝚒𝚌𝚊𝚝𝚒𝚟𝚎Applicative instances for lists. Which of these instances, if any, are commutative? Explain your answer.
iii. (5 Marks) A commutative monad is the same as a commutative applicative, only specialised to monads. Express the commutativity laws above in terms of monads, using either dodo notation or the raw pure/bind functions.
2. (10 Marks) Translate the following logical formulae into types, and provide Haskell types that correspond to proofs of these formulae, if one exists. If not, explain why not.
i. (2 Marks) (A ∨ B) → (B ∨ A)(A ∨ B) → (B ∨ A)
ii. (2 Marks) (A ∨ A) → A(A ∨ A) → A
iii. (3 Marks) (A ∧ (B ∨ C)) → ((A ∧ B) ∨ (A ∧ C)) (A∧(B∨C)) → ((A∧B)∨(A∧C))
iv. (3 Marks) ¬((A → ⊥) ∨ A)¬((A → ⊥) ∨ A)
3. (5 Marks) Here is a Haskell data type:
data X data X
= 𝖥𝗂𝗋𝗌𝗍 () 𝖠
| 𝖲𝖾𝖼𝗈𝗇𝖽 () 𝖵𝗈𝗂𝖽
| 𝖳𝗁𝗂𝗋𝖽 (𝖤𝗂𝗍𝗁𝖾𝗋 𝖡 ())
= First () A
| Second () Void
| Third (Either B ())
Using known type isomorphisms, simplify this type as much as possible.
END OF SAMPLE EXAM
(don’t forget to save!)
Time Remaining 2h 9m 33s
Save
Loading [MathJax]/jax/output/HTML-CSS/jax.js