git.iko.soy/Haskell-HSE/haskell-lectures-2024
on main help sign in
Haskell-HSE/haskell-lectures-2024/5.Parametricity.md
126 lines 3.1 kB history raw
1import Control.Monad.ST (ST, runST)
2import Data.Foldable (for_)
3import Data.List (nub, partition)
4import Data.STRef (STRef)
5import GHC.Arr (STArray, elems, freezeSTArray, newSTArray, writeSTArray)
7-- Parametricity, polynomials and ST
9-- newtype State s a = State { runState :: s -> (s, a) }
11increment :: Int -> Int
12increment = (+ 1)
14increment' :: (Num a) => a -> a
15increment' = (+ 1)
17whatIsThis :: forall a. a -> a
18whatIsThis x = x -- ?
20-- parametricity
21-- Wadler: Theorems for free
23-- f :: forall a. a -> a
24-- g :: b -> c
25-- g . f = f . g
27map' :: forall a. (a -> a) -> [a] -> [a]
28map' = map
30-- g :: [a] -> [a]
31-- map' f . g = g . map' f
33f :: (Num a) => a -> a
34f x = x + 3 * x * x + x * x * x
36newtype Poly = Poly {runPoly :: forall a. (Num a) => a -> a}
38instance Num Poly where
39 Poly p + Poly q = Poly (\x -> p x + q x)
40 Poly p * Poly q = Poly (\x -> p x * q x)
41 abs (Poly p) = Poly (abs . p)
42 signum (Poly p) = Poly (signum . p)
43 negate (Poly p) = Poly (negate . p)
44 fromInteger c = Poly (const (fromInteger c))
46eval :: (Num a) => Poly -> a -> a
47eval (Poly p) = p
49subst :: Poly -> Poly -> Poly
50subst = eval
52newtype PolyN i = PolyN {runPolyN :: forall a. (Num a) => (i -> a) -> a}
54instance Num (PolyN i)
56eval' :: (Num a) => PolyN i -> (i -> a) -> a
57eval' (PolyN f) = f
59subst' :: PolyN i -> (i -> PolyN j) -> PolyN j
60subst' = eval'
62newtype Variables i = Variables {getVariables :: [i]}
64instance (Eq i) => Num (Variables i) where
65 Variables xs + Variables ys = Variables $ nub (xs <> ys)
66 Variables xs * Variables ys = Variables $ nub (xs <> ys)
67 abs (Variables xs) = Variables xs
68 signum (Variables xs) = Variables xs
69 fromInteger _ = Variables []
70 negate (Variables xs) = Variables xs
72variables :: (Eq i) => PolyN i -> [i]
73variables p = getVariables $ eval' p (Variables . (: []))
75-- data ST s a
77runST' :: (forall s. ST s a) -> a
78runST' = runST
80-- what if a is a type of mutable variables?
82-- STRef s a
84-- bad :: ST s (STRef s' Int)
85-- bad = _
87-- leak :: forall s. ST s Int
88-- leak = runST bad
90qsort :: (Ord a) => [a] -> [a]
91qsort [] = []
92qsort (x : xs) =
93 let (ys, zs) = partition (< x) xs
94 in qsort ys ++ x : qsort zs
96sort :: (Ord a) => [a] -> [a]
97sort xs = runST $ do
98 let range = (0, length xs - 1)
99 arr <- newSTArray range (head xs)
100 for_ (zip [0 ..] xs) $ \(i, x) -> writeSTArray arr i x
101 sortStep arr range
102 arr' <- freezeSTArray arr
103 return (elems arr')
105sortStep :: (Ord a) => STArray s Int a -> (Int, Int) -> ST s ()
106sortStep arr (l, r) = do
107 let m = l + (r - l) `div` 2
108 sortStep arr (l, m - 1)
109 sortStep arr (m, r)
110 merge arr (l, m, r)
112merge :: Ord a => STArray s Int a -> (Int, Int, Int) -> ST s ()
113merge = _
115newtype Gen s = Gen { genState :: STRef s Int }
117nextInt :: Gen s -> ST s Int
118nextInt = error "TODO"
120-- functor parametricity
121-- t = t * t | t + t | t -> t | mu x. t(x) | x
122-- fmap :: (a -> b) -> (f a, g a) -> (f b, g b)
123-- fmap :: (a -> b) -> Either (f a) (g a) -> Either (f b) (g b)
124-- fmap :: (a -> b) -> Fix (f a) -> Fix (f b)
125-- fmap :: (a -> b) -> a -> b
126-- fmap :: (a -> b) -> ((f a -> h) -> g a) -> ((f a -> h) -> g b)