Можно ли выполнить "ST" -подобную монаду (без библиотеки `ST`)?

Ответ 1

tl; dr: Это невозможно без поправок к определению PT. Здесь основная проблема: вы будете запускать вычисления с учетом состояния в контексте какого-либо носителя данных, но указанный носитель информации должен знать, как хранить произвольные типы. Это невозможно без упаковки каких-либо доказательств в конструктор MkRef - либо экзистенциально обернутый словарь Typeable, как предлагали другие, либо доказательство того, что это значение принадлежит одному из известных конечных наборов типов.

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

newtype Ix a = MkIx Int  -- the index of an element in a list

interp :: PT Ix a -> State [b] a
interp (MkRef x) = modify (++ [x]) >> gets (Ref . MkIx . length)
-- ...

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

Это неправильно. Я могу сделать ссылку на любой тип a, но тип interp говорит, что носитель данных является однородным списком b s. GHC имеет права на права, когда он отклоняет подпись этого типа, жалуясь, что он не может соответствовать b с типом вещи внутри MkRef.

Неперемещаемый, давайте перейдем к использованию гетерогенного списка в качестве среды для монады State, в которой мы будем интерпретировать PT.

infixr 4 :>
data Tuple as where
    E :: Tuple '[]
    (:>) :: a -> Tuple as -> Tuple (a ': as)

Это один из моих личных любимых типов данных Haskell. Это расширяемый кортеж, индексированный списком типов вещей внутри него. Кортежи - это разнородные связанные списки с информацией типа типа о типах вещей внутри него. (Он часто назывался HList после Киселевской бумаги, но я предпочитаю Tuple.) Когда вы добавляете что-то к передней части кортежа, вы добавьте его тип в начало списка типов. В поэтическом настроении Я когда-то так выразился: "Кортеж и его тип растут вместе, как виноградная лоза, ползающая бамбуковым растением."

Примеры Tuple s:

ghci> :t 'x' :> E
'x' :> E :: Tuple '[Char]
ghci> :t "hello" :> True :> E
"hello" :> True :> E :: Tuple '[[Char], Bool]

Как выглядят ссылки на значения внутри кортежей? Мы должны доказать GHC, что тип вещи, которую мы получаем из кортежа, действительно тот тип, которого мы ожидаем.

data Elem as a where  -- order of indices arranged for convenient partial application
    Here :: Elem (a ': as) a
    There :: Elem as a -> Elem (b ': as) a

Определение Elem структурно отличается от натуральных чисел (Elem, таких как There (There Here), похоже на натуральные числа, такие как S (S Z)), но с дополнительными типами - в этом случае, доказывая, что тип a находится в списке типов as. Я упоминаю это, потому что это наводит на мысль: Nat сделать хорошие индексы списка, а также Elem полезно для индексирования в кортеж. В этом отношении это будет полезно для замены Int внутри нашего ссылочного типа.

(!) :: Tuple as -> Elem as a -> a
(x :> xs) ! Here = x
(x :> xs) ! (There ix) = xs ! ix

Нам нужна пара функций для работы с кортежами и индексами.

type family as :++: bs where
    '[] :++: bs = bs
    (a ': as) :++: bs = a ': (as :++: bs)

appendT :: a -> Tuple as -> (Tuple (as :++: '[a]), Elem (as :++: '[a]) a)
appendT x E = (x :> E, Here)
appendT x (y :> ys) = let (t, ix) = appendT x ys
                      in (y :> t, There ix)

Попробуйте написать и написать интерпретатор для PT в среде Tuple.

interp :: PT (Elem as) a -> State (Tuple as) a
interp (MkRef x) = do
    t <- get
    let (newT, el) = appendT x t
    put newT
    return el
-- ...

Нет, может, бэттер. Проблема в том, что тип Tuple в среде изменяется, когда мы получаем новую ссылку. Как я уже упоминал ранее, добавление чего-то в кортеж добавляет его тип к типу кортежа, что противоречит типу State (Tuple as) a. GHC не обманывается этой попыткой уловки: Could not deduce (as ~ (as :++: '[a1])).

Вот как колеблются колеса, насколько я могу судить. То, что вы действительно хотите сделать, это сохранить размер константы tuple во всех вычислениях PT. Это потребовало бы, чтобы вы индексировали PT сам по списку типов, к которым вы можете получить ссылки, доказывая каждый раз, когда вы делаете так, чтобы вам разрешалось (путем предоставления значения Elem). Тогда среда будет выглядеть как кортеж списков, а ссылка будет состоять из Elem (для выбора правильного списка) и Int (чтобы найти конкретный элемент в списке).

Этот план, разумеется, нарушает правила (вам нужно изменить определение PT), но также имеет технические проблемы. Когда я звоню MkRef, бремя на меня, чтобы дать Elem для значения, на которое я ссылаюсь, что довольно утомительно. (Тем не менее, вы обычно можете убедить GHC найти значения Elem путем поиска доказательств с использованием класса хакерского типа.)

Другое дело: сочинение PT становится сложным. Все части вашего расчета должны быть проиндексированы одним и тем же списком типов. Вы можете попытаться ввести комбинаторы или классы, которые позволят вам вырастить среду PT, но вам также придется обновлять все ссылки, когда вы это делаете. Использование монады было бы довольно сложно.

Возможно, более чистая реализация позволит изменять список типов в PT при обходе типа данных: каждый раз, когда вы сталкиваетесь с MkRef, тип получает больше. Поскольку тип вычисления изменяется по мере его продвижения, вы не можете использовать обычную монаду - вам нужно прибегнуть к IxMonad. Если вы хотите узнать, как выглядит эта программа, см. Мой другой ответ.

В конечном счете, точка приклеивания состоит в том, что тип кортежа определяется значением запроса PT. Окружающая среда - это то, что данный запрос решает сохранить в нем. interp не может выбрать, что в кортеже, он должен исходить из индекса на PT. Любая попытка обмануть это требование будет разрушаться и гореть. Теперь, в настоящей системе с надписью с надписью, мы могли бы изучить значение PT, которое нам было дано, и выяснить, что должно быть as. Увы, Haskell не является строго типизированной системой.

Ответ 2

Простое решение - обернуть монаду State и представить тот же API, что и ST. В этом случае нет необходимости хранить информацию типа времени выполнения, поскольку ее можно определить по типу STRef -s, а обычный трюк квантификации ST s позволяет нам помешать пользователям помешать контейнеру, хранящему ссылки.

Мы сохраняем ref-s в IntMap и увеличиваем счетчик каждый раз, когда мы выделяем новый ref. Чтение и запись просто изменяет IntMap с помощью unsafeCoerce.

{-# LANGUAGE DeriveFunctor, GeneralizedNewtypeDeriving, RankNTypes, RoleAnnotations #-}

module PureST (ST, STRef, newSTRef, readSTRef, modifySTRef, runST) where

import Data.IntMap (IntMap, (!))
import qualified Data.IntMap as M

import Control.Monad
import Control.Applicative
import Control.Monad.Trans.State
import GHC.Prim (Any)
import Unsafe.Coerce (unsafeCoerce)

type role ST nominal representational
type role STRef nominal representational
newtype ST s a = ST (State (IntMap Any, Int) a) deriving (Functor, Applicative, Monad)
newtype STRef s a = STRef Int deriving Show

newSTRef :: a -> ST s (STRef s a)
newSTRef a = ST $ do
  (m, i) <- get
  put (M.insert i (unsafeCoerce a) m, i + 1)
  pure (STRef i)

readSTRef :: STRef s a -> ST s a
readSTRef (STRef i) = ST $ do
  (m, _) <- get
  pure (unsafeCoerce (m ! i))

writeSTRef :: STRef s a -> a -> ST s ()
writeSTRef (STRef i) a = ST $ 
  modify $ \(m, i') -> (M.insert i (unsafeCoerce a) m, i')

modifySTRef :: STRef s a -> (a -> a) -> ST s ()
modifySTRef (STRef i) f = ST $
  modify $ \(m, i') -> (M.adjust (unsafeCoerce f) i m, i')                      

runST :: (forall s. ST s a) -> a
runST (ST s) = evalState s (M.empty, 0)

foo :: Num a => ST s (a, Bool)
foo = do
  a <- newSTRef 0 
  modifySTRef a (+100)
  b <- newSTRef False
  modifySTRef b not
  (,) <$> readSTRef a <*> readSTRef b

Теперь мы можем сделать:

> runST foo
(100, True)

Но следующее с ошибкой типа ST не выполняется:

> runST (newSTRef True)

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

Кроме того, использование unsafeCoerce означает здесь, что использование внутренних компонентов напрямую бит настолько опасно, как непосредственно с GHC.ST внутренними и State#, поэтому мы должны убедиться, что вы предоставили безопасный API, а также протестировали наши внутренние компоненты (иначе мы можем получить Segfaults в Haskell, великий грех).

Ответ 3

Поскольку я отправил свой более ранний ответ, вы указали, что не возражаете внести изменения в свое определение PT. Я рад сообщить: расслабление этого ограничения изменяет ответ на ваш вопрос от нет до да! Я уже утверждал, что вам нужно индексировать свою монаду с помощью набора типов на вашем носителе, поэтому здесь приведен пример рабочего кода, показывающего, как это сделать. (Я изначально имел это как редактирование моего предыдущего ответа, но он слишком длинный, так что мы здесь.)

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TypeOperators #-}

import Prelude

Нам понадобится более умный Monad класс, чем тот, что был в Prelude: индексированные монад-подобные вещи, описывающие пути через ориентированный граф. По причинам, которые должны стать очевидными, я также буду определять индексированные функторы.

class FunctorIx f where
    imap :: (a -> b) -> f i j a -> f i j b

class FunctorIx m => MonadIx m where
    ireturn :: a -> m i i a
    (>>>=) :: m i j a -> (a -> m j k b) -> m i k b

(>>>) :: MonadIx m => m i j a -> m j k b -> m i k b
ma >>> mb = ma >>>= \_ -> mb

replicateM_ :: MonadIx m => Int -> m i i a -> m i i ()
replicateM_ 0 _ = ireturn ()
replicateM_ n m = m >>> replicateM_ (n - 1) m

Индексированная монада использует систему типов для отслеживания хода вычисления состояния. m i j a является монадическим вычислением, которое требует входного состояния i, изменяет состояние на j и выдает значение типа a. Последовательные индексированные монады с >>>= похожи на игру в домино. Вы можете запрограммировать вычисление, которое принимает состояние от i до j в вычисление, которое идет от j до k, и получает большее вычисление от i до k. (Там более богатая версия этой индексированной монады, описанная в Kleisli Arrows of Outrageous Fortune (и в другом месте), но этого вполне достаточно для наших целей.)

Одна возможность с MonadIx - это монада File, которая отслеживает состояние дескриптора файла, гарантируя, что вы не забудете освободить ресурсы. fOpen :: File Closed Open () начинается с закрытого файла и открывает его, fRead :: File Open Open String возвращает содержимое открытого файла, а fClose :: File Open Closed () принимает файл от открытого до закрытого. Операция run выполняет вычисление типа File Closed Closed a, которое гарантирует, что ваши файлы всегда будут очищены.

Но я отвлекся: здесь нас беспокоит не дескриптор файла, а набор заданных "ячеек памяти"; типы вещей в банке памяти виртуальных машин - это то, что мы будем использовать для индексов монады. Мне нравится бесплатно получать мои монады "program/interpreter" , поскольку он выражает тот факт, что результаты живут на листах вычислений, а также способствуют композиционному использованию и повторному использованию кода, поэтому здесь функтор, который будет производить PT, когда мы подключим его к FreeIx ниже:

data PTF ref as bs r where
    MkRef_ :: a -> (ref (a ': as) a -> r) -> PTF ref as (a ': as) r
    GetRef_ :: ref as a -> (a -> r) -> PTF ref as as r
    PutRef_ :: a -> ref as a -> r -> PTF ref as as r

instance FunctorIx (PTF ref) where
    imap f (MkRef_ x next) = MkRef_ x (f . next)
    imap f (GetRef_ ref next) = GetRef_ ref (f . next)
    imap f (PutRef_ x ref next) = PutRef_ x ref (f next)

PTF параметризуется типом ссылки ref :: [*] -> * -> * - ссылки имеют право знать, какие типы находятся в системе, и индексируются по списку типов, хранящихся в памяти "интерпретатор" интерпретатора. Интересным случаем является MkRef_: создание новой ссылки добавляет в память значение типа a, взяв as до a ': as; продолжение ожидает a ref в расширенной среде. Другие операции не изменяют список типов в системе.

Когда я создаю ссылки последовательно (x <- mkRef 1; y <- mkRef 2), они будут иметь разные типы: первый будет ref (a ': as) a, а второй будет ref (b ': a ': as) b. Чтобы создать типы, мне нужен способ использовать ссылку в более крупной среде, чем та, в которой она была создана. В общем, эта операция зависит от типа ссылки, поэтому я помещу ее в класс.

class Expand ref where
    expand :: ref as a -> ref (b ': as) a

Одно из возможных обобщений этого класса завершило бы шаблон повторяющихся приложений expand с типом типа inflate :: ref as a -> ref (bs :++: as) a.

Вот еще один многоразовый бит инфраструктуры, указана свободная монада, о которой я упоминал ранее. FreeIx превращает индексированный функтор в индексированную монаду, предоставляя операцию присоединения типа Free, которая связывает рекурсивный узел в параметре функтора и операцию do-nothing Pure.

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

lift :: FunctorIx f => f i j a -> FreeIx f i j a
lift f = Free (imap Pure f)

instance FunctorIx f => MonadIx (FreeIx f) where
    ireturn = Pure
    Pure x >>>= f = f x
    Free love {- , man -} >>>= f = Free $ imap (>>>= f) love

instance FunctorIx f => FunctorIx (FreeIx f) where
    imap f x = x >>>= (ireturn . f)

Один недостаток свободных монад - это шаблон, который вы должны написать, чтобы упростить работу с Free и Pure. Ниже приведено одно-действие PT, которые составляют основу API-интерфейсов monad и некоторые синонимы шаблонов, чтобы скрыть конструкторы Free, когда мы распаковываем значения PT.

type PT ref = FreeIx (PTF ref)

mkRef :: a -> PT ref as (a ': as) (ref (a ': as) a)
mkRef x = lift $ MkRef_ x id

getRef :: ref as a -> PT ref as as a
getRef ref = lift $ GetRef_ ref id

putRef :: a -> ref as a -> PT ref as as ()
putRef x ref = lift $ PutRef_ x ref ()

pattern MkRef x next = Free (MkRef_ x next)
pattern GetRef ref next = Free (GetRef_ ref next)
pattern PutRef x ref next = Free (PutRef_ x ref next)

Это все, что нам нужно, чтобы писать вычисления PT. Вот ваш пример fib. Я использую RebindableSyntax и локально переопределяя операции монады (их индексированные эквиваленты), поэтому я могу использовать нотацию do для моей индексированной монады.

-- fib adds two Ints to an arbitrary environment
fib :: Expand ref => Int -> PT ref as (Int ': Int ': as) Int
fib n = do
    rold' <- mkRef 0
    rnew <- mkRef 1
    let rold = expand rold'
    replicateM_ n $ do
        old <- getRef rold
        new <- getRef rnew
        putRef new rold
        putRef (old+new) rnew
    getRef rold
        where (>>=) = (>>>=)
              (>>) = (>>>)
              return :: MonadIx m => a -> m i i a
              return = ireturn
              fail :: MonadIx m => String -> m i j a
              fail = error

Эта версия fib выглядит так же, как та, которую вы хотели написать в исходном вопросе. Единственное отличие (кроме локальных привязок >>= и т.д.) - это вызов expand. Каждый раз, когда вы создаете новую ссылку, вы должны expand все старые, что немного утомительно.

Наконец, мы можем закончить задание, которое мы намереваемся сделать, и построить PT -машину, которая использует Tuple в качестве носителя данных и Elem в качестве ссылочного типа.

infixr 5 :>
data Tuple as where
    E :: Tuple '[]
    (:>) :: a -> Tuple as -> Tuple (a ': as)

data Elem as a where
    Here :: Elem (a ': as) a
    There :: Elem as a -> Elem (b ': as) a

(!) :: Tuple as -> Elem as a -> a
(x :> xs) ! Here = x
(x :> xs) ! There ix = xs ! ix

updateT :: Elem as a -> a -> Tuple as -> Tuple as
updateT Here x (y :> ys) = x :> ys
updateT (There ix) x (y :> ys) = y :> updateT ix x ys

Чтобы использовать Elem в большом кортеже, чем тот, для которого вы его построили, вам просто нужно сделать его более подробным в списке.

instance Expand Elem where
    expand = There

Обратите внимание, что это развертывание Elem скорее похоже на индекс de Bruijn: более поздние связанные переменные имеют меньшие индексы.

interp :: PT Elem as bs a -> Tuple as -> a
interp (MkRef x next) tup = let newTup = x :> tup
                            in interp (next $ Here) newTup
interp (GetRef ix next) tup = let x = tup ! ix
                              in interp (next x) tup
interp (PutRef x ix next) tup = let newTup = updateT ix x tup
                                in interp next newTup
interp (Pure x) tup = x

Когда интерпретатор встречает запрос MkRef, он увеличивает размер своей памяти, добавляя x к фронту. Средство проверки типов напомнит вам, что любой ref от MkRef должен быть правильно expand ed, поэтому существующие ссылки не выходят из строя, когда кортеж меняет размер. Мы заплатили за переводчика без небезопасных бросков, но мы получили ссылочную целостность для загрузки.

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

run :: (forall ref. Expand ref => PT ref '[] bs a) -> a
run x = interp x E

Это typechecks, но работает ли он?

ghci> run (fib 5)
5
ghci> run (fib 3)
2