Created
August 17, 2017 13:59
-
-
Save lehmacdj/fecafa2f5fcbed647b5864a1b8c7cc02 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Excercises given in: | |
[Origami Programming](http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/origami.pdf) | |
> {-# LANGUAGE OverloadedLists, TypeFamilies #-} | |
> {-# LANGUAGE ViewPatterns #-} | |
> {-# LANGUAGE ScopedTypeVariables #-} | |
> {-# LANGUAGE TemplateHaskell #-} | |
> import GHC.Exts (IsList, fromList, Item, toList) | |
> import Data.Maybe (isJust, fromJust) | |
> import Test.QuickCheck.All | |
> import Data.Char (digitToInt) | |
Here is a simple definition of a list as given in the paper. Where possible I | |
will duplicate the definitions rather than modifying to use standard library | |
functions. | |
> data List a = Nil | Cons a (List a) | |
> deriving (Show, Eq) | |
> | |
> wrap :: a -> List a | |
> wrap x = Cons x Nil | |
> | |
> nil :: List a -> Bool | |
> nil Nil = True | |
> nil (Cons _ _) = False | |
> | |
> asMaybe :: List a -> Maybe (a, List a) | |
> asMaybe Nil = Nothing | |
> asMaybe (Cons x xs) = Just (x, xs) | |
> | |
> reverseL :: List a -> List a | |
> reverseL = go Nil where | |
> go a Nil = a | |
> go a (Cons x xs) = go (Cons x a) xs | |
For convenience I also provide an instance of `IsList` for this data type. | |
> instance IsList (List a) where | |
> type Item (List a) = a | |
> fromList = foldr Cons Nil | |
> toList = foldL (:) [] | |
Here is the simple `foldL` function defined in the paper. | |
> foldL :: (a -> b -> b) -> b -> List a -> b | |
> foldL f e Nil = e | |
> foldL f e (Cons x xs) = f x (foldL f e xs) | |
The universal property is effectively the definition of this function | |
eta reduced. | |
Excercise 3.1: | |
h . foldL f e | |
Excercise 3.2: | |
> mapL :: (a -> b) -> List a -> List b | |
> mapL f = foldL (Cons . f) Nil | |
> | |
> appendL :: List a -> List a -> List a | |
> appendL = foldL Cons | |
> | |
> concatL :: List (List a) -> List a | |
> concatL = foldL appendL Nil | |
Excercise 3.3: | |
The insertion sort presented in the paper: | |
> isort :: Ord a => List a -> List a | |
> isort = foldL insert Nil | |
> where | |
> insert :: Ord a => a -> List a -> List a | |
> insert y Nil = wrap y | |
> insert y (Cons x xs) | y < x = Cons y (Cons x xs) | |
> | otherwise = Cons x (insert y xs) | |
> insert :: Ord a => a -> List a -> List a | |
> insert y Nil = wrap y | |
> insert y (Cons x xs) | y < x = Cons y (Cons x xs) | |
> | otherwise = Cons x (insert y xs) | |
Excercise 3.4: | |
> insert1 :: Ord a => a -> List a -> (List a, List a) | |
> insert1 y = foldL (\x (a, i) -> | |
> ( Cons x a | |
> , if y < x | |
> then Cons y (Cons x a) | |
> else Cons x i)) | |
> (Nil, Cons y Nil) | |
> prop_insert1 = \(y :: Int, fromList -> xs) -> | |
> insert1 y xs == (xs, insert y xs) | |
Definition of paramorphism: | |
> paraL :: (a -> (List a, b) -> b) -> b -> List a -> b | |
> paraL f e Nil = e | |
> paraL f e (Cons x xs) = f x (xs, paraL f e xs) | |
Excercise 3.5: | |
> insert_para :: Ord a => a -> List a -> List a | |
> insert_para y = paraL | |
> (\x (a, i) -> if y < x then Cons y (Cons x a) else Cons x i) | |
> (Cons y Nil) | |
> prop_insert_para = \(y :: Int, fromList -> xs) -> | |
> insert y xs == insert_para y xs | |
Definintion of unfold for lists: | |
> unfoldL' :: (b -> Maybe (a, b)) -> b -> List a | |
> unfoldL' f u = case f u of | |
> Nothing -> Nil | |
> Just (x, v) -> Cons x (unfoldL' f v) | |
> | |
> unfoldL :: (b -> Bool) -> (b -> a) -> (b -> b) -> b -> List a | |
> unfoldL p f g b = if p b then Nil else Cons (f b) (unfoldL p f g (g b)) | |
Excercise 3.6: | |
> unfoldL'_ :: (b -> Maybe (a, b)) -> b -> List a | |
> unfoldL'_ f = unfoldL (isJust . f) (fst . fromJust . f) (snd . fromJust . f) | |
> | |
> unfoldL_ :: (b -> Bool) -> (b -> a) -> (b -> b) -> b -> List a | |
> unfoldL_ p f g = unfoldL' (\b -> if p b then Just (f b, g b) else Nothing) | |
Definition of foldL' the dual of unfoldL' | |
> foldL' :: (Maybe (a, b) -> b) -> List a -> b | |
> foldL' f Nil = f Nothing | |
> foldL' f (Cons x xs) = f (Just (x, foldL' f xs)) | |
Excercise 3.8: | |
> foldL'_ :: (Maybe (a, b) -> b) -> List a -> b | |
> foldL'_ f = foldL (curry (f . Just)) (f Nothing) | |
> foldL_ :: (a -> b -> b) -> b -> List a -> b | |
> foldL_ f b = foldL' (\x -> if isJust x then uncurry f (fromJust x) else b) | |
Excercise 3.9: | |
> foldLargs :: (a -> b -> b) -> b -> (Maybe (a, b) -> b) | |
> foldLargs f b = (\x -> if isJust x then uncurry f (fromJust x) else b) | |
> unfoldLargs :: (b -> Bool) -> (b -> a) -> (b -> b) -> (b -> Maybe (a, b)) | |
> unfoldLargs p f g = (\b -> if p b then Just (f b, g b) else Nothing) | |
Selection sort as an unfold: | |
> delmin :: Ord a => List a -> Maybe (a, List a) | |
> delmin Nil = Nothing | |
> delmin xs = Just (y, deleteL y xs) | |
> where y = minimumL xs | |
> minimumL :: Ord a => List a -> a | |
> minimumL (Cons x xs) = foldL min x xs | |
> deleteL :: Eq a => a -> List a -> List a | |
> deleteL y Nil = Nil | |
> deleteL y (Cons x xs) | |
> | y == x = xs | |
> | otherwise = Cons x (deleteL y xs) | |
> ssort :: Ord a => List a -> List a | |
> ssort = unfoldL' delmin | |
Excercise 3.10: | |
> deleteL' :: Eq a => a -> List a -> List a | |
> deleteL' y = paraL (\x (xs, a) -> | |
> if y == x | |
> then xs | |
> else Cons x a) | |
> Nil | |
> prop_deleteL' = \(x :: Int, fromList -> y) -> deleteL x y == deleteL' x y | |
Excercise 3.11: | |
> delmin' :: Ord a => List a -> Maybe (a, List a) | |
> delmin' = undefined | |
Bubble sort: | |
> bubble :: Ord a => List a -> Maybe (a, List a) | |
> bubble = foldL step Nothing | |
> where | |
> step x Nothing = Just (x, Nil) | |
> step x (Just (y, ys)) | |
> | x < y = Just (x, Cons y ys) | |
> | otherwise = Just (y, Cons x ys) | |
Excercise 3.12: | |
> bubble' :: Ord a => List a -> List a | |
> bubble' = foldL step Nil | |
> where | |
> step x Nil = wrap x | |
> step x (Cons y ys) | |
> | x < y = Cons x (Cons y ys) | |
> | otherwise = Cons y (Cons x ys) | |
> prop_bubble' = \(fromList -> y :: List Int) -> bubble y == asMaybe (bubble' y) | |
Excercise 3.13: | |
> insert_unfold :: Ord a => a -> List a -> List a | |
> insert_unfold y xs = unfoldL' step (Just y, xs) | |
> where | |
> step (Nothing, Nil) = Nothing | |
> step (Just y', Nil) = Just (y', (Nothing, Nil)) | |
> step (Nothing, Cons x xs') = Just (x, (Nothing, xs')) | |
> step (Just y', Cons x xs') | |
> | y' > x = Just (x, (Just y', xs')) | |
> | otherwise = Just (y', (Nothing, Cons x xs')) | |
> -- this only holds for sorted lists but that is okay because insert needn't | |
> -- work with unsorted lists regardless | |
> prop_insert_unfold = \(x :: Int, fromList -> ys) -> | |
> insert x (ssort ys) == insert_unfold x (ssort ys) | |
Definition of apomorphism: | |
> apoL' :: (b -> Maybe (a, Either b (List a))) -> b -> List a | |
> apoL' f u = case f u of | |
> Nothing -> Nil | |
> Just (x, Left v) -> Cons x (apoL' f v) | |
> Just (x, Right xs) -> Cons x xs | |
That is, an apomorphism is a short circuiting unfold. | |
Excercise 3.14: | |
> insert_apo :: Ord a => a -> List a -> List a | |
> insert_apo y xs = apoL' step (Just y, xs) | |
> where | |
> step (Just y', Nil) = Just (y', Right Nil) | |
> step (Just y', Cons x xs') | |
> | y' > x = Just (x, Left (Just y', xs')) | |
> | otherwise = Just (y', Right (Cons x xs')) | |
> -- other equations are unreachable because we have already short | |
> -- circuited | |
> step _ = undefined | |
> -- similarly to above, only works on sorted lists | |
> prop_insert_apo = \(x :: Int, fromList -> ys) -> | |
> insert x (ssort ys) == insert_apo x (ssort ys) | |
Definition of hylomorphism: | |
> hyloL f e p g h = foldL f e . unfoldL p g h | |
this could also be defined as: | |
> hyloL' f e p g h b = if p b then e else f (g b) (hyloL f e p g h (h b)) | |
but in practice the compiler is good enough at stream fusion that fusing is not | |
necessary in this case | |
Exercise 3.15: | |
> toBinary :: String -> List Bool | |
> toBinary = reverseL | |
> . unfoldL (==0) ((==1).(`mod`2)) (`div`2) | |
> . snd | |
> . foldL stepFold (1, 0) | |
> . fromList | |
> where | |
> stepFold x (m, a) = (m * 10, a + m * digitToInt x) | |
> toInt :: List Bool -> Int | |
> toInt = snd . foldL stepFold (1, 0) where | |
> stepFold x (m, a) = (m * 2, a + m * intOf x) | |
> intOf True = 1 | |
> intOf False = 0 | |
> prop_toBinary (abs -> i) = show i == (show $ toInt $ toBinary $ show i) | |
Natural Numbers: | |
I slightly modify the definition to write this more easily | |
> data Nat = Z | S Nat | |
> deriving (Show, Eq, Ord) | |
Num instance for ergonomics | |
> instance Num Nat where | |
> fromInteger = unfoldN (==0) (+(-1)) | |
> (*) = mulN | |
> (+) = addN | |
> (-) = (fromJust .) . subN | |
> abs = id | |
> signum = const (S Z) | |
and natural numbers fold: | |
> foldN :: a -> (a -> a) -> Nat -> a | |
> foldN a f Z = a | |
> foldN a f (S k) = f (foldN a f k) | |
its the same as iter with arguments reversed | |
> iter :: Nat -> (a -> a) -> a -> a | |
> iter n f x = foldN x f n | |
Exercise 3.16: | |
> foldN' :: (Maybe a -> a) -> Nat -> a | |
> foldN' f Z = f Nothing | |
> foldN' f (S k) = f $ Just $ foldN' f k | |
> foldN_ :: a -> (a -> a) -> Nat -> a | |
> foldN_ a f = foldN' (\x -> if isJust x then f (fromJust x) else a) | |
> foldN'_ :: (Maybe a -> a) -> Nat -> a | |
> foldN'_ f = foldN (f Nothing) (f . Just) | |
Excercise 3.18: | |
> addN, mulN, powN :: Nat -> Nat -> Nat | |
> addN = flip foldN S | |
> mulN n = foldN Z (addN n) | |
> powN n = foldN (S Z) (mulN n) | |
Exercise 3.19: | |
> predN :: Nat -> Maybe Nat | |
> predN = foldN Nothing (maybe (Just Z) (Just . S)) | |
Exercise 3.20: | |
> subN :: Nat -> Nat -> Maybe Nat | |
> subN = flip foldN (>>= predN) . Just | |
> eqN :: Nat -> Nat -> Bool | |
> eqN n m = case subN n m of | |
> Just Z -> True | |
> _ -> False | |
> lessN :: Nat -> Nat -> Bool | |
> lessN = ((not . isJust) .) . subN | |
Unfolds for natural numbers | |
> unfoldN' :: (a -> Maybe a) -> a -> Nat | |
> unfoldN' f x = case f x of | |
> Nothing -> Z | |
> Just y -> S (unfoldN' f y) | |
> unfoldN :: (a -> Bool) -> (a -> a) -> a -> Nat | |
> unfoldN p f x = if p x then Z else S (unfoldN p f (f x)) | |
Exercise 3.21: | |
> unfoldN'_ f = unfoldN (isJust . f) (fromJust . f) | |
> unfoldN_ p f = unfoldN' (\x -> if p x then Nothing else Just (f x)) | |
Exercise 3.23: | |
> divN :: Nat -> Nat -> Nat | |
> divN n m = unfoldN' (flip subN m) n | |
Exercise 3.24: | |
> logN :: Nat -> Nat -> Nat | |
> logN n m = unfoldN (flip lessN m) (flip divN m) n | |
until function that models while loops | |
> untilN :: (a -> Bool) -> (a -> a) -> a -> a | |
> untilN p f x = foldN x f (unfoldN p f x) | |
here is a simple hylomorphism | |
> hyloN' :: (Maybe a -> a) -> (a -> Maybe a) -> a -> a | |
> hyloN' f g = foldN' f . unfoldN' g | |
Exercise 3.25: | |
> hyloN'_ :: (Maybe a -> a) -> (a -> Maybe a) -> a -> a | |
> hyloN'_ f g x = case g x of | |
> Nothing -> x | |
> y@(Just _) -> hyloN'_ f g (f y) | |
Exercise 3.28: | |
> fix_hyloL f = hyloL const undefined (const True) id f undefined | |
> -- hacky code to be able to test all properties at the same time | |
> return [] | |
> testAll = $quickCheckAll |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment