12/08/2020 Code (Week 8 Wednsday)
Code (Week 8 Wednsday) Format Strings
module Format where
{-
– Format
– ======
–
– Add type of expected arguments
–
– * End of format string
– * String literal
– * Decimal argument
– * String argument
-}
{-
data Format
= End — End :: Format
| L String Format — L :: String -> Format -> Format
| Dec Format — Dec :: Format -> Format
| Str Format — Str :: Format -> Format
deriving (Show, Eq)
-}
data Format :: * -> * where
End :: Format ()
L :: String -> Format a -> Format a
Dec :: Format a -> Format (Int, a)
Flt :: Format a -> Format (Float, a)
Str :: Format a -> Format (String, a)
deriving instance Show (Format a)
printf :: Format a -> a -> IO ()
printf End () = putChar ‘\n’
printf (L literal fs) as = do
putStr literal
printf fs as
printf (Dec fs) (i, as) = do
putStr $ show (i :: Int)
printf fs as
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/Wednesday/Code.html
1/4
12/08/2020 Code (Week 8 Wednsday)
Measures
module Measure where
newtype Measure p u = M Float
data One
data Square p
data Kilometers
data Miles
distance :: Float -> Measure One Kilometers
distance = M
imDistance :: Float -> Measure One Miles
imDistance = M
square :: Measure p u -> Measure (Square p) u
square (M i) = M $ i * i
data Stage = One | Two | Final
descentStage :: Measure One Kilometers -> Stage
descentStage (M 125) = One
descentStage (M 50) = Two
descentStage (M 1) = Final
imToMet :: Measure One Miles -> Measure One Kilometers
imToMet (M i) = M $ i * 1.60934
s = descentStage $ imToMet $ imDistance 70
Vectors
printf (Flt fs) (i, as) = do
putStr $ show (i :: Float)
printf fs as
printf (Str fs) (s, as) = do
putStr s
printf fs as
— “Hello %s you are %d years old”
example = L “Hello ” $ Str $ L ” you are ” $ Dec $ L ” years old” End
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, GADTs #-}
{-# LANGUAGE UndecidableInstances, StandaloneDeriving #-}
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/Wednesday/Code.html
2/4
12/08/2020 Code (Week 8 Wednsday)
module Vector where
— Natural numbers, values will be promoted to types
data Nat
= Z — Zero
| S Nat — Successor (+1)
data Vec (a :: *) :: Nat -> * where
— Nil has zero length
Nil :: Vec a Z
— Cons has length of the tail + 1
Cons :: a -> Vec a n -> Vec a (S n)
deriving instance Show a => Show (Vec a n)
— head :: [a] -> a
hd :: Vec a (S n) -> a
hd (Cons x xs) = x
— tail :: [a] -> [a]
tl :: Vec a (S n) -> Vec a n
tl (Cons x xs) = xs
— map :: (a -> b) -> [a] -> [b]
vMap :: (a -> b) -> Vec a n -> Vec b n
vMap f Nil = Nil
vMap f (Cons x xs) = Cons (f x) (vMap f xs)
— (++) :: [a] -> [a] -> [a]
vAppend :: Vec a n -> Vec a m -> Vec a (Plus n m)
vAppend Nil xs = xs
vAppend (Cons y ys) xs = Cons y (vAppend ys xs)
— Type-level addition
type family Plus (x :: Nat) (y :: Nat) :: Nat where
Plus Z n= n
Plus (S m) n = S (Plus m n)
— concat :: [[a]] -> [a]
vConcat :: Vec (Vec a n) m -> Vec a (Times m n)
vConcat Nil = Nil
vConcat (Cons xs xss) = xs `vAppend` vConcat xss
— Type-level multiplication
type family Times (x :: Nat) (y :: Nat) :: Nat where
Times Z m = Z
Times (S n) m = Plus m (Times n m)
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/Wednesday/Code.html
3/4
12/08/2020 Code (Week 8 Wednsday)
vFilter :: (a -> Bool) -> Vec a n -> [a]
vFilter p Nil = []
vFilter p (Cons x xs)
| p x = x : vFilter p xs
| otherwise = vFilter p xs
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/Wednesday/Code.html
4/4