public
Created

  • Download Gist
gistfile1.hs
Haskell
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
{-# Language ViewPatterns, GADTs, KindSignatures #-}
import Data.List
 
{-
catamorphisms: folds
anamorphisms: unfolds
 
foldr vs foldl: foldl is almost never the right thing to use, use foldl' instead, which is a strict version
(optimiser will do this for us)
-}
 
foldr2 :: (a -> b -> b) -> b -> [a] -> b
foldr2 f b [] = b
foldr2 f b (h:t) = f h (foldr2 f b t)
 
-- easy to visualise with the list tree: it replaces the cons nodes (:) with f and nil ([]) with b
 
foldr3 :: ((a, b) -> b, () -> b) -> [a] -> b
foldr3 (f, b) [] = b ()
foldr3 (f, b) (h:t) = f (h, foldr3 (f, b) t)
 
{-
-- these two functions correspond to list type constructors:
-- data List a = Cons a (List a) -- (a, b) -> b
-- | Nil -- () -> b
 
 
this view lets us generalise folds. What's the "shape" of list type?
- 2 alternatives
- in 1st, there are two values combined
- in 2nd, empty
 
it's a sum of products.
Products are modelled using tuples: (a, List a)
Unions are modelled using Either, so:
 
type List' a = Either () (a, List' a)
 
1:2:3:4:[]
R (1, R(2, R(3, R(4, L ()))))
 
these two things are isomorphic.
 
-}
 
foldr4 :: (Either (a, b) () -> b) -> [a] -> b
foldr4 f [] = f $ Right ()
foldr4 f (h:t) = f $ Left (h, foldr4 f t)
 
-- a simple equivalence that lets us use a single function that combines the two cases above
 
-- aside: turning a pair of functions into function of Either:
 
pair2either :: (a -> c, b -> c) -> Either a b -> c
pair2either (f, g) (Left a) = f a
pair2either (f, g) (Right b) = g b
 
{-
but why are we doing this? To generalise foldr to our own data type.
All we need is generalise the type of the function; we should always be able to represent the shape of our ADT
as Eithers and pairs, and then have appropriate cases
 
if we have multiple data constructors -> nest eithers
if we have more than two types in a product -> nest pairs
 
 
But this is not all; we can unfold lists:
-}
 
stars :: Int -> String
stars = unfoldr go
where
go :: Int -> Maybe (Char, Int)
go 0 = Nothing
go n = Just ('*', n - 1)
 
-- this can be generalised as well by switching to paris and eithers!
 
unfoldr2 :: (b -> Either (a, b) ()) -> b -> [a]
unfoldr2 f (f -> Right ()) = []
unfoldr2 f (f -> Left (h, unfoldr2 f -> t)) = (h:t)
 
{-
(this uses view pattern: f -> x says that before pattern matching we apply f to x and pattern match on the result)
note that this is the inverse of foldr4
 
-}
 
stars2 :: Int -> String
stars2 = unfoldr2 go
where
go :: Int -> Either (Char, Int) ()
go 0 = Right ()
go n = Left ('*', n - 1)
 
 
-- if we don't care too much about that nice symmetry, we can rewrite unfoldr2 without view patterns:
 
unfoldr3 :: (b -> Either (a, b) ()) -> b -> [a]
unfoldr3 f b = case f b of
Right () -> []
Left (h, b') -> case (unfoldr3 f b') of t -> (h:t)
 
{-
Since there is no generalisation of Either to 3, 4 etc. we have to nest them, and it gets messy.
 
Can we write a general unfold that works for any data type? Idea:
 
-- X []
-- X (:) :$ '*' :? (n - 1)
 
Lost? Let's try to explain, but first a quick demo of GADTs...
-}
 
data List a = Nil | Cons a (List a)
 
data List2 :: * -> * where
Nil2 :: List2 a
Cons2 :: a -> List2 a -> List2 a
 
-- basically, GADTs provide more flexible, function-like syntax
 
 
{-
 
data X :: * -> * where
X :: a -> X a
(:$) :: X (a -> b) -> a -> X b
(:?) :: X (a -> b) -> s -> X b
 
Well, this is not gonna work, the (:?) is dodgy
 
let's try to work out what types we need:
X (:) :: X (a -> ([a] -> [a]))
X (:) :$ '*' :: X (String -> String)
X (:) :$ '*' :? (n-1) :: X String
 
Hmm, we might need this:
-}
 
data X :: * -> * -> * -> * where
X :: a -> X c s a
(:$) :: X c s (a -> b) -> a -> X c s b
(:?) :: X c s (c -> b) -> s -> X c s b
 
{-
s -- the seed (Int in our case)
c -- the final type we are constructing (String)
 
now:
 
go :: Int -> X String Int String
-}
 
{-
Why don't we just do an ordinary anamorphism on an unfixed data type? Because we don't want to have to unfix our type!
 
So, we were defeated during the session, but look what Peter did on his train home:
-}
 
unf :: forall s c . (s -> X c s c) -> s -> c
unf f = go . f
where
go :: X c s b -> b
go (X x) = x
go (x :$ v) = go x v
go (x :? s) = go x (unf f s)
 
stars3 :: Int -> String
stars3 n = unf go n
where
go :: Int -> X String Int String
go 0 = X []
go n = X (:) :$ '*' :? (n - 1)

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.