1 TODO Лекция 0

2 TODO Лекция 1

3 TODO Лекция 2

4 TODO Лекция 3

5 TODO Лекция 4

6 TODO Лекция 5

7 TODO Лекция 6

8 Лекция 7

class Applicative m => Monad m where
  return :: a -> m a                -- return
  (>>=) :: m a -> (a -> m b) -> m b -- bind

Для Maybe:

instance Monad Maybe where
  return = Just

  Nothing >>= _ = Nothing
  Just a >>= f = f a

Пример для Identity

newtype Identity a = Identity { runIdentity :: a }

Инстанс монады тривиальный

Пример для Either

instance Monad (Either e)  where
  --snip--

NB: Здесь тип e фиксированый для одного монадического вычисления

Композиция функция для монад:

(<=<)  :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c
(>=>)  :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c

m >>= (f >=> g) ≡ m >>= f >>= g
m >>= (f <=< g) ≡ m >>= g >>= f
Ассоциативность

Пример монады []

instance Monad [] where
  return x = [x]

  l >>= f = concat (map f l)

(>>)  :: Monad m => m a -> m b -> mb
m >> k = m >>= \_ -> k

Пример

ghci> [True, False]  >> [1, 2, 3]
[1, 2, 3, 1, 2, 3]

guard для списка

guard :: Bool -> [()]
guard True  = [()]
guard False = []

Полиморфная сигнатура

guard :: (Alternative f) => Bool -> f ()

Бесполезный пример

ghci> [True, False, True]  >> [1, 2]
[1, 2, 1, 2, 1, 2]
ghci> [True, False, True] >>= \b -> guard b >> [1, 2]
[1, 2, 1, 2]

join :: Monad m => m (m a) -> m a

Нельзя написать валидный инстанс монады 😭

data BarBaz a = Bar a | Baz a a

liftM :: Monad m => (a -> b) -> m a -> m b

Альтернитвные булевские опрераторы

(||^), (&&^) :: m Bool -> m Bool -> m Bool

Законы монад

return a >>= f ≡ f a
m >>= return ≡ m
(m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)

Можем попробовать доказать законы руками

9 Лекция 8

9.1 Writer

newtype Wrtier w a = Writer { runWriter :: (a, w) }  -- a is value, w is log

instance Monoid w => Moand (Writer w) where
  return a = Writer (a, mempty)

  Writer (a, oldLog) >>= f = let Wrtier (b, newLog) = f a
                             in Writer (b, oldLog <> newLog)

Вспомогательные функции

tell       :: w -> Writer w ()
execWriter :: Writer w a -> w
writer     :: (a, w) -> Writer w a

Есть инстанс монады для пары, который работает как Writer
Writer не эффективный, кушает много памяти

9.2 Reader

newtype Reader e a = Reader { runReader :: e -> a } -- e is environment

instance Monad (Reader e) where
  return a = Reader $ \_ -> a

  m >>= f = Reader $ \r -> runReader (f $ runReader m r) r

Вспомогательные функции

ask   :: Reader e e
asks  :: (e -> a) -> Reader e a
local :: (e -> b) -> Reader b a -> Reader e a

Note: Typed holes — foo x = _x

9.3 State

newtype State s a = State { runState :: s -> (a, s) } 

instance Monad (State s) where
  return a = State $ \s -> (a, s)

  oldState >>= f = State $ \s -> let (a, newState) = runState oldState s
                                 in runState (f a) newState

Пример для стека

type Stack = [Int]

pop :: State Stack Int
pop = State $ \(x:xs) -> (x, xs)

push :: Int -> State Stack ()
push x = State $ \xs -> ((), x:xs)

Полезные функции

get       :: State s s
put       :: s -> State s ()
modify    :: (s -> s) -> State s ()
gets      :: (s -> a) -> State s a
withState :: (s -> s) -> State s a -> State s a
evalState :: State s a -> s -> a
execState :: State s a -> s -> s

Полезные функции для монадов

replicateM :: Moad m => Int -> m a -> m [a] 

forM_ :: (Monad m, Foldable t) => t a -> (a -> m b) -> m ()

9.4 Cont

addCPS :: Int -> Int -> ((Int -> r) -> r)
addCPS x y = \k -> k (x + y)

newtype Cont r a = Cont { runCont :: (a -> r) -> r }

10 Лекция 9

Почему не можем получит ввод с помощью функций

getChar :: Char 
get2Char :: [Char]
get4Char :: [Char]

Исопльзуем что-то вроде

getChar :: RealWorld -> (Char, RealWorld) 
get2Char :: ReadWorld -> ([Char], RealWorld)
get4Char :: ReadWorld -> ([Char], RealWorld)

do нотация

Полезные функции

sequence_ :: [IO a] -> IO ()

return не то чем кажется

Ленивость с файлами

FFI, IORef, IOArray, IOException, unsafePerformIO

OverloadedStrings

Text, ByteString используют unsafe операции, по использовать их безопасно

11 Лекция 10

newtype Parser a = Parser { runP :: String -> Maybe (a, String) }

Делаем простые парсеры, комбинируя их получаем более сложные

ok :: Parser ()
ok = Parser $ \s -> Just ((), s)

isnot :: Parser a -> Parser ()
isnot parser = Parser $ \s ->
  case runP parser s of
    Just _  -> Nothing
    Nothing -> Just ((), s)

eof :: Parser ()
eof = Parser $ \s ->
  case s of
    [] -> Just ((), "")
    _  -> Nothing


satisfy :: (Char -> Bool) -> Parser Char
satisfy p = Parser $ \s ->
  case s of
    [] -> Nothing
    (x:xs) -> if p x then Just (x, xs) else Nothing

notok :: Parser ()
notok = isnot ok

char :: Char -> Parser Hcar
char c = satisfy (== c)

--snip--

instance Functor Parser where
  fmap f (Parser parser) = Parser (fmap (first f) . parser)

instance Applicative Parser where
  pure a = Parser $ \s -> Just (s, s)

  Parser pf <*> Parser pa = Praser $ \s ->
    case pf s of
      Nothing -> Nothing
      Just (f, t) -> case pa t of
        Nothing -> Nothing
        Just (a, r) -> Just (f a, r)


instance Monad Parser where
  return = pure

  p >>= f = Parser $ \s ->
    case runP p s of
      Nothing -> Nothing
      Just (a, t) -> runP (f a) t

instance Aternative Parser
  --snip--

12 Лекция 11

12.1 Unit testing — `HSpec`

Может сам искать тесты в модулях с префиксом spec?

shouldSatisfy проверяет по предикату
shouldBe проверяет на равенство

hspecTestTree :: IO TestTree
hspecTestTree = testSpec "Simple parser" spec_Parser

spec_Parser :: Spec
spec_Parser = do
  describe "eof works" $ do
    it "eof no empty input" $
      runP eof "" `shouldSatisfy` isJust
    it "eof no non-empty input" $
      runP eof "x" `shouldSatisfy` isNothing
  describe "char works" $ do
    it "char parses character" $
      runP (char 'a') "abc" `shouldBe` Just ('x', "bc")

12.2 Property-based — `Hedgehog`

Пример: ∀ xs. reverse (reverse xs) ≡ xs

genIntList :: Gen [Int]
genIntList =
  let listLength = Range.linear 0 10000
  in Gen.List listLength Gen.enumBounded

prop_reverse :: Property
prop_reverse = property $
  forAll genIntList >>= \xs ->
  List.reverse (List.reverse xs) === xs

Shrinking — уменьшение размера теста до читабельного вида, который повторяет поведение

Проверка обратных

read        . show      ≡ id
decode      . encode    ≡ id
deserialize . serialize ≡ id

Проверка законов моноидов и пр..

(a <> b) <> c ≡ a <> (b <> c)
a <> mempty   ≡ a
mempty <> a   ≡ a

13 Лекция 12

Можем композировать функторы, аппликативы, и т.д.

newtype Compose f g a = Compose { getCompose :: f (g a) }

instance (Functor f, Functor g) => Functor (Compose f g)
instance (Foldable f, Foldable g) => Foldable (Compose f g)
instance (Applicative f, Applicative g) => Applicative (Compose f g)
--snip--

Но не монад

Для Maybe

newtype MaybeIO = MaybeIO { runMaybeIO :: IO (Maybe a) }

instance Monad MaybeIO where
  return x = MaybeIO (return (Just x))
  MaybeIO action >>= f = MaybeIO $ do
    result <- action
    case result of
      Nothing -> return Nothing
      Just x -> runMaybeIO (f x)

Проблема

result <- runMaybeIO $ do
  c1 <- MaybeIO $ tryConnect "host1"
  print "Hello"
  c2 <- MaybeIO $ tryConnect "host2"

print возвращает не Maybe

transformIO2MaybeIO :: IO a -> MaybeIO a
transformIO2MaybeIO action = MaybeIO $ do
  result <- action
  return (Just result)

Первый трансформер

newtype MaybeT m a = MaybeT { runMaybeT :: m (Maybe a) } 

type MaybeIO = MaybeT IO

instance Monad m => Monad (MaybeT m) where
  return x = MaybeT (return (Just x))
  MaybeT action >>= f = MaybeT $ do
    result <- action
    case result of
      Nothing -> return Nothing
      Just x -> runMaybeT (f x)

transformIO2MaybeT :: Functor m => m a -> MaybeT m a
transformIO2MaybeT action = MaybeT . fmap Just

Класс трансформеров

class MonadTrans t where
  lift :: Monad m => m a -> t m a

lift . return ≡ return
lift (m >>= f) ≡ lift m >>= (lift . f)

Пример для Reader

newtype ReaderT r m a = Reader T { runReaderT :: r -> m a }

type Reader r a = ReaderT r Identity a
type LoggerIO a = ReaderT LoggerName IO a

инстанс монады для ReaderT почти такой же как и для Reader

NB Таблица трансофрмеров

Base Monad	Transormer	Original Type	Combined Type
`Maybe`	`MaybeT`	`Maybe a`	`m (Maybe a)`
`Either`	`EitherT`	`Either a b`	`m (Either a b)`
`Writer`	`WriterT`	`(a, w)`	`m (a, w)`
`Reader`	`ReaderT`	`r -> a`	`r -> m a`
`State`	`StateT`	`s -> (a, s)`	`s -> m (a, s)`
`Cont`	`ContT`	`(a -> r) -> r`	`(a -> m r) -> m r`

IO не может быть трансформером

Проблема: Если трансформеров много, то придется писать много lift

Все выше в пакете transformers. Пакет mtl решает эту проблему

class Monad m => MonadReader r m | m -> r where
  ask :: m r
  --snip--

instance Monad m => MonadReader r (ReaderT r m) where
  --snip--

instance Monad m => MonadReader r (StateT s m) where
  ask = lift ask
  --snip--

class Monad m => MonadThrow m where
  throwM : Exception e => e -> m a

class MonadThrow m => MonadCatch m where
  catch :: Exception e => m a -> (e -> m a) -> m a

ThrowError – когда надо сломать все

Можем испольовать deriving и mtl

newtype M a = M(ReaderT Environment (StateT MyState IO) a)
  deriving (Functor, Applicative, Monad, MonadIO, MonadState MyState, MonadReader Environment)

Заворачивать IO только в ReaderT
Использовать конкретную монаду, если конечно не пишите либу

14 Лекция 13

Слайды

Конкатенация списков за O(1)

newtype DList a = DL { unDL :: [a] -> [a] }

fromList :: [a] -> DList a
fromList l = DL (l++)

toList :: DList a -> [a]
toList (DL lf) = lf []

append :: DList a -> DList a -> DList a
(DL f) `append` (DL g) = DL $ \xs -> f (g xs) -- append = mappend = <>

Откладываем операции конкатенации, до тех пор. пока нам не понадобится результат, который вычислится за длину списка, благодаря правильному порядку аргументов ++

Игрушечная реализация seq — форсит вычисление первого аргумента до WHNF

seq :: a -> b -> b
_|_ `seq` _ = _|_
_   `seq` b = b

foldl, foldr медленные
foldl' — строгая версия, использует seq

deepseq как seq, но вычисляет до нормальной формы. Чтобы компилятор знал, как вычислять вашу структуру до нормальной формы, нужно заинстансировать NFData

class NFData a where
  rnf :: a -> ()
  rnf a = a `seq` ()

instance NFData a => NFData (Maybe a) where
  rnf Nothing = ()
  rnf (Just x) = rnf x

instance NFData a => NFData [a] where
  rnf [] = ()
  rnf (x:xs) = rnf x `seq` rnf xs


deepseq :: NFData a => a -> b -> b
a `deepseq` b = rnf a `seq` b

-XBangPatterns — можно ставить ! перед паттерном чтобы вычислить его до WHNF — сахар для seq

-XIrrefutablePatterns

f :: (a, b) -> Int
f (a, b) = const 1 a -- f undefined падает

g :: (a, b) -> Int
g ~(a, b) = const 1 a -- g undefined не падает

Можем форсить вычисление полей

data Config = Config
  { user : !Int
  , extra :: !Maybe Settings
  } deriving (Show)

-XStrictData — строгие поля по умолчанию
-XStrict — строгость по умолчанию

Когда стоит форсить:

Программа медленная или выходит за димит стека
Арифметические операции
Уменьшить рост вызовов
- f x = g$! (h x)
- f x = g x
- f !x = g (h x)
Поля структур

15 Лекция 14

Проблема: `map f . map g` медленнее чем map (f. g)

Deforestataion: Можем разворачивая, сворачивая функции можем делать эвристические оптимизации

func = foldr (+) 0 . map (*10)

func l = case l of
  [] -> 0
  (y:ys) -> 10 * y + func ys

Игрушечный поток

newtype List a = List ([a] -> Maybe (a, [a]))

map1 : (a -> b) -> List a -> List b
map1 g (List f) = List h
  where
    h s' = case f s' of
      Nothing -> Nothing
      Just (x, s'') -> Just (g x, s'')

Проблема: типы не сойдутся

Норм версия

data List a b = List ([a] -> Maybe (b, [a]))  [a]

unfoldr :: b -> ([a] -> Maybe (b, [a]))  -> [a]

Добавим возможность скипать элементы стрима

data Step s a = Done
              | Skip    s
              | Yield a s

data Stream a = forall s. Stream (s -> Step s a) s

stream :: forall a. [a] -> Stream a
stream xs = Stream next xs
  where
    next :: [a] -> Step [a] a
    next [] = Done
    next (x:xs) = Yield x xs

unstream :: forall a. Stream a -> [a]
unstream (Stream next s0) = go s0
  where
    go s = case next s of
             Done -> []
             Skip s' -> go s'
             Yield a s' -> a : go s'

Альтернативные функции

mapS :: forall a b. (a -> b)-> Stream a -> Stream b
mapS f (Stream next s) = Stream next' s
  where
    next' xs = case next xs of
                 Done -> Done
                 Skip s' -> Skip s'
                 Yield a s' -> Yield (f a) s'

mapS :: forall a. (a -> Bool)-> Stream a -> Stream b
mapS p (Stream next s) = Stream next' s
  where
    next' xs = case next xs of
                 Done -> Done
                 Skip s' -> Skip s'
                 Yield a s' -> if p a then Yield a s' else Skip s'

Rewrite rule:

map s = unstream . mapS s . stream
filter s = unstream . filterS s . stream

foo = map show . filter even

foo раскрывается в foo s = unstream . mapS s . stream . unstream . filterS s . stream Можем написать правило чтобы компилятор сворачивал stream (unstream s)

{-# RULES "stream/unstream"
    forall (s :: Stream a). stream (unstream s) = s
#-}

ST монада — что-то вроде IO, но без доступа к внешнему миру

16 Лекция 15

Используются зеленые потоки, плюс есть т.н. spark’и — еще более легковесная единица выполнения

forkIO :: IO () -> IO ThreadId

Можем указать флаги +RTS -N2 чтобы программа выполнялась в 2х потоках

data MVar a

Можем достать/полоить с ожиданием, внутри используется блокировка. Могут быть выкинуты исключения при успешной попытке задетектить deadlock.

throwTo :: Exception e => ThreadId -> e -> IO()
killThread :: ThreadId -> IO()

Кидает AsyncException исключение в поток

Можно ловить исключения. сигналы(SIGINT и пр.) - тоже исключения

handle :: Exception e => IO a -> (e -> IO a) -> IO a
handle :: Exception e => (e -> IO a) -> IO a -> IO a

mask_ :: IO a -> IO a

Если обернуть действие в mask_ то это действие не может быть убито.

bracket, finally — идиома RAII

forkIO плоха

17 Лекция 16

STM монада позволяет делать атомарные действия с аналогами MVar.

Распараллеливание читсых функций. Монада Eval

runEval $ do
   a <- rpar (f x)
   b <- rpar (f y)
   return (a, b)

Рантайм сам позаботиться об ожидании потоков, когда произойдет попытка получить зание a или b. rseq позволяет явно подождать вычисление?

runEval $ do
   a <- rpar (f x)
   b <- rseq (f y)
   return (a, b)

18 Лекция 17

18.1 Линзы

Проблема: Сеттеры для record’ов больно

Lens(obj, field) — пара из геттера и сеттера

data Lens obj field = Lens
  { view :: obj -> field
  , set :: field -> obj -> obj
  }

view :: Lens obj field -> obj -> field
set  :: Lens obj field -> field -> obj -> obj

over :: Lens obj field :: (field -> field) -> (obj -> obj)
over lens updated obj = set lens (updater $ view lens obj) obj

Удобнее следующая реализация

data Lens obj field = Lens
  { view :: obj -> field
  , over :: (field -> field) -> (obj -> obj) }

Пример:

data Person = Person
  { name :: String
  , age  :: Int
  , address :: Address
  }
data Address = Address
  { house :: Int
  , street :: Street
  , city :: City}

newtype City = City String
newtype Street = Street String

personAddressLens :: Lens Person Address
personAddressLens = Lens address (\fn obj -> obj { address = fn (address obj) })

addressCityLens :: Lens Address City
addressCityLens = Lens city (\fn obj -> obj { city = fn (city obj) })

Попробуем сделать композицию этих линз

personCityLens :: Lens Person City
personCityLens =
  Lens (city . address)
  (\cityFn person -> person
     { address = address person
       { city = cityFn $ city $ address $ person }
     }
  )

Упростим

personCityLens :: Lens Person City
personCityLens =
  Lens (view addressCityLens . view personAddressLens)
       (over personAddressLens . over addressCityLens)

Сделаем функцию для композиции:

(.>)  :: Lens obj field
      -> Lens field subfield
      -> Lens obj subfield
o2f .> f2s = Lens (view f2s . view o2f)
                  (over o2f . over f2s)

На самом деле используется одна функция объединяющая view и over

type Lens s t a b = forall f. Functor f => (a -> f b) -> (s -> f t)
type Lens' s a = Lens s s a a
type Lens' s a = forall f. Functor f => (a -> f a) -> (s -> f s)

view :: S -> a
over :: (a -> a) -> (S -> S)

Добавим Identity к over

type LensOver s a = (a -> Identity a) -> (s -> Identity s)

over :: LensOver s a -> (a -> a) -> (s -> s)
over lens f x = runIdentity (lens (Identity . f) x)

Попробуем сделать view

type LensGetter s a = (a -> Const a a) -> (s -> Const a s)

get :: LensGetter s a -> s -> a
get lens x = getConst (lens Const x)

lens :: (s -> a)  -> (s -> a -> s) -> Lens' s a
lens get set f s = set s <$> f (get s)

19 Лекция 18

19.1 Traverse

Зачем нужны линзы с 4 типовыми параметрами

data Person a = Person
  { name :: String
  , age :: a
  ]}

Traversal' компиозируется с Lens'. Заметим что Traversal — частный случай Lens

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> (s -> f t)
type Traversal' obj field = forall f. Applicative f => (field -> f field) -> (obj -> f obj)

class (Functor t, Foldable t) => Traversable r where
  traverse :: Applicative f => (a -> f b) -> (t a) -> f (t b)

traversed :: Traversable t => Traversal' (t a) a
traversed = traverse

(.) :: Lens' a b -> Traversal' b c -> Traversal a c

Можем использовать например:

unit :: Lens' Game [Unit]
unit.traversed :: Traversal' Game Unit
unit.traversed.health :: Traversal' Game Int

Хотим получить все объекты на которые сфокурисованы, положить в список

data Endo = Endo { appEndo :: a -> a}

type Getting r s a = (a -> Const r a) -> s -> Const r s

toListOf :: Getting (Endo [a]) s a -> s -> [a]
(^..) :: s -> Getting (Endo [a]) s a -> [a]

game^..unit.traversed.health :: Lens' Game [Int] -- ???

zoom:

partyLoc :: Traversal' Game Point
partyLoc = unit.travesred.position

retreat :: StateT Game IO ()
retreat = do
  lift $ putStrLn "Retreat!"
  zoom partyLoc $ do
    x += 10
    y += 10

battle :: StateT Game IO ()
battle = do
  --snip--
  zoom (boss.position) $ do
    x += 10
    y += 10

19.2 Призмы

type Prism s t a b = forall p f. (Choice p, Applicative f) => p a (f b) -> p s (f t)

preview :: Prism' s a -> s -> Maybe a
review :: Prism' s a -> a -> s

Пример для Either и Maybe

_Left :: Prism' (Either a b) a
_Just :: Prism' (Maybe a) a

ghci> preview _Left (Left "hi")
Just "ho"
ghci> preview _Left (Right "hi")
Nothing

ghci> review _Left "hi"
Left "hi"

Более сложный пример:

data X = mkX { _fieldX :: String }
data C = MkC1 X | MkC2 Y
data B = MkB { _fieldB :: C }
data A = MkA { _fieldA :: [B] }

foo :: A

Как изменить fieldX в A, только если он в X

foo & fieldA.traversed.fieldB._MkC1.fieldX .~ "New string"

20 Лекция 19

Можем использовать Сишный препроцессор

Можем генерировать линзы написав просто makeLenses ''Game

Напишем генерацию функции получения первого аргумента тюплов разного размера:

VarP :: Name -> Pat
VarE :: Name -> Exp

newName :: String -> Q Name
varE :: Name -> Q Expr
varP :: Name -> Q Pat

Как выглядит код \(x, _, _) -> x в AST

LamE [TupP [VarP x_1, WildP, WildP]] (VarE x_1)

fst3 = do
  x <- newName "x"
  lamE [tupP [varP x, wildP, wildP]] (varE x) -- \(x, _, _) -> x

fst3 :: Q Expr
$(fst3) :: (t2, t1, t) -> t2

ghci> $(fst3) (1, 2, 3)
1

fstN = do
  x <- newName "x"
  lamE [tupP $ varP x : replicate (n - 1) wildP] (varE x) -- \(x, _, _, ... , _) -> x

NB: Использование и сами макросы должны быть в разных модулях

-XQuasiQuotes: Теперь может писать AST не ручками а в [|...|]

ghci> runQ [| \x -> x |]
LamE [VarP x_0] (VarE x_0)

Чтобы распарсить другие штуки, специально это бозначаем:

Объявление: [d|..|]
Выражение: [e|..|]
Тип: [t|..|]
Паттерн: [p|..|]
Библиотеки могут предоставлять свои форматы, например форматированый текст

20.1 DSLки

Попробуем сделать DSL для арифметичских выражений

data ArithExpr = AENum Int
               | AEPlus ArithExpr ArithExpr
               | AEAnd ArithExpr ArithExpr
               | AEGt ArithExpr ArithExpr

Проблема: можем складывать булы

-XGADTs:

data ArithExpr a where
  AENum :: Int -> ArithExpr Int
  AEPlus :: ArithExpr Int -> ArithExpr Int -> ArithExpr Int
  AEAnd :: ArithExpr Bool -> ArithExpr Bool -> ArithExpr Bool
  AEGt :: ArithExpr Int -> ArithExpr Int -> ArithExpr Bool

Теперь не можем написать некоректное выражение

В тоже время, если попробуем написать парсер для таких выражений, то просто не сможем этого сделать. Следующий код не компилируется:

parse :: String -> Maybe (ArithExpr a)
parse "1" = Just (AENum 1)
parse _ = Nothing

Используем экзистенциальные типы:

data SomeAE where
  SomeAE :: Show a => ArithExpr a -> SomeAE

interpret :: ArithExpr a -> a

parse :: String -> Maybe SomeAE
parse "1" = Just (SomeAE $ AENum 1)
parse "1+2" = Just $ SomeAE $ AENum 1 `AEPlus` AENum 2
parse _ = Nothing

interpretShow :: SomeAE -> String
interpretShow (SomeAE expr) = show (interpret expr)

Альтернативный синтаксис с использованием -XExistentialQuantification

data SomeAE = forall a. Show a => SomeAE (ArithExpr a)

Хотим попробовать получить Int из interpret. Можем получать информацию о типе в рантайме

data SomeAE where
  SomeAE :: (Typeable a, Show a) => ArithExpr a -> SomeAE

class Typeable (a :: k)

data a :~: b where
  Refl :: a :~: a

eqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)

parseInt :: String -> Maybe (ArithExpr Int)
parseInt s = parse s >>=
  \(SomeAE (expr :: ArithExpr t)) ->
    do
      Refl <- eqT @t @Int
      pure expr

21 Лекция 20

21.1 Где используем `forall`

-XRankNTypes

applyToTuple :: (forall a. [a] -> Int) -> ([b], [c]) -> (Int, Int)
applyToTuple f (x, y) = (f x, f y)

Вспомним ST:

runSt :: forall a. (forall s. ST s a)  -> a

newSTRef :: forall a s. a -> ST s (STRef s a)
readSTRef :: forall a s. STRef s a -> ST s a
writeSTRef :: forall a s. STRef s a -> a -> ST s ()

Не можем использовать ST монаду немонадически. Не можем хакнуть ST монаду

changeVarWrong var =
  let _ = runST $ writeSTRef var 10
      _ = runST $ writeSTRef var 42
  in var

Не можем применить тип, т.к. тип s внутри. То есть тип s — маркер контекста, уникальный для него

В дататипах

data Ctx = Ctx { modulus :: Int }

newtype Action a = Action
  { runAction :: forall m. (MonadReader Ctx m, MonadCatch m) => m a }

Это не экзистенциальный тип!

-XScopedTypeVariables

21.2 Final tagless DSLs

Вместо вышеописанного дататайпа ArithExpr:

class ArithExpr expr where
  aeNum :: Int -> expr Int
  aePlus :: expr Int -> expr Int -> expr Int
  aeAnd :: expr Bool -> expr Bool -> expr Bool
  aeGt :: expr Int -> expr Int -> expr Bool

newtype ToS a = ToS { toString :: String }
  deriving (Show, Semigroup)

castTS :: ToS a -> ToS b
castTS (ToS s) = ToS s

instance ArithExpr ToS where
  aeNum = ToS . show
  aePlus a b = a <> (ToS " + ") <> b
  aeAnd a b = a <> (ToS " && ") <> b
  aeGt a b = castTS a <> (ToS " > ") <> castTS b

22 Лекция 21

Про кайнды

newtype ReaderT r (m :: * -> *) (a :: *) = ReaderT { runReaderT :: r -> m a }
ReaderT :: * -> (* -> *) -> * -> *

class Num a where
  --snip--

Num :: * -> Constraint

Можем делать алиасы для констрейнтов

type MyConstraint a = (Reade a, Num a, Show a)

foo :: MyConstraint a => String -> a -> a

type ConstraintEndomorphism p a = p a => a -> a
ConstraintEndomorphism :: (* -> Constraint) -> * -> *

-XTypeOperators

data a * b = Mult a b
(*) :: Num a => a -> a -> a -- type
(*) :: * -> * -> * -- kind

22.1 Кастомный кайнды

data Z
data S n

data Vec :: * -> * -> * where
  Nil :: Vec a Z
  Cons :: a -> Vec a n -> Vec a (S n)


v2 :: Vec Int (S (S Z))
v2 = 1 `Cons` (2 `Cons` Nil) -- ok

v3 :: Vec Int Char -- не хотим чтобы это было валидно
-- v3 = ??

Если включить -XDataKinds, для каждой data создается соответствующий кайнд

data Nat = Z | S Nat

data Vec :: * -> Nat -> * where
  Nil :: Vec a Z
  Const :: a -> Vec a n -> Vec a (S n)

data Nat = Zero | Succ Nat

Succ :: Nat -> Nat -- type
Nat :: * -- kind

С расширением

Succ :: Nat -> Nat -- kind

type Two = 'Succ ('Succ 'Zero)
Two :: Nat -- kind

С апострофами типы. без — типовой конструктор

Пример для листов, -XTypeOperators

Prelude> :set -XDataKinds
Prelude> :k '[]
'[] :: [a]
Prelude> :k '[Int, Bool]
'[Int, Bool] :: [*]
Prelude> :k '[Maybe, Either String]
'[Maybe, Either String] :: [* -> *]
Prelude> :set -XTypeOperators
Prelude> :k (Int ': '[Bool])
(Int ': '[Bool]) :: [*]

С такими строгими списками, можем сделать zip только для списков одинаковой длинны

Гетерогенные списки:

data HList :: [*] -> * where
  HNil :: HList '[]
  (:^) :: a -> HList t -> HList (a ': t)

infixr 2 :^

foo0 :: HList '[]
foo0 = HNil

foo1 :: HList '[Int]
foo1 = 3 :^ HNil

foo2 :: HList '[Int, Bool]'
foo2 = 5 :^ False :^ HNil

Show для этой фигни

instance Show (HList '[]) where
  show _ = "H[]"

instance (Show e, Show (HList l)) => Show (HList (e ': l)) where
  show (x :^ l) = let 'H' : '[' : s = show l
                  in "H[" ++ show x ++ (if s == "]" then s else ", " ++ s)

Числа на уровне типов:

data Vec :: * -> Nat -> * where
  Nil :: Vec a 0
  (:>) :: a -> Vec a n -> Vec a (n + 1)

newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a)

clearPage :: ArrPtr 4096 Word8 -> IO ()

23 Лекция 22

Как сделать +?

newtype Foo bar = MkFoo { unFoo :: bar }

MkFoo :: bar -> Foo bar -- (term level)
Foo :: * -> * -- (type level)

data Foo a where
  Foo :: Int -> Foo Int
  Bar :: Char -> Foo Double

Foo :: Int -> Foo Int -- (term level)
Bar :: Char -> Foo Double -- (term level)
Foo :: * -> * -- (type level)

Хотим писать что-то вроде

type fun Foo a where
  | a == Char = Double
  | otherwise = a

23.1 Type and data families

-- открытая type family
type family Foo var :: * where
  Foo Char = Double
  Foo b = b

-- закрытая type family
type family Foo bar :: *
type instance Foo Char = Double
type instance Foo Int = Int

-- так нельзя! (можно только в открытых)
type family Foo bar :: *
type instance Foo Char = Double
type instance Foo a = a

data family Foo bar :: *
data instance Foo Int = MkFoo Int

class Foo p where
  type AType p :: *
  data BType p :: *

  make :: AType p -> BType p

instance Foo Int where
  type AType Int = Int
  data BType Int = B Integer

  make = B .toInteger

type family FromMaybe (m :: Maybe *) (def :: *) :: * where
  FromMaybe ('Just t) def = t
  FromMaybe 'Nothing def = def

FromMaybe ('Just Int) Bool ~ Int

type family Foo bar :: * where
  Foo Char = Double
  Foo a = a

show' :: Show (Foo a) => Foo a -> String
show' = show

В кратце: компилятору нужна инъеткивность типа a в show'. Это решается следующим:

{-# LANGUAGE TypeFamilyDependencies #-}

type family Foo a = r | r -> a where
  Foo Char = Double
  Foo Int = Int

Через r -> a обещаем инъективность. Пришлось убрать полиморфный паттерн, т.к. он нарушает инъективность. Теперь show' работает

23.2 `Free` Monad

data Free f a = Pure a | Free (f (Free f a))

instance Functor f => Monad (Free f) where
  return = pure

  Pure a >>= f = f a
  Free m >>= f = Free ((>>= f) <$> m)

24 DRIFTED Лекция 23

class Functor w => Comonad w where
  extract :: w a -> a
  duplicate :: w a -> w (w a)
  extend :: (w a -> b) -> w a -> w b

(=>>) :: Comonad w => w a -> (w a -> b) -> w b

Определения по умолчанию

duplicate w = extend id w
extend f w = fmap f (duplicate w)

Простой пример:

data Identity a = Identity { runIdentity :: a } 

instance Comonad Indetity where
  extract = runIdentity
  duplicate = Identity

Maybe, [] не комонады(нельзя сделать extract), а NonEmpty вполне себе.

Двойственность в монаде:

return  :: a -> m a
extract :: a <- m a


(>>=) :: m a -> (a -> m b) -> m b
(=>>) :: m a <- (a <- m b) <- m b


join     :: m (m a) -> m a
dupicate :: m (m a) <- m a

Незакончено