Разрабатываем детали типа монадированной свободной монады

Ответ 1

Я нашел удовлетворительное решение этой проблемы. Вот краткий взгляд на конечный результат:

addTwo = do
  (x :: Int) <- input
  (y :: Int) <- input 
  output $ show (x + y)

eval (1 ::: 2 ::: HNil) addTwo = ["3"]

Для этого требуется большое количество шагов. Во-первых, нам нужно заметить, что тип данных ActionF сам индексируется. Мы адаптируем FreeIx для создания индексированной монады, используя списки свободных моноидов. Конструктор Free для FreeIx должен будет зафиксировать свидетеля конечности одного из двух его индексов для использования в доказательствах. Мы будем использовать систему из-за András Kovács для написания доказательств о добавлении списков уровня типов, чтобы сделать доказательства как ассоциативности, так и правильной идентичности. Мы описываем индексированные монады так же, как Олег Гренрус. Мы будем использовать расширение RebindbableSyntax для записи выражений для IxMonad, используя обычную нотацию do.

Пролог

В дополнение ко всем расширениям, которые уже требуется вашему примеру, и RebindbableSyntax, которые были упомянуты выше, нам также понадобится UndecidableInstances для тривиальной цели повторного использования определения семейства типов.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RebindableSyntax #-}

Мы будем использовать :~: GADT из Data.Type.Equality для управления равенством типов.

import Data.Type.Equality
import Data.Proxy

Поскольку мы будем перепроверять синтаксис Monad, мы скроем все Monad из импорта Prelude. Расширение RebindableSyntax использует для обозначения do любые функции >>=, >> и fail в области видимости.

import Prelude hiding (Monad, (>>=), (>>), fail, return)

У нас также есть несколько бит нового кода библиотеки общего назначения. Я дал HList конструктор инфикса, :::.

data HList i where
  HNil :: HList '[]
  (:::) :: h -> HList t -> HList (h ': t)

infixr 5 :::

Я переименовал семейство типов Append ++, чтобы отобразить оператор ++ в списках.

type family (++) (a :: [k]) (b :: [k]) :: [k] where
  '[]      ++ l  = l
  (e ': l) ++ l' = e ': l ++ l'

Полезно говорить о ограничениях формы forall i. Functor (f i). Они не существуют в Haskell вне GADT, которые фиксируют ограничения, такие как Dict GADT в ограничениях. Для наших целей достаточно определить версию Functor с дополнительным игнорируемым аргументом.

class Functor1 (f :: k -> * -> *) where
    fmap1 :: (a -> b) -> f i a -> f i b

Индексированный ActionF

ActionF Functor чего-то не хватало, он не смог захватить информацию о типе уровня о требованиях методов. Мы добавим дополнительный тип индекса i, чтобы зафиксировать это. Input требуется один тип, '[a], а Output не требует типов, '[]. Мы будем называть этот новый тип параметра индексом функтора.

data ActionF i next where
   Input :: (a -> next) ->  ActionF '[a] next
   Output :: String -> next -> ActionF '[] next 

Мы напишем экземпляры Functor и Functor1 для ActionF.

instance Functor (ActionF i) where
  fmap f (Input c) = Input (fmap f c)
  fmap f (Output s n) = Output s (f n)

instance Functor1 ActionF where
  fmap1 f = fmap f

FreeIx Reconstructed

Мы сделаем два изменения в FreeIx. Мы изменим, как построены индексы. Конструктор Free будет ссылаться на индекс из базового функтора и выражать FreeIx с индексом, что свободная моноидальная сумма (++) индекса от базового функтора и индекс из обернутого FreeIx, Мы также потребуем, чтобы Free фиксировал свидетеля доказательства того, что индекс базового функтора конечен.

data FreeIx f (i :: [k]) a where
  Return :: a -> FreeIx f '[] a
  Free :: (WitnessList i) => f i (FreeIx f j a) -> FreeIx f (i ++ j) a

Мы можем определить экземпляры Functor и Functor1 для FreeIx.

instance (Functor1 f) => Functor (FreeIx f i) where
  fmap f (Return a) = Return (f a)
  fmap f (Free x) = Free (fmap1 (fmap f) x)

instance (Functor1 f) => Functor1 (FreeIx f) where
  fmap1 f = fmap f

Если мы хотим использовать FreeIx с обычным, неиндексированным функтором, мы можем поднять эти значения на неограниченный проиндексированный функтор IxIdentityT. Это не нужно для ответа.

data IxIdentityT f i a = IxIdentityT {runIxIdentityT :: f a}

instance Functor f => Functor (IxIdentityT f i) where
    fmap f = IxIdentityT . fmap f . runIxIdentityT

instance Functor f => Functor1 (IxIdentityT f) where
    fmap1 f = fmap f

Доказательства

Нам нужно будет доказать два свойства о добавлении списков уровней типов. Чтобы написать liftF, нам нужно будет доказать правильное тождество xs ++ '[] ~ xs. Мы будем называть это доказательство appRightId для добавления правильного идентификатора. Чтобы написать bind, нам нужно доказать ассоциативность xs ++ (yz ++ zs) ~ (xs ++ ys) ++ zs, которую будем называть appAssoc.

Доказательства записываются в виде списка преемников, который по существу является списком прокси, по одному для каждого типа type SList xs ~ HFMap Proxy (HList xs).

data SList (i :: [k]) where
  SNil :: SList '[]
  SSucc :: SList t -> SList (h ': t)

Следующее доказательство ассоциативности наряду с методом написания этого доказательства из-за András Kovács. Используя только SList для списка типов xs, мы деконструируем и используем Proxy для других списков типов, мы можем задерживать (возможно, бесконечно) необходимость WitnessList экземпляров для ys и zs.

appAssoc ::
  SList xs -> Proxy ys -> Proxy zs ->
  (xs ++ (ys ++ zs)) :~: ((xs ++ ys) ++ zs)
appAssoc SNil ys zs = Refl
appAssoc (SSucc xs) ys zs =
  case appAssoc xs ys zs of Refl -> Refl

Refl, конструктор для :~:, может быть создан только тогда, когда компилятор имеет доказательство того, что оба типа равны. Согласование шаблонов на Refl вводит доказательство равенства типа в текущую область.

Мы можем доказать правое тождество аналогичным образом

appRightId :: SList xs -> xs :~: (xs ++ '[])
appRightId SNil = Refl
appRightId (SSucc xs) = case appRightId xs of Refl -> Refl

Чтобы использовать эти доказательства, мы создаем списки свидетелей для класса списков конечного типа.

class WitnessList (xs :: [k]) where
  witness :: SList xs

instance WitnessList '[] where
  witness = SNil

instance WitnessList xs => WitnessList (x ': xs) where
  witness = SSucc witness

Подъемное

Оборудованный appRightId, мы можем определить значения подъема из базового функтора в FreeIx.

liftF :: forall f i a . (WitnessList i, Functor1 f) => f i a -> FreeIx f i a
liftF = case appRightId (witness :: SList i) of Refl -> Free . fmap1 Return

Явный forall для ScopedTypeVariables. Свидетельству о конечности индекса WitnessList i требуется как конструктор Free, так и appRightId. Доказательство appRightId используется, чтобы убедить компилятор, что построенный FreeIx f (i ++ '[]) a имеет тот же тип, что и FreeIx f i a. Этот '[] появился из Return, который был обернут в базовый функтор.

Наши две команды Input и Output записываются в терминах liftF.

type Action i a = FreeIx ActionF i a

input :: Action '[a] a
input = liftF (Input id)

output :: String -> Action '[] ()
output s = liftF (Output s ())

IxMonad и привязка

Чтобы использовать RebindableSyntax, мы определим класс IxMonad с теми же именами функций (>>=), (>>) и fail как Monad, но разными типами. Этот класс описан в ответе Олега Гренруса.

class Functor1 m => IxMonad (m :: k -> * -> *) where
    type Unit :: k
    type Plus (i :: k) (j :: k) :: k

    return :: a -> m Unit a
    (>>=) :: m i a -> (a -> m j b) -> m (Plus i j) b

    (>>) :: m i a -> m j b -> m (Plus i j) b
    a >> b = a >>= const b

    fail :: String -> m i a
    fail s = error s

Реализация bind для FreeIx требует доказательства ассоциативности, appAssoc. Единственный экземпляр WitnessList в области видимости, WitnessList i - это тот, который был захвачен деконструированным конструктором Free. Еще раз, явный forall для ScopedTypeVariables.

bind :: forall f i j a b. (Functor1 f) => FreeIx f i a -> (a -> FreeIx f j b) -> FreeIx f (i ++ j) b
bind (Return a) f = f a
bind (Free (x :: f i1 (FreeIx f j1 a))) f =
    case appAssoc (witness :: SList i1) (Proxy :: Proxy j1) (Proxy :: Proxy j)
    of Refl -> Free (fmap1 (`bind` f) x)

bind является единственной интересной частью экземпляра IxMonad для FreeIx.

instance (Functor1 f) => IxMonad (FreeIx f) where
    type Unit = '[]
    type Plus i j = i ++ j

    return = Return
    (>>=) = bind

Мы закончили

Вся сложная часть выполнена. Мы можем написать простой интерпретатор для Action xs () самым прямым способом. Единственный трюк, который требуется, - избегать сопоставления шаблонов в конструкторе HList :::, пока не будет известен список типов i, поскольку мы уже сопоставлены с Input.

eval :: HList i -> Action i () -> [String]
eval inputs action = 
    case action of 
        Return () -> []
        Free (Input f) -> 
            case inputs of
                (x ::: xs) -> eval xs (f x)
        Free (Output s next) -> s : eval inputs next

Если вам интересно узнать о предполагаемом типе addTwo

addTwo = do
  (x :: Int) <- input
  (y :: Int) <- input 
  output $ show (x + y)

это

> :t addTwo
addTwo :: FreeIx ActionF '[Int, Int] ()

Ответ 2

У меня есть новое решение, которое является простым и общеприменимым.

До сих пор в потоке мы использовали монады, индексированные моноидом, но здесь я полагаюсь на другое популярное понятие индексированной монады, которая имеет типичные переходы (стиль логики Хоар):

    return :: a -> m i i a
    (>>=) :: m i j a -> (a -> m j k b) -> m i k b

Я считаю, что два подхода эквивалентны (по крайней мере теоретически), поскольку мы получаем монаду Хоара путем индексирования с моноидом эндоморфизма, и мы также можем пойти в обратном направлении с помощью CPS, кодирующего моноидальные приложения в состояниях. На практике язык типа Haskell и тип уровня языка довольно слабый, поэтому перемещение назад и вперед между двумя представлениями не является вариантом.

Существует проблема, хотя с указанным выше типом для >>=: это означает, что мы должны вычислить typestate в порядке сверху вниз, i. е. он заставляет следующее определение для IxFree:

data IxFree f i j a where
  Pure :: a -> IxFree f i i a
  Free :: f i j (IxFree f j k a) -> IxFree f i k a

Итак, если у нас есть выражение Free exp, то мы сначала переходим от i до j после конструктора exp, а затем получаем от j до k, проверяя субэксперсии exp. Это означает, что если мы попытаемся скопировать типы input в список, мы получим обратный список:

-- compute transitions top-down
test = do
  (x :: Int) <- input       -- prepend Int to typestate
  (y :: String) <- input    -- prepend String to typestate
  return ()                 -- do nothing         

Если мы добавим типы в конец списка, порядок будет правильным. Но для того, чтобы эта работа в Haskell (особенно для работы eval) потребовала бы изнурительного количества написания доказательств, если это вообще возможно.

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

{-# LANGUAGE
    RebindableSyntax, DataKinds,
    GADTs, TypeFamilies, TypeOperators,
    PolyKinds, StandaloneDeriving, DeriveFunctor #-}

import Prelude hiding (Monad(..))

class IxFunctor (f :: ix -> ix -> * -> *) where
    imap :: (a -> b) -> f i j a -> f i j b

class IxFunctor m => IxMonad (m :: ix -> ix -> * -> *) where
    return :: a -> m i i a
    (>>=) :: m j k a -> (a -> m i j b) -> m i k b -- note the change of index orders

    (>>) :: m j k a -> m i j b -> m i k b -- here too
    a >> b = a >>= const b

    fail :: String -> m i j a
    fail = error

data IxFree f i j a where
  Pure :: a -> IxFree f i i a
  Free :: f j k (IxFree f i j a) -> IxFree f i k a -- compute bottom-up

instance IxFunctor f => Functor (IxFree f i j) where
  fmap f (Pure a)  = Pure (f a)
  fmap f (Free fa) = Free (imap (fmap f) fa)

instance IxFunctor f => IxFunctor (IxFree f) where
  imap = fmap

instance IxFunctor f => IxMonad (IxFree f) where
  return = Pure
  Pure a  >>= f = f a
  Free fa >>= f = Free (imap (>>= f) fa)

liftf :: IxFunctor f => f i j a -> IxFree f i j a
liftf = Free . imap Pure

Теперь реализация Action становится простой.

data ActionF i j next where
  Input  :: (a -> next) -> ActionF i (a ': i) next
  Output :: String -> next -> ActionF i i next

deriving instance Functor (ActionF i j)                                      
instance IxFunctor ActionF where
  imap = fmap

type family (++) xs ys where -- I use (++) here only for the type synonyms
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

type Action' xs rest = IxFree ActionF rest (xs ++ rest)
type Action xs a = forall rest. IxFree ActionF rest (xs ++ rest) a  

input :: Action '[a] a
input = liftf (Input id)

output :: String -> Action '[] ()
output s = liftf (Output s ())

data HList i where
  HNil :: HList '[]
  (:::) :: h -> HList t -> HList (h ': t)
infixr 5 :::

eval :: Action' xs r a -> HList xs -> [String]
eval (Pure a)              xs         = []
eval (Free (Input k))      (x ::: xs) = eval (k x) xs
eval (Free (Output s nxt)) xs         = s : eval nxt xs

addTwice :: Action [Int, Int] ()
addTwice = do
  x <- input
  y <- input
  output (show $ x + y)

Чтобы сделать вещи менее запутанными для пользователей, я ввел синонимы типов с более дружественными схемами индексов: Action' xs rest a означает, что действие читается из xs, и за ним могут следовать действия, содержащие rest. Action - это синоним типа, эквивалентный тому, который появляется в вопросе нити.

Мы можем реализовать различные DSL-ы с этим подходом. Обратный порядок ввода дает немного вращения, но мы можем делать обычные индексированные монады все равно. Здесь монада с индексированным состоянием, например:

data IxStateF i j next where
  Put :: j -> next -> IxStateF j i next
  Get :: (i -> next) -> IxStateF i i next

deriving instance Functor (IxStateF i j)
instance IxFunctor IxStateF where imap = fmap

put s = liftf (Put s ())
get   = liftf (Get id)

type IxState i j = IxFree IxStateF j i

evalState :: IxState i o a -> i -> (a, o)
evalState (Pure a)         i = (a, i)
evalState (Free (Get k))   i = evalState (k i) i
evalState (Free (Put s k)) i = evalState k s

test :: IxState Int String ()
test = do
  n <- get
  put (show $ n * 100)

Теперь я считаю, что этот подход является более практичным, чем индексирование с моноидами, потому что у Haskell нет классных классов или функций класса первого класса, которые сделали бы моноидный подход приемлемым. Было бы неплохо иметь класс VerifiedMonoid, например, в Idris или Agda, который включает доказательства корректности, помимо обычных методов. Таким образом, мы могли бы написать FreeIx, который является общим в выборе моноида индекса, и не ограничивается отмененными списками или чем-то еще.

Ответ 3

В скором времени об индексированных монадах: они являются монадами, индексированными моноидами. Для сравнения monad:

class Monad m where
  return :: a -> m a
  bind :: m a -> (a -> m b) -> m b
  -- or `bind` alternatives:
  fmap :: (a -> b) -> m a -> m b
  join :: m (m a) -> m a

Моноид - это тип, оснащенный mempty - идентификационным элементом, и (<>) :: a -> a -> a двоичная ассоциативная операция. На уровне уровня мы могли бы иметь тип Unit и Plus ассоциативный двоичный тип операции. Обратите внимание: список представляет собой свободный моноид на уровне значения, а HList - на уровне типа.

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

class IxMonad m where
  type Unit
  type Plus i j

  return :: a -> m Unit a
  bind :: m i a -> (a -> m j b) -> m (Plus i j) b
  --
  fmap :: (a -> b) -> m i a -> m i b
  join :: m i (m j a) -> m (Plus i j) a

Вы можете указать законы монады для индексированной версии. Вы заметите, что для выравнивания индексов они должны подчиняться моноидным законам.

С помощью бесплатной монады вы хотите оснастить Functor операциями return и join. Немного изменив ваше определение:

data FreeIx f i a where
  Return :: a -> FreeIx f '[] a -- monoid laws imply we should have `[] as index here!
  Free :: f (FreeIx f k a) -> FreeIx f k a

bind :: Functor f => FreeIx f i a -> (a -> FreeIx f j b) -> FreeIx f (Append i j) b
bind (Return a) f = f a
bind (Free x) f   = Free (fmap (flip bind f) x)

Я должен признать, что я не уверен на 100%, как индексы конструктора Free оправданы, но они, похоже, работают. Если мы рассмотрим функцию wrap :: f (m a) -> m a класса MonadFree с законом:

wrap (fmap f x) ≡ wrap (fmap return x) >>= f

и комментарий о Free в Free пакете

На практике вы можете просто просмотреть Free f a столько слоев f, которые обернуты вокруг значений типа a, где (>>=) выполняет подстановку и трансплантирует новые слои f для каждого из свободных переменных.

тогда идея состоит в том, что значения упаковки не влияют на индекс.

Тем не менее, вы хотите поднять любое значение f на произвольное индексированное монадическое значение. Это очень разумное требование. Но единственное действительное значение определения заставляет поднятое значение иметь индекс '[] - Unit или mempty:

liftF :: Functor f => f a -> FreeIx f '[] a
liftF = Free . fmap Return

Если вы попытаетесь изменить определение return на :: a -> FreeIx f k a (k, а не [] - чистое значение может иметь произвольный индекс), то определение bind не будет вводить проверку.

Я не уверен, что вы можете сделать бесплатную индексированную монаду только с небольшими исправлениями. Одна идея - поднять произвольную монаду в индексированную монаду:

data FreeIx m i a where
  FreeIx :: m a -> FreeIx m k a

liftF :: Proxy i -> f a -> FreeIx f i a
liftF _ = FreeIx

returnIx :: Monad m => a -> FreeIx m i a
returnIx = FreeIx . return

bind :: Monad m => FreeIx m i a -> (a -> FreeIx m j b) -> FreeIx m (Append i j) b
bind (FreeIx x) f = FreeIx $ x >>= (\x' -> case f x' of
                                             FreeIx y -> y)

Этот подход немного похож на обман, так как мы всегда можем переопределить значение.

Другой подход - напомнить Functor его индексированный функтор или сразу начать с индексированного функтора, как в ответе Cirdec.

Ответ 4

Если вы готовы пожертвовать неявным порядком и использовать явные аксессоры, ваш Action '[Int, Int] может быть реализован с помощью ReaderT (HList '[Int, Int]). Если вы используете существующую библиотеку типа vinyl, которая предоставляет объективы, вы можете написать что-то вроде этого:

-- Implemented with pseudo-vinyl
-- X and Y are Int fields, with accessors xField and yField
addTwo :: ReaderT (PlainRec '[X, Y]) Output ()
addTwo = do
  x <- view (rGet xField)
  y <- view (rGet yField)
  lift . output $ show (x + y) -- output :: String -> Output ()

Безопасность типа обеспечивается принудительным распространением: rGet xField вводит требование, чтобы X был членом записи.

Для более простой иллюстрации без машин типового уровня сравните:

addTwo :: ReaderT (Int, Int) IO ()
addTwo = do
  x <- view _1
  y <- view _2
  lift . putStrLn $ show (x + y)

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

Кроме того, теперь мы должны использовать runReaderT (~ eval). Мы не можем, скажем, чередовать ввод пользователя с выходом.

Ответ 5

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

Мое решение делает то, о чем попросил OP (хотя он включает ручную запись экземпляра монады, поэтому есть место для уточнения).

Пакет effect-monad (который упоминается в OP) уже содержит эффект, который обрабатывает чтение из HList. Он называется ReadOnceReader. Однако для Output нам также нужен эффект Writer, и мне кажется, что библиотека не позволяет нам объединить эти два.

Мы все еще можем взять идею ReadOnceReader и вручную написать AST для желаемого языка. Конечно, AST должен быть проиндексированной монадой. Это было бы аккуратно, если бы мы могли сделать это через индексированную свободную монаду или оперативную монаду. До сих пор у меня не было успеха со свободными монадами. Я мог бы обновить свой ответ после того, как посмотрел на операционные монады.

Отборочный:

{-# LANGUAGE
    RebindableSyntax, DataKinds, ScopedTypeVariables,
    GADTs, TypeFamilies, TypeOperators,
    PolyKinds, StandaloneDeriving, DeriveFunctor #-}

import Prelude hiding (Monad(..))

data HList (xs :: [*]) where
  Nil  :: HList '[]
  (:>) :: x -> HList xs -> HList (x ': xs)
infixr 5 :>                     

type family (++) (xs :: [*]) (ys :: [*]) where
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

Индексированные монады должны обеспечивать способ объединения (Plus) индексов с идентификатором (Unit). Короче говоря, индексы должны быть моноидами.

class IxMonad (m :: k -> * -> *) where
  type Unit m :: k
  type Plus m (i :: k) (j :: k) :: k
  return :: a -> m (Unit m) a
  (>>=)  :: m i a -> (a -> m j b) -> m (Plus m i j) b
  fail   :: m i a

Здесь интересен тип Input: мы добавляем тип ввода к полученному индексу следующего вычисления:

data Action i a where
  Return :: a -> Action '[] a
  Input  :: (x -> Action xs a) -> Action (x ': xs) a
  Output :: String -> Action i a -> Action i a
deriving instance Functor (Action i)

Экземпляр IxMonad и интеллектуальные конструкторы полностью стандартные, а функция eval также реализована прямо.

instance IxMonad Action where
  type Unit Action = '[]
  type Plus Action i j = i ++ j
  return = Return
  Return a     >>= f = f a
  Input k      >>= f = Input ((>>= f) . k)
  Output s nxt >>= f = Output s (nxt >>= f)
  fail = undefined

input :: Action '[a] a
input = Input Return

output :: String -> Action '[] ()
output s = Output s (Return ())

eval :: Action xs a -> HList xs -> [String]
eval (Return a)     xs        = []
eval (Input k)      (x :> xs) = eval (k x) xs
eval (Output s nxt) xs        = s : eval nxt xs

Теперь все работает по желанию:

concat' :: Action '[String, String] ()
concat' = do
  (x :: String) <- input
  (y :: String) <- input 
  output $ x ++ " " ++ y

main = print $ eval concat' ("a" :> "b" :> Nil)
-- prints ["a b"]

Ответ 6

У меня есть рабочая реализация индексированной свободной монады на github за несколько лет назад:

https://github.com/ekmett/indexed/blob/master/src/Indexed/Monad/Free.hs

Он использует форму индексированной монады, предложенную Конором Макбрайдом в Kleisli Arrows of Outrageous Fortune, и которая может быть адаптирована для обеспечения 2- в монашеской монаде в стиле Боба Атки, как описано в статье.