Exercise 5 GADTs TypeSafe printf More on Vectors Administrivia
1
Software System Design and Implementation
GADTs Practice
Curtis Millar
CSE, UNSW (and Data61) 22 July 2020
Exercise 5
GADTs TypeSafe printf More on Vectors Administrivia
2
Parse a series of tokens.
Stack push and pop.
Evaluate a sequence of tokens. Calculate a string.
Exercise 5
Exercise 5 GADTs TypeSafe printf More on Vectors Administrivia
3
Recall: GADTs
Generalised Algebraic Datatypes (GADTs) is an extension to Haskell that, among other things, allows data types to be specified by writing the types of their constructors:
{-# LANGUAGE GADTs, KindSignatures #-}
— Unary natural numbers, e.g. 3 is S (S (S Z)) data Nat = Z | S Nat
— is the same as
data Nat :: * where
Z :: Nat
S :: Nat -> Nat
Exercise 5 GADTs TypeSafe printf More on Vectors Administrivia
4
The printf function
Consider the well known C function printf:
printf(“Hello %s You are %d years old!”, “Nina”, 22)
In C, the type (and number) of parameters passed to this function are dependent on the first parameter (the format string).
Exercise 5 GADTs TypeSafe printf More on Vectors Administrivia
5
The printf function
To do a similar thing in Haskell, we would like to use a richer type that allows us to
define a function whose subsequent parameter is determined by the first.
data Format :: * -> * where
End :: Format () — Empty format Str :: Format t -> Format (String, t) — %s
Dec :: Format t -> Format (Int, t) — %d
L :: String -> Format t -> Format t — literal strings deriving instance Show (Format ts)
— just like deriving (Show) for normal data types.
Our format strings are indexed by a tuple type containing all of the types of the %directives used.
Exercise 5 GADTs TypeSafe printf More on Vectors Administrivia
6
is written:
L “Hello” $ Str $ L ” You are ”
$ Dec $ L ” years old!” End
The printf function
“Hello %s You are %d years old!”
Exercise 5 GADTs TypeSafe printf More on Vectors Administrivia
7
The printf function
printf :: Format ts -> ts -> IO ()
printf End () =
pure () — type is () printf (Str fmt) (s,ts) =
do putStr s; printf fmt ts — type is (String, …) printf (Dec fmt) (i,ts) =
do putStr (show i); printf fmt ts — type is (Int,..) printf (L s fmt) ts =
do putStr s; printf fmt ts
Exercise 5 GADTs TypeSafe printf More on Vectors Administrivia
8
Vectors
Define a natural number kind to use on the type level:
data Nat = Z | S Nat
Our length-indexed list can be defined, called a Vec:
data Vec (a :: *) :: Nat -> * where Nil ::VecaZ
Cons :: a -> Vec a n -> Vec a (S n)
The functions hd and tl can be total:
hd :: Vec a (S n) -> a
hd (Cons x xs) = x
tl :: Vec a (S n) -> Vec a n
tl (Cons x xs) = xs
Exercise 5 GADTs TypeSafe printf More on Vectors Administrivia
Vectors, continued
Our map for vectors is as follows:
mapVec :: (a -> b) -> Vec a n -> Vec b n
mapVec f Nil = Nil
mapVec f (Cons x xs) = Cons (f x) (mapVec f xs)
Properties
Using this type, it’s impossible to write a mapVec function that changes the length of the vector.
Properties are verified by the compiler!
9
Exercise 5 GADTs TypeSafe printf More on Vectors Administrivia
Appending Vectors
Example (Problem)
10
appendV :: Vec a m -> Vec a n -> Vec a ???
We want to write m + n in the ??? above, but we do not have addition defined for
kind Nat.
We can define a normal Haskell function easily enough:
plus :: Nat -> Nat -> Nat
plus Z y = y
plus (S x) y = S (plus x y)
This function is not applicable to type-level Nats, though. ⇒ we need a type level function.
Exercise 5 GADTs TypeSafe printf More on Vectors Administrivia
11
Type Families
Type level functions, also called type families, are defined in Haskell like so:
{-# LANGUAGE TypeFamilies #-}
type family Plus (x :: Nat) (y :: Nat) :: Nat where
Plus Z y = y
Plus (S x) y = S (Plus x y)
We can use our type family to define appendV:
appendV :: Vec a m -> Vec a n -> Vec a (Plus m n)
appendV Nil ys = ys
appendV (Cons x xs) ys = Cons x (appendV xs ys)
Exercise 5 GADTs TypeSafe printf More on Vectors Administrivia
Concatenating Vectors
Example (Problem)
12
concatV :: Vec (Vec a m) n -> Vec a ???
We want to write m * n in the ??? above, but we do not have times defined for kind
Nat.
{-# LANGUAGE TypeFamilies #-}
type family Times (a :: Nat) (b :: Nat) :: Nat where
Times Z n = Z
Times (S m) n = Plus n (Times m n)
We can use our type family to define concatV:
concatV :: Vec (Vec a m) n -> Vec a (Times n m)
concatV Nil = Nil
concatV (Cons v vs) = v `appendV` concatV vs
Exercise 5 GADTs TypeSafe printf More on Vectors Administrivia
Filtering Vectors
Example (Problem)
13
filterV :: (a -> Bool) -> Vec a n -> Vec a ??? What is the size of the result of filter?
Exercise 5 GADTs TypeSafe printf More on Vectors Administrivia
Filtering Vectors
Example (Problem)
14
filterV :: (a -> Bool) -> Vec a n -> [a] We do not know the size of the result.
We can use our type family to define concatV:
filterV :: (a -> Bool) -> Vec a n -> [a]
filterV p Nil = []
filterV p (Cons x xs)
|px =x:filterVpxs | otherwise = filterV p xs
Exercise 5
GADTs TypeSafe printf More on Vectors Administrivia
15
1
2 3 4
Assignment 2 is released. Due on 5th August, 3 PM (in 14 days).
Week 7’s quiz is due on Friday. Make sure you submit your answers.
The sixth programming exercise is due by the start of my next lecture (in 7 days). This week’s quiz is also up, it’s due Friday week (in 9 days).
Homework
Exercise 5
GADTs TypeSafe printf More on Vectors Administrivia
16
Consultations
Consultations will be made on request. Ask on piazza or email cs3141@cse.unsw.edu.au.
If there is a consultation it will be announced on Piazza with a link a room number for Hopper.
Will be in the Thursday lecture slot, 9am to 11am on Blackboard Collaborate.
Make sure to join the queue on Hopper. Be ready to share your screen with REPL (ghci or stack repl) and editor set up.