Created
June 14, 2012 18:08
-
-
Save mmakowski/2931873 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
{-# 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