Skip to content

Instantly share code, notes, and snippets.

@mmakowski
Created June 14, 2012 18:08
Show Gist options
  • Save mmakowski/2931873 to your computer and use it in GitHub Desktop.
Save mmakowski/2931873 to your computer and use it in GitHub Desktop.
{-# 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment