12/08/2020 Quiz (Week 8)
Quiz (Week 8)
Phantom Types Safe Division
Below we have a simple use of phantom types to avoid divide-by-zero errors.
data Zero
data NonZero
newtype CheckedInt t = Checked Int
safeDiv :: Int -> CheckedInt NonZero -> Int
safeDiv x (Checked y) = x `div` y
Question 1
Which of the following statements are true?
1. ✗ The types Zero and are phantom types.
2. ✔ The type argument is a phantom type parameter.
3. ✗ This code will not compile as and NonZero have not been de ned. 4. ✗ All types declared with are phantom types.
Question 2
What is the type of a smart constructor for the type CheckedInt ?
1. ✗
2. ✗
3. ✗
4. ✔ check :: Int -> Either (CheckedInt Zero) (CheckedInt NonZero)
t
NonZero
Zero
newtype
A phantom type parameter is a does not occur in the data type de nition, i.e. t in this example. and are types that do not have any constructors, not phantom types. introduces a type with the same representation as the internal type, i.e. a cost-free new type, not a phantom type.
Zero
newtype
check :: Int -> CheckedInt t
NonZero
check :: Int -> CheckedInt NonZero
check :: Int -> CheckedInt (Either Zero NonZero)
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/quiz.html
1/7
12/08/2020 Quiz (Week 8)
Linear Algebra
Here Phantom types of a kind Size have been used to make vectors of various dimensions. Note that, unlike a GADT solution, the vector size is not statically checked if we use the default V data constructor. Rather we must be sure to only use the given smart constructors that establish the length invariant about the data:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data Size = OneD | TwoD | ThreeD
newtype Vector (s :: Size) a = V [a]
vec1D :: a -> Vector OneD a
vec1D a = V [a]
vec2D :: (a, a) -> Vector TwoD a
vec2D (a,b) = V [a,b]
vec3D :: (a, a, a) -> Vector ThreeD a
vec3D (a,b,c) = V [a,b,c]
Question 3
Which of the following implementations of vector addition encode statically the precondition that the vectors must be the same size (and only that precondition), as well as the postcondition that the output vector will be the same size as the input?
1. ✗
addV :: (Num n) => Vector a n -> Vector b n -> Vector c n
addV (V xs) (V ys) = V (zipWith (+) xs ys)
A smart constructor is a function that checks a condition in order to establish an invariant for a particular type. As it’s meant to replace a regular data constructor, we expect it to be total, and so the type of Option 2 is incorrect, as would be unde ned. Option 1 is also incorrect, as this returns a for any
t , so it may for example apply the type tag to zero values. Option 3 is also incorrect, as isn’t a valid tag for our phantom type. The correct answer is option 4, which can return a CheckedInt Zero if the input is 0 and a CheckedInt NonZero otherwise.
check 0
CheckedInt t
NonZero
Either Zero NonZero
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/quiz.html
2/7
12/08/2020 Quiz (Week 8)
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/quiz.html
3/7
2. ✔
addV :: (Num n) => Vector a n -> Vector a n -> Vector a n
addV (V xs) (V ys) = V (zipWith (+) xs ys)
3. ✗
4. ✗
addV :: (Num n) => Vector TwoD n -> Vector TwoD n -> Vector TwoD n
addV (V xs) (V ys) = V (zipWith (+) xs ys)
addV :: (Num n) => Vector a n -> Vector a n -> Vector b n
addV (V xs) (V ys) = V (zipWith (+) xs ys)
Option 1 allows the input vectors to be any size, and produces an output vector with an arbitrary size tag, which may not accurately re ect the size of the contents, so it is incorrect. Option 3 requires that both input vectors are two- dimensional and the output vector is also two-dimensional. This is too excessive a restriction, as we only require that the sizes are equal. Option 4 allows the output vector to have an arbitrary size tag, which is also incorrect.
Option 2 requires both input vectors to have the same size a and then returns a vector of the same size. This is the correct answer.
Question 4
Suppose we made a Matrix type using vectors of vectors:
What is the correct type for a matrix multiplication function?
1. ✗
2. ✗
3. ✗
4. ✔ mm :: Num a => Matrix r i a -> Matrix i c a -> Matrix r c a
type Matrix r c a = Vector r (Vector c a)
mm :: Num a => Matrix r i a -> Matrix r i a -> Matrix r i a
mm :: Num a => Matrix r i a -> Matrix i c a -> Matrix r i a
mm :: Num a => Matrix r i a -> Matrix c i a -> Matrix i i a
Matrix multiplication of requires the number of columns in be the same as the number of rows in . The result will have the same number of rows as
and the same number of columns as . Thus, option 4 is correct.
B AB
A B×A
12/08/
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/quiz.html 4/7
2020 Quiz (Week 8)
GADTs
Emptiness-indexed types Question 5
Here is an ordinary binary tree type presented using GADT syntax:
Suppose we have this function to get the root element of a Tree :
Unfortunately, this function is partial, that is, it is not de ned for its entire domain (all values of type Tree a ). Which of the following GADT de nitions of the Tree type would enable us to re ne the type of root to express the precondition that the tree must not be empty?
1. ✗
2. ✗
data Tree a where
Leaf :: Tree a
Branch :: a -> Tree a -> Tree a -> Tree a
root :: Tree a -> a
root (Branch v _ _) = v
data IsEmpty = Empty | NotEmpty
data Tree (t :: IsEmpty) a where
Leaf :: Tree Empty a
Branch :: a -> Tree t a -> Tree t a -> Tree NotEmpty a
data IsEmpty = Empty | NotEmpty
data Tree (t :: IsEmpty) a where
Leaf :: Tree t a
Branch :: a -> Tree t a -> Tree t a -> Tree t a
3. ✔
Option 1 requires the matrices have the same exact dimensions. Option 2 makes the output the same size as . Option 3 incorrectly mixes the dimensionalities of the inputs.
A
12/08/2020 Quiz (Week 8)
4. ✗
data IsEmpty = Empty | NotEmpty
data Tree (t :: IsEmpty) a where
Leaf :: Tree t a
Branch :: a -> Tree t1 a -> Tree t2 a -> Tree NotEmpty a
Option 1 is incorrect, as it forces the two children of any node to have the same Empty / NotEmpty status. Option 2 is incorrect, as it never places any constraint
on the type variable t . Option 3 is correct, as requiring a NotEmpty input to
root makes it a total function (rules out the case). Option 4 is incorrect, as
it allows the Leaf node to be tagged , so the root function would potentially still be partial.
Leaf
NotEmpty
Typed Abstract Syntax
We have here a language of boolean and arithmetic expressions, annotated with their types.
data Exp a where
Plus :: Exp Int -> Exp Int -> Exp Int
Const :: (Show a) => a -> Exp a
LessOrEq :: Exp Int -> Exp Int -> Exp Bool
Not :: Exp Bool -> Exp Bool
And :: Exp Bool -> Exp Bool -> Exp Bool
Question 6
The full evaluation function for this language has the following type:
What are the possible types that eval may return? 1.✗an Int ora Bool
eval :: Exp a -> a
data IsEmpty = Empty | NotEmpty
data Tree (t :: IsEmpty) a where
Leaf :: Tree Empty a
Branch :: a -> Tree t1 a -> Tree t2 a -> Tree NotEmpty a
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/quiz.html
5/7
12/08/2020 Quiz (Week 8)
2. ✔ an , a , or a value of any type implementing . 3. ✗ It will always return Int
4. ✗ The evaluation function may return any type.
Question 7
Here is a function that evaluates only arithmetic expressions.
What type signature should be given to evalArith such that it is total?
Int
Bool
The return type of is any for which an eitherand Int (from or ),a
can be constructed. This is , Not, And,or
).
rval
a
Exp a
(from
Const ), or any type implementing
(from
Plus
Const
Bool
LessOrEq
Show
Const
evalArith (Plus a b) = evalArith a + evalArith b
evalArith (Const a) = a
1. ✗
2. ✗
3. ✗
4. ✔ Exp Int -> Int
Propositional Equality Question 8
Suppose we had the following GADT:
Suppose we had a function f of type
that this type signature indicates may be returned by
. Check all of the values below .
Exp a -> a
Exp Int -> a
Exp a -> Int
Options 1 and 3, which take an Exp a , would crash at runtime if given, e.g. an And expression. Option 2 does not typecheck. Thus Option 4 is correct.
data Id a b where
Refl :: Id x x
1. ✗ True
Id a Int -> a
f
Show
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/quiz.html
6/7
12/08/2020 Quiz (Week 8)
2. ✔ 3. ✔ 4. ✗ 5. ✗
34
0
Refl
a
The only way a value of could be constructed is if the type a was an . Thus, the function will learn that a is an Int when it matches on
Refl , and can then return any integer value, i.e. option 2 and option 3.
Id a Int
Int
f
Submission is already closed for this quiz. You can click to check your submission (if any).
here here
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/quiz.html
7/7