On Vox: Ограниченное - часть 1

Некоторое время тому назад уважаемый hsenag описал способ превратить так называемую "ограниченную монаду" (restricted monad) в настоящую. Я в комментах там описал способ попроще и поэлегантнее; позднее я его расширил и теперь представляю интересующимся.

Что такое, собственно, ограниченная монада? Это то же самое, что и обычная монада, но имеющая смысл только тогда, когда тип, который она содержит, относится к некоторому классу. Характерный пример - множество, "Set". Мы не можем образовать "Set a", если "a" не относится к классу "Ord". В то же время, "Set" не так уж сильно отличается от "[]", и можно ожидать, что стандартный "do"-синтаксис окажется полезным и здесь. Однако, из-за указанного ограничения, превратить "Set" в монаду нельзя.

То, что я сказал, можно превратить в описание класса "OrdMonad" и его инстанса для "Set":

> module OrdMonadSet where
> import qualified Data.Set as Set

> class OrdMonad m where
>     ordReturn :: Ord a => a -> m a
>     ordBind :: (Ord a, Ord b) => m a -> (a -> m b) -> m b

> instance OrdMonad Set.Set where
>     ordReturn = Set.singleton
>     s `ordBind` f = Set.fold (\v ret -> f v `Set.union` ret) Set.empty s

Далее, в соответствии с тем, что сделано для монады "[]", можно также объявить аналог "MonadPlus":

> class OrdMonad m => OrdMonadPlus m where
>     ordMZero :: Ord a => m a
>     ordMPlus :: Ord a => m a -> m a -> m a

> instance OrdMonadPlus Set.Set where
>     ordMZero = Set.empty
>     ordMPlus = Set.union

В дальнейшем нам пригодится аналог функции "msum":

> ordMSum :: (OrdMonadPlus m, Ord a) => [m a] -> m a

> ordMSum = foldr ordMPlus ordMZero

Как же заставить "do"-синтаксис работать с такими "ограниченными монадами"? Ну, один из вариантов - использовать Template Haskell и руками преобразовать do-нотацию в выражение с "ordReturn" и "ordBind". Однако, использовать TH - значит признать своё поражение; мы поищем другой способ.

Один из способов сделать это внутри хаскеля описан в посте, на который выше стоит ссылка. Желающие могут посмотреть, как это сделано; я же изложу собственный вариант.

Для начала нам потребуются GADT-ы (без них, увы, никуда, разве что existential types вспомнить, а это то же самое).

> {-# LANGUAGE GADTs #-}
> module Rest1 where
> import Control.Monad
> import qualified Data.Set as Set
> import OrdMonadSet

Последний импорт - это импорт того модуля, который приведён выше; он содержит, в частности, класс "OrdMonad".

Тип данных, который мы будем использовать, содержит, собственно, два конструктора - аналоги >>= и return. Однако, поскольку цепочка >>= будет всегда начинаться с чего-то, относящегося к классу "Ord", мы можем ограничить один из типов:

> data OrdM m a where
>     ReturnOrdM :: a -> OrdM m a
>     BindOrdM :: Ord a => m a -> (a -> OrdM m b) -> OrdM m b

Теперь несложно объявить этот тип монадой. При этом мы будем использовать монадические законы - например, то, что "return x >>= f = f x". Именно эти законы предопределяют определение ">>=" для нашего типа "OrdM".

> instance Monad (OrdM m) where
>     return = ReturnOrdM
>     ReturnOrdM x >>= f = f x
>     BindOrdM mx g >>= f = BindOrdM mx $ \x -> g x >>= f

Далее, нужно найти способ перегнать нашу "ограниченную монаду" в настоящую:

> embed :: Ord a => m a -> OrdM m a
> embed mx = BindOrdM mx return

и обратно:

> unembed :: (OrdMonad m, Ord a) => OrdM m a -> m a
> unembed (ReturnOrdM x) = ordReturn x
> unembed (BindOrdM mx g) = mx `ordBind` (unembed . g)

Уже неплохо. Однако, нам нужно работать ещё и с "OrdMonadPlus". Увы, даже если есть инстанс "OrdMonadPlus" для "m", превратить "OrdM m" в инстанс "MonadPlus" не удаётся.

Решение по ссылке выше - добавить в "OrdM" парочку конструкторов, скажем, "OrdMZero" и "OrdMPlus". Мне это решение не нравится, так как не учитывает законы, связанные с "mzero" и "mplus" - например, ассоциативность. Вместо этого я буду просто хранить список, элементы которого - по сути те же, что и раньше. "mzero" превратится в пустой список, а "mplus" - в конкатенацию.

> data OrdPlusData m a where
>     ReturnOrdPlus :: a -> OrdPlusData m a
>     BindOrdPlus :: Ord a => m a -> (a -> OrdP m b) -> OrdPlusData m b

> newtype OrdP m a = OrdP {fromOrdP :: [OrdPlusData m a]}

Для "OrdP" я объявлю - по сути, точно так же - инстанс класса "Monad":

> instance Monad (OrdP m) where
>     return x = OrdP [ReturnOrdPlus x]
>     OrdP omxs >>= f = OrdP $ omxs >>= handleOmx
>         where handleOmx (ReturnOrdPlus x) = fromOrdP $ f x
>               handleOmx (BindOrdPlus mx g) = [BindOrdPlus mx $ \x -> g x >>= f]

Правда, разбор случаев пришлось упаковать во вспомогательную функцию "handleOmx"; заметьте, что в выражении ">>= handleOmx" оператор ">>=" - это ">>=" для монады-списка, то есть, по сути, "concatMap".

Теперь можно определить и инстанс "MonadPlus":

> instance MonadPlus (OrdP m) where
>     mzero = OrdP []
>     OrdP omxs1 `mplus` OrdP omxs2 = OrdP $ omxs1 ++ omxs2

Наконец, нам понадобятся варианты функций "embed" и "unembed" для "OrdP":

> embedPlus :: Ord a => m a -> OrdP m a
> embedPlus mx = OrdP [BindOrdPlus mx return]

> unembedPlus :: (OrdMonadPlus m, Ord a) => OrdP m a -> m a
> unembedPlus (OrdP omxs) = ordMSum $ map handleOmx omxs
>     where handleOmx (ReturnOrdPlus x) = ordReturn x
>           handleOmx (BindOrdPlus mx g) = mx `ordBind` (unembedPlus . g)

Это те же определения, что и для "OrdM", только опять-таки разбор случаев запихнут в ">>= handleOmx"

Теперь можно писать такие, например, вещи:

> test = unembedPlus $ do x <- embedPlus $ Set.fromList [6, 2, 3]
>                         (do y <- return x
>                             z <- embedPlus $ Set.fromList [1..2]
>                             guard $ y < 5
>                             return $ y + z)
>                         `mplus` return 10

Запускаем, получаем:

*Rest1> test
fromList [3,4,5,10]

Originally posted on migmit.vox.com

On Vox: Ограниченное - часть 2

В предыдущем решении один и тот же, по существу, код повторялся дважды. Это не есть хорошо. Вполне можно написать то же самое ОДИН раз, используя "Identity" в первом случае и "[]" во втором. Ну и, интуиция подсказывает, что нужно использовать тот факт, что и то, и другое является монадой.

Нам понадобится чуть больший список импортов:

> {-# LANGUAGE GADTs #-}
> module Rest2 where
> import Control.Monad
> import Control.Monad.Identity
> import Control.Monad.List
> import Control.Monad.Trans
> import qualified Data.Set as Set
> import OrdMonadSet

Тип данных мы определим так же, как и "OrdP" ранее, только вместо "[]" у нас будет произвольное "n".

> data OrdTData m n a where
>     OrdReturn :: a -> OrdTData m n a
>     OrdBind :: Ord a => m a -> (a -> OrdT m n b) -> OrdTData m n b
> newtype OrdT m n a = OrdT {fromOrdT :: n (OrdTData m n a)}

Снова так же определяется инстанс "Monad".

> instance Monad n => Monad (OrdT m n) where
>     return = OrdT . return . OrdReturn
>     OrdT nomnx >>= f = OrdT $ nomnx >>= handleOmnx
>       where handleOmnx (OrdReturn x) = fromOrdT $ f x
>             handleOmnx (OrdBind mu g) = return $ OrdBind mu $ \x -> g x >>= f

Теперь, "OrdT m n" является монадой, если "n" является монадой. То есть, "OrdT m" - это такой преобразователь монад. Трансформер, иначе говоря. Для полноты картины можно объявить и инстанс "MonadTrans".

> instance MonadTrans (OrdT m) where lift nx = OrdT $ liftM OrdReturn nx

Я не знаю, зачем это может понадобиться, но пусть уж будет, хотя бы для красоты.

Функция "embed" выглядит как и раньше, а вот "unembed" - не совсем. В предыдущем посте "unembed" и "unembedPlus" различались - в unembedPlus участвовала функция "ordMSum". Поскольку её аналог для произвольного "n" заранее неизвестен, придётся передавать её в "unembed" как параметр.

> embed mx = OrdT $ return $ OrdBind mx return
> unembed f = unembed'
>     where unembed' (OrdT nomnx) = f $ liftM handleOmnx nomnx
>           handleOmnx (OrdReturn x) = ordReturn x
>           handleOmnx (OrdBind mu g) = ordBind mu $ unembed' . g

Ну, теперь несложно воспроизвести старый "OrdM":

> type OrdM m a = OrdT m Identity a
> unembedId :: (OrdMonad m, Ord a) => OrdM m a -> m a
> unembedId = unembed $ runIdentity

Далее, если "n" - не просто монада, но инстанс "MonadPlus" (как, скажем, "[]"), то "OrdT m n" - тоже инстанс "MonadPlus"; кроме того, если "m" - инстанс "OrdMonadPlus", то можно воспроизвести старое "unembedPlus":

> instance MonadPlus n => MonadPlus (OrdT m n) where
>     mzero = OrdT mzero
>     OrdT nomnx1 `mplus` OrdT nomnx2 = OrdT $ nomnx1 `mplus` nomnx2
> unembedPlus :: (OrdMonadPlus m, Ord a) => OrdT m [] a -> m a
> unembedPlus = unembed $ foldr ordMPlus ordMZero

Наш пример теперь выглядит так:

> test = unembedPlus $ do x <- embed $ Set.fromList [6, 2, 3]
>                         (do y <- return x
>                             z <- embed $ Set.fromList [1..2]
>                             guard $ y < 5
>                             return $ y + z)
>                         `mplus` return 10

Originally posted on migmit.vox.com

On Vox: Ограниченное - часть 3

Всё изложенное ранее - очень хорошо, но относится к одному единственному классу - "Ord". Увы, мы не можем сделать класс параметром чего бы то ни было - тип можем, а вот класс - нет. Однако в Haskell-Café пробежало решение и этой проблемы.

Для этого решения требуются type families. Я вынесу в отдельный модуль как общий код, так и то, что нужно написать для "Set":

> {-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}
> module Suitable where

Прагм многовато, но, за исключением первой, GHC подсказывает все остальные.

Мы используем "Set" для примера, так что импортируем соответствующий модуль:

> import qualified Data.Set as Set

Суть дела - в следующем классе; функция "constraints" не использует свой аргумент, ей нужен только его тип; все необходимые ограничения на тип "a" содержатся в типе "Constraints m a" - позднее мы увидим, как именно они задаются.

> class Suitable m a where
>     data Constraints m a :: *
>     constraints :: m a -> Constraints m a

Теперь можно ввести собственно "ограниченную монаду"

> class RestrMonad m where
>     restrReturn :: Suitable m a => a -> m a
>     restrBind :: (Suitable m a, Suitable m b) => m a -> (a -> m b) -> m b

и ограниченный вариант "MonadPlus":

> class RestrMonad m => RestrPlus m where
>     restrMZero :: Suitable m a => m a
>     restrMPlus :: Suitable m a => m a -> m a -> m a

Как и раньше, нам пригодится аналог функции "msum":

> restrMSum :: (RestrPlus m, Suitable m a) => [m a] -> m a
> restrMSum = foldr restrMPlus restrMZero

Теперь посмотрим, как это всё работает для "Set". Для начала - класс "Suitable".

> instance Ord a => Suitable Set.Set a where
>     data Constraints Set.Set a = Ord a => SetConstraints
>     constraints _ = SetConstraints

Как видим, и класс "Suitable" и тип "Constraints" определены лишь тогда, когда "a" относится к классу "Ord". Это и есть то ограничение, которое нам нужно. Функция "constraints" позволяет нам проверять это ограничение, как, например, в определении инстанса "RestrMonad"

> instance RestrMonad Set.Set where
>     restrReturn = Set.singleton
>     restrBind sx f = let result = case constraints result of SetConstraints -> Set.unions $ map f $ Set.toList sx in result

или инстанса "RestrPlus".

> instance RestrPlus Set.Set where
>     restrMZero = Set.empty
>     restrMPlus sx1 sx2 = case constraints sx1 of SetConstraints -> Set.union sx1 sx2

Теперь основной модуль выглядит ровно так же, как и раньше, только функции, начинающиеся на "ord" заменяются функциями, начинающимися на "restr".
> {-# LANGUAGE GADTs #-}
> module Restricted where
> import Control.Monad
> import Control.Monad.Identity
> import Control.Monad.List
> import Control.Monad.Trans
> import qualified Data.Set as Set
> import Suitable
>
> data RestrTData m n a where
>     RestrRet :: a -> RestrTData m n a
>     RestrBind :: Suitable m a => m a -> (a -> RestrT m n b) -> RestrTData m n b
> newtype RestrT m n a = RestrT {fromRestrT :: n (RestrTData m n a)}
> instance Monad n => Monad (RestrT m n) where
>     return = RestrT . return . RestrRet
>     RestrT nrmnx >>= f = RestrT $ nrmnx >>= handleRmnx
>         where handleRmnx (RestrRet x) = fromRestrT $ f x
>               handleRmnx (RestrBind mu g) = return $ RestrBind mu $ \x -> g x >>= f
> instance MonadTrans (RestrT m) where lift nx = RestrT $ liftM RestrRet nx
> embed mx = RestrT $ return $ RestrBind mx return
> unembed f = unembed'
>     where unembed' (RestrT nrmnx) = f $ liftM handleRmnx nrmnx
>           handleRmnx (RestrRet x) = restrReturn x
>           handleRmnx (RestrBind mu g) = restrBind mu $ unembed' . g
> instance MonadPlus n => MonadPlus (RestrT m n) where
>     mzero = RestrT mzero
>     RestrT nrmnx1 `mplus` RestrT nrmnx2 = RestrT $ nrmnx1 `mplus` nrmnx2
> type RestrM m a = RestrT m Identity a
> unembedId :: (RestrMonad m, Suitable m a) => RestrM m a -> m a
> unembedId = unembed runIdentity
> unembedPlus :: (RestrPlus m, Suitable m a) => RestrT m [] a -> m a
> unembedPlus = unembed restrMSum
Пример тоже выглядит в точности как раньше:

> test = unembedPlus $ do x <- embed $ Set.fromList [6, 2, 3]
>                         (do y <- return x
>                             z <- embed $ Set.fromList [1..2]
>                             guard $ y < 5
>                             return $ y + z)
>                         `mplus` return 10
Вот и всё.
 

Originally posted on migmit.vox.com