ТЛ; др
{-# LANGUAGE InstanceSigs #-}
newtype Id t = Id t
instance Monad Id where
return :: t -> Id t
return = Id
(=<<) :: (a -> Id b) -> Id a -> Id b
f =<< (Id x) = f x
Пролог
Оператор приложения $ функций
forall a b. a -> b
канонически определено
($) :: (a -> b) -> a -> b
f $ x = f x
infixr 0 $
в терминах применения функции на Хаскелле f x (infixl 10).
Композиция . определяется в терминах $ как
(.) :: (b -> c) -> (a -> b) -> (a -> c)
f . g = \ x -> f $ g x
infixr 9 .
и удовлетворяет эквивалентности forall f g h.
f . id = f :: c -> d Right identity
id . g = g :: b -> c Left identity
(f . g) . h = f . (g . h) :: a -> d Associativity
. является ассоциативным, а id - его правая и левая идентичность.
Тройной Клейсли
В программировании монада - это конструктор типа функтора с экземпляром класса типа монады. Существует несколько эквивалентных вариантов определения и реализации, каждый из которых несет в себе несколько разные представления об абстракции монады.
Функтор - это конструктор типа f вида * -> * с экземпляром класса типа функтора.
{-# LANGUAGE KindSignatures #-}
class Functor (f :: * -> *) where
map :: (a -> b) -> (f a -> f b)
В дополнение к следующему статически обязательному протоколу типов экземпляры класса функторов должны подчиняться алгебраическим законам функторов forall f g.
map id = id :: f t -> f t Identity
map f . map g = map (f . g) :: f a -> f c Composition / short cut fusion
Функтор Вычисления имеют тип
forall f t. Functor f => f t
Вычисление c r состоит из результатов r в контексте c.
Унарные монадические функции или Стрелки Клейсли имеют тип
forall m a b. Functor m => a -> m b
Стрелки Kleisi - это функции, которые принимают один аргумент a и возвращают монадическое вычисление m b.
Монады канонически определены в терминах тройки Клейсли forall m. Functor m =>
(m, return, (=<<))
реализовано как класс типов
class Functor m => Monad m where
return :: t -> m t
(=<<) :: (a -> m b) -> m a -> m b
infixr 1 =<<
Идентификатор Клейсли return - это стрелка Клейсли, которая переводит значение t в монадический контекст m. Расширение или Приложение Kleisli =<< применяет стрелку Клейсли a -> m b к результатам вычисления m a.
Клейсли состав <=< определяется в терминах расширения как
(<=<) :: Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
f <=< g = \ x -> f =<< g x
infixr 1 <=<
<=< составляет две стрелки Клейсли, применяя левую стрелку к результатам применения правой стрелки.
Экземпляры класса типа монады должны подчиняться законам монады , наиболее элегантно сформулированным с точки зрения композиции Клейсли: forall f g h.
f <=< return = f :: c -> m d Right identity
return <=< g = g :: b -> m c Left identity
(f <=< g) <=< h = f <=< (g <=< h) :: a -> m d Associativity
<=< является ассоциативным, а return - его правая и левая идентичность.
Идентичность
Тип личности
type Id t = t
- это функция тождественности для типов
Id :: * -> *
интерпретируется как функтор,
return :: t -> Id t
= id :: t -> t
(=<<) :: (a -> Id b) -> Id a -> Id b
= ($) :: (a -> b) -> a -> b
(<=<) :: (b -> Id c) -> (a -> Id b) -> (a -> Id c)
= (.) :: (b -> c) -> (a -> b) -> (a -> c)
В каноническом Хаскеле тождественная монада определена
newtype Id t = Id t
instance Functor Id where
map :: (a -> b) -> Id a -> Id b
map f (Id x) = Id (f x)
instance Monad Id where
return :: t -> Id t
return = Id
(=<<) :: (a -> Id b) -> Id a -> Id b
f =<< (Id x) = f x
Опция
Тип опции
data Maybe t = Nothing | Just t
кодирует вычисления Maybe t, которые не обязательно дают результат t, вычисления, которые могут «потерпеть неудачу». Опция монада определена
instance Functor Maybe where
map :: (a -> b) -> (Maybe a -> Maybe b)
map f (Just x) = Just (f x)
map _ Nothing = Nothing
instance Monad Maybe where
return :: t -> Maybe t
return = Just
(=<<) :: (a -> Maybe b) -> Maybe a -> Maybe b
f =<< (Just x) = f x
_ =<< Nothing = Nothing
a -> Maybe b применяется к результату, только если Maybe a дает результат.
newtype Nat = Nat Int
Натуральные числа могут быть закодированы как целые числа, большие или равные нулю.
toNat :: Int -> Maybe Nat
toNat i | i >= 0 = Just (Nat i)
| otherwise = Nothing
Натуральные числа не вычитаются при вычитании.
(-?) :: Nat -> Nat -> Maybe Nat
(Nat n) -? (Nat m) = toNat (n - m)
infixl 6 -?
Монада опций охватывает базовую форму обработки исключений.
(-? 20) <=< toNat :: Int -> Maybe Nat
Список
Монада списка, над типом списка
data [] t = [] | t : [t]
infixr 5 :
и его аддитивная моноидная операция «добавление»
(++) :: [t] -> [t] -> [t]
(x : xs) ++ ys = x : xs ++ ys
[] ++ ys = ys
infixr 5 ++
кодирует нелинейное вычисление [t], получая натуральное количество 0, 1, ... результатов t.
instance Functor [] where
map :: (a -> b) -> ([a] -> [b])
map f (x : xs) = f x : map f xs
map _ [] = []
instance Monad [] where
return :: t -> [t]
return = (: [])
(=<<) :: (a -> [b]) -> [a] -> [b]
f =<< (x : xs) = f x ++ (f =<< xs)
_ =<< [] = []
Расширение =<< объединяет ++ все списки [b], полученные в результате применения f x стрелки Клейсли a -> [b] к элементам [a] в единый список результатов [b].
Пусть правильные делители натурального числа n будут
divisors :: Integral t => t -> [t]
divisors n = filter (`divides` n) [2 .. n - 1]
divides :: Integral t => t -> t -> Bool
(`divides` n) = (== 0) . (n `rem`)
тогда
forall n. let { f = f <=< divisors } in f n = []
При определении класса типа монады вместо расширения =<< стандарт Haskell использует свой переворот, оператор bind >>=.
class Applicative m => Monad m where
(>>=) :: forall a b. m a -> (a -> m b) -> m b
(>>) :: forall a b. m a -> m b -> m b
m >> k = m >>= \ _ -> k
{-# INLINE (>>) #-}
return :: a -> m a
return = pure
Для простоты в этом объяснении используется иерархия классов типов
class Functor f
class Functor m => Monad m
В Haskell текущая стандартная иерархия
class Functor f
class Functor p => Applicative p
class Applicative m => Monad m
Бекиспользовать не только каждую монаду - функтор, но каждая аппликативная функция - функтор, и каждая монада также аппликативная.
Использование монады списка, императивного псевдокода
for a in (1, ..., 10)
for b in (1, ..., 10)
p <- a * b
if even(p)
yield p
примерно переводится в блок do ,
do a <- [1 .. 10]
b <- [1 .. 10]
let p = a * b
guard (even p)
return p
эквивалент понимание монады ,
[ p | a <- [1 .. 10], b <- [1 .. 10], let p = a * b, even p ]
и выражение
[1 .. 10] >>= (\ a ->
[1 .. 10] >>= (\ b ->
let p = a * b in
guard (even p) >> -- [ () | even p ] >>
return p
)
)
Обозначения нотации и монады являются синтаксическим сахаром для вложенных выражений связывания. Оператор связывания используется для локального связывания имен монадических результатов.
let x = v in e = (\ x -> e) $ v = v & (\ x -> e)
do { r <- m; c } = (\ r -> c) =<< m = m >>= (\ r -> c)
, где
(&) :: a -> (a -> b) -> b
(&) = flip ($)
infixl 0 &
Функция защиты определена
guard :: Additive m => Bool -> m ()
guard True = return ()
guard False = fail
где тип блока или «пустой кортеж»
data () = ()
Аддитивные монады , поддерживающие выбор и сбой , могут быть абстрагированы с использованием класса типов
class Monad m => Additive m where
fail :: m t
(<|>) :: m t -> m t -> m t
infixl 3 <|>
instance Additive Maybe where
fail = Nothing
Nothing <|> m = m
m <|> _ = m
instance Additive [] where
fail = []
(<|>) = (++)
, где fail и <|> образуют моноид forall k l m.
k <|> fail = k
fail <|> l = l
(k <|> l) <|> m = k <|> (l <|> m)
и fail - поглощающий / аннигилирующий нулевой элемент аддитивных монад
_ =<< fail = fail
Если в
guard (even p) >> return p
even p истинно, тогда охранник выдает [()], и, по определению >>, локальную постоянную функцию
\ _ -> return p
применяется к результату (). Если ложь, то охранник создает список монад fail ([]), который не дает результата для стрелки Клейсли, к которой нужно применить >>, так что этот p пропускается.
Государство
Печально, монады используются для кодирования вычислений с состоянием.
A процессор состояний является функцией
forall st t. st -> (t, st)
, который переходит в состояние st и дает результат t. Состояние st может быть любым. Ничего, флаг, количество, массив, дескриптор, машина, мир.
Тип государственных процессоров обычно называется
type State st t = st -> (t, st)
Монада процессора состояний - это * -> * функтор State st. Клейсли стрелки состояния процессора монады являются функциями
forall st a b. a -> (State st) b
В каноническом Haskell определяется ленивая версия монады процессора состояний
newtype State st t = State { stateProc :: st -> (t, st) }
instance Functor (State st) where
map :: (a -> b) -> ((State st) a -> (State st) b)
map f (State p) = State $ \ s0 -> let (x, s1) = p s0
in (f x, s1)
instance Monad (State st) where
return :: t -> (State st) t
return x = State $ \ s -> (x, s)
(=<<) :: (a -> (State st) b) -> (State st) a -> (State st) b
f =<< (State p) = State $ \ s0 -> let (x, s1) = p s0
in stateProc (f x) s1
Процессор состояния запускается путем предоставления начального состояния:
run :: State st t -> st -> (t, st)
run = stateProc
eval :: State st t -> st -> t
eval = fst . run
exec :: State st t -> st -> st
exec = snd . run
Доступ к состоянию обеспечивается примитивами get и put, методами абстракции над с сохранением состояния монад:
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
class Monad m => Stateful m st | m -> st where
get :: m st
put :: st -> m ()
m -> st объявляет функциональную зависимость типа состояния st от монады m; что State t, например, определит тип состояния как t однозначно.
instance Stateful (State st) st where
get :: State st st
get = State $ \ s -> (s, s)
put :: st -> State st ()
put s = State $ \ _ -> ((), s)
с типом устройства, используемым аналогично void в C.
modify :: Stateful m st => (st -> st) -> m ()
modify f = do
s <- get
put (f s)
gets :: Stateful m st => (st -> t) -> m t
gets f = do
s <- get
return (f s)
gets часто используется со средствами доступа к полям записи.
Монад состояния, эквивалентный переменной threading
let s0 = 34
s1 = (+ 1) s0
n = (* 12) s1
s2 = (+ 7) s1
in (show n, s2)
, где s0 :: Int, - одинаково прозрачный, но бесконечно более элегантный и практичный
.
(flip run) 34
(do
modify (+ 1)
n <- gets (* 12)
modify (+ 7)
return (show n)
)
modify (+ 1) - это вычисление типа State Int (), за исключением его эффекта , эквивалентного return ().
(flip run) 34
(modify (+ 1) >>
gets (* 12) >>= (\ n ->
modify (+ 7) >>
return (show n)
)
)
Закон ассоциативности монад можно записать в терминах >>= forall m f g.
(m >>= f) >>= g = m >>= (\ x -> f x >>= g)
или
do { do { do {
r1 <- do { x <- m; r0 <- m;
r0 <- m; = do { = r1 <- f r0;
f r0 r1 <- f x; g r1
}; g r1 }
g r1 }
} }
Как и в программировании, ориентированном на выражения (например, Rust), последний оператор блока представляет его доходность. Оператор связывания иногда называют «программируемой точкой с запятой».
Примитивы структуры управления итерациями из структурированного императивного программирования эмулируются монадически
for :: Monad m => (a -> m b) -> [a] -> m ()
for f = foldr ((>>) . f) (return ())
while :: Monad m => m Bool -> m t -> m ()
while c m = do
b <- c
if b then m >> while c m
else return ()
forever :: Monad m => m t
forever m = m >> forever m
Вход / выход
data World
Монада процессора состояний мира ввода / вывода - это согласование чистого Хаскелла и реального мира с функциональной денотативной и императивной операционной семантикой. Близкий аналог собственно строгой реализации:
type IO t = World -> (t, World)
Взаимодействию способствуют нечистые примитивы
getChar :: IO Char
putChar :: Char -> IO ()
readFile :: FilePath -> IO String
writeFile :: FilePath -> String -> IO ()
hSetBuffering :: Handle -> BufferMode -> IO ()
hTell :: Handle -> IO Integer
. . . . . .
Примесь кода, использующего примитивы IO, постоянно протоколируется системой типов. Поскольку чистота потрясающая, то, что происходит в IO, остается в IO.
unsafePerformIO :: IO t -> t
Или, по крайней мере, должен.
Подпись типа программы на Haskell
main :: IO ()
main = putStrLn "Hello, World!"
расширяется до
World -> ((), World)
фудеятельность, которая преобразует мир.
Эпилог
Категория, в которой объекты относятся к типам Haskell, а морфизмы являются функциями между типами Haskell, это «быстрая и свободная» категория Hask.
Функтор T - это отображение из категории C в категорию D; для каждого объекта в C объект в D
Tobj : Obj(C) -> Obj(D)
f :: * -> *
и для каждого морфизма в C морфизм в D
Tmor : HomC(X, Y) -> HomD(Tobj(X), Tobj(Y))
map :: (a -> b) -> (f a -> f b)
, где X, Y - объекты в C. HomC(X, Y) является классом гомоморфизмов всех морфизмов X -> Y в C. Функтор должен сохранять индивидуальность и композицию морфизма, «структуру» C, в D.
Tmor Tobj
T(id) = id : T(X) -> T(X) Identity
T(f) . T(g) = T(f . g) : T(X) -> T(Z) Composition
категория Клейсли категории C дается тройкой Клейсли
<T, eta, _*>
эндофунктора
T : C -> C
(f), морфизм тождества eta (return) и оператор расширения * (=<<).
Каждый морфизм Клейсли в Hask
f : X -> T(Y)
f :: a -> m b
оператором расширения
(_)* : Hom(X, T(Y)) -> Hom(T(X), T(Y))
(=<<) :: (a -> m b) -> (m a -> m b)
получает морфизм в категории Hask Клейсли
f* : T(X) -> T(Y)
(f =<<) :: m a -> m b
Композиция в категории Клейсли .T дана в терминах расширения
f .T g = f* . g : X -> T(Z)
f <=< g = (f =<<) . g :: a -> m c
и удовлетворяет аксиомам категории
eta .T g = g : Y -> T(Z) Left identity
return <=< g = g :: b -> m c
f .T eta = f : Z -> T(U) Right identity
f <=< return = f :: c -> m d
(f .T g) .T h = f .T (g .T h) : X -> T(U) Associativity
(f <=< g) <=< h = f <=< (g <=< h) :: a -> m d
который, применяя преобразования эквивалентности
eta .T g = g
eta* . g = g By definition of .T
eta* . g = id . g forall f. id . f = f
eta* = id forall f g h. f . h = g . h ==> f = g
(f .T g) .T h = f .T (g .T h)
(f* . g)* . h = f* . (g* . h) By definition of .T
(f* . g)* . h = f* . g* . h . is associative
(f* . g)* = f* . g* forall f g h. f . h = g . h ==> f = g
в терминах расширения даны канонически
eta* = id : T(X) -> T(X) Left identity
(return =<<) = id :: m t -> m t
f* . eta = f : Z -> T(U) Right identity
(f =<<) . return = f :: c -> m d
(f* . g)* = f* . g* : T(X) -> T(Z) Associativity
(((f =<<) . g) =<<) = (f =<<) . (g =<<) :: m a -> m c
Монады также могут быть определены в терминах не расширения Клейса, а естественного преобразования mu в программировании, называемом join. Монада определяется как mu как тройка над категорией C эндофунктора
T : C -> C
f :: * -> *
и две природные трансформации
eta : Id -> T
return :: t -> f t
mu : T . T -> T
join :: f (f t) -> f t
удовлетворяющих эквивалентности
mu . T(mu) = mu . mu : T . T . T -> T . T Associativity
join . map join = join . join :: f (f (f t)) -> f t
mu . T(eta) = mu . eta = id : T -> T Identity
join . map return = join . return = id :: f t -> f t
Затем определяется класс типа монады
class Functor m => Monad m where
return :: t -> m t
join :: m (m t) -> m t
Каноническая mu реализация опции монады:
instance Monad Maybe where
return = Just
join (Just m) = m
join Nothing = Nothing
Функция concat
concat :: [[a]] -> [a]
concat (x : xs) = x ++ concat xs
concat [] = []
является join монадой списка.
instance Monad [] where
return :: t -> [t]
return = (: [])
(=<<) :: (a -> [b]) -> ([a] -> [b])
(f =<<) = concat . map f
Реализации join можно перевести из формы расширения с использованием эквивалентности
mu = id* : T . T -> T
join = (id =<<) :: m (m t) -> m t
Обратный перевод от mu к форме расширения дается
f* = mu . T(f) : T(X) -> T(Y)
(f =<<) = join . map f :: m a -> m b
Но почему такая абстрактная теория должна быть полезна для программирования?
Ответ прост: как компьютерные ученые, мы оцениваем абстракцию ! Когда мы проектируем интерфейс к программному компоненту, мы хотим , чтобы он раскрыл как можно меньше информации о реализации. Мы хотим иметь возможность заменить реализацию многими альтернативами, многими другими «экземплярами» той же «концепции». Когда мы разрабатываем общий интерфейс для многих программных библиотек, еще более важно, чтобы у выбранного нами интерфейса были различные реализации. Это общность понятия монады, которое мы так высоко ценим, это , потому что теория категорий настолько абстрактна, что ее понятия так полезны для программирования.
Поэтому неудивительно, что обобщение монад, которое мы представляем ниже, также имеет тесную связь с теорией категорий. Но мы подчеркиваем, что наша цель очень практична: не «реализовать теорию категорий», а найти более общий способ структурирования библиотек комбинаторов. Нам просто повезло, что математики уже проделали большую часть работы за нас!
из Обобщая монады в стрелки Джон Хьюз