Может ли `ST`-подобная монада выполняться чисто (без библиотеки` ST`)?
Этот пост грамотный Хаскель. Просто поместите в файл, как "pad.lhs" и ghci сможет запустить его.
> {-# LANGUAGE GADTs, Rank2Types #-}
> import Control.Monad
> import Control.Monad.ST
> import Data.STRef
Итак, я смог понять, как представить ST Монада в чистом коде. Сначала мы начнем с нашего ссылочного типа. Его конкретное значение не очень важно. Самое главное, что PT s a не должен быть изоморфен любому другому типу forall s, (В частности, оно не должно быть ни изоморфным ни () ни Void.)
> newtype PTRef s a = Ref {unref :: s a} -- This is defined liked this to make `toST'` work. It may be given a different definition.
Вид для s является *->*, но это не очень важно сейчас. Это может быть многообещающим, несмотря ни на что.
> data PT s a where
> MkRef :: a -> PT s (PTRef s a)
> GetRef :: PTRef s a -> PT s a
> PutRef :: a -> PTRef s a -> PT s ()
> AndThen :: PT s a -> (a -> PT s b) -> PT s b
Довольно прямо вперед. AndThen позволяет нам использовать это как Monad, Вы можете быть удивлены, как return реализовано. Вот его монадный экземпляр (он соблюдает законы монады только в отношении runPF, будет определено позже):
> instance Monad (PT s) where
> (>>=) = AndThen
> return a = AndThen (MkRef a) GetRef --Sorry. I like minimalism.
> instance Functor (PT s) where
> fmap = liftM
> instance Applicative (PT s) where
> pure = return
> (<*>) = ap
Теперь мы можем определить fib в качестве теста.
> fib :: Int -> PT s Integer
> fib n = do
> rold <- MkRef 0
> rnew <- MkRef 1
> replicateM_ n $ do
> old <- GetRef rold
> new <- GetRef rnew
> PutRef new rold
> PutRef (old+new) rnew
> GetRef rold
И это типа проверки. Ура! Теперь я смог преобразовать это в ST (теперь мы понимаем, почему s должен был быть * -> *)
> toST :: PT (STRef s) a -> ST s a
> toST (MkRef a ) = fmap Ref $ newSTRef a
> toST (GetRef (Ref r)) = readSTRef r
> toST (PutRef a (Ref r)) = writeSTRef r a
> toST (pa `AndThen` apb) = (toST pa) >>= (toST . apb)
Теперь мы можем определить функцию для запуска PT без ссылки ST совсем:
> runPF :: (forall s. PT s a) -> a
> runPF p = runST $ toST p
runPF $ fib 7 дает 13, что правильно.
Мой вопрос, мы можем определить runPF без использования ссылки ST совсем?
Есть ли чистый способ определить runPF? PTRef определение совершенно неважно; в любом случае это только тип заполнителя. Это может быть переопределено к тому, что заставляет его работать.
Если вы не можете определить runPF чисто, докажи, что не может.
Производительность не является проблемой (если бы это было, я бы не сделал каждый return есть своя ссылка)
Я думаю, что экзистенциальные типы могут быть полезны.
Примечание: это тривиально, если мы предположим, что a динамически или что-то. Я ищу ответ, который работает со всеми a,
Примечание. На самом деле ответ не обязательно имеет непосредственное отношение к PT, Он просто должен быть таким же мощным, как ST без использования магии. (Преобразование из (forall s. PT s) является своего рода проверкой того, является ли ответ действительным или нет.)
3 ответа
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 s мы ранее выдавали указание на правильный элемент.
Это не правильно. Я могу сделать ссылку на любой тип 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 S составить хороший список индексов, а также 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])),
Это, где колеса отрываются, насколько я могу судить. То, что вы действительно хотите сделать, это сохранить размер кортежа постоянным на протяжении PT вычисление. Это потребует от вас индексации PT сам по списку типов, на которые вы можете получить ссылки, доказывая каждый раз, когда вы делаете так, что вам разрешено (давая Elem значение). Среда тогда будет выглядеть как кортеж списков, а ссылка будет состоять из Elem (чтобы выбрать правильный список) и Int (чтобы найти конкретный пункт в списке).
Этот план, конечно, нарушает правила (вам нужно изменить определение PT), но у него также есть технические проблемы. Когда я звоню MkRef на меня лежит обязанность дать Elem для значения, на которое я делаю ссылку, это довольно утомительно. (Тем не менее, вы можете обычно убедить GHC найти Elem значения с помощью пробного поиска с использованием класса hacky type.)
Другое дело: сочинение PT с становится трудно. Все части вашего вычисления должны быть проиндексированы одним и тем же списком типов. Вы можете попытаться ввести комбинаторы или классы, которые позволят вам PT, но вы также должны обновить все ссылки, когда вы делаете это. Использовать монаду было бы довольно сложно.
Возможно более чистая реализация позволила бы список типов в PT изменяться, когда вы идете вокруг типа данных: каждый раз, когда вы сталкиваетесь с MkRef тип получает один дольше. Поскольку тип вычислений меняется по мере его продвижения, вы не можете использовать обычную монаду - вам приходится прибегать к IxMonad, Если вы хотите узнать, как выглядит эта программа, посмотрите мой другой ответ.
В конечном счете, камнем преткновения является то, что тип кортежа определяется значением PT запрос. Среда - это то, что данный запрос решает хранить в ней. interp не может выбрать, что находится в кортеже, оно должно исходить из индекса на PT, Любая попытка обмануть это требование обрушится и сгорит. Теперь в истинно зависимой системе мы могли бы изучить PT значение, которое нам дали, и выяснить, что as должно быть. Увы, Haskell не является системой с зависимой типизацией.
Простое решение - обернуть State монада и представить тот же API, что и ST, В этом случае нет необходимости хранить информацию о типе среды выполнения, поскольку ее можно определить по типу STRefи обычный ST s трюк с квантификацией позволяет нам не допустить, чтобы пользователи испортили контейнер, хранящий ссылки
Мы держим ссылки в IntMap и увеличивать счетчик каждый раз, когда мы выделяем новую ссылку. Чтение и запись только изменяет 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, а также тщательно протестировать наши внутренние компоненты (иначе мы можем получить ошибки в Haskell, большой грех).
Поскольку я опубликовал свой предыдущий ответ, вы указали, что не против внесения изменений в свое определение 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, что гарантирует, что ваши файловые дескрипторы всегда будут очищены.
Но я отступаю: здесь мы имеем дело не с дескриптором файла, а с набором типизированных "областей памяти"; типы вещей в банке памяти виртуальной машины - это то, что мы будем использовать для индексов монады. Мне нравится получать мои монады "программа / интерпретатор" бесплатно, потому что они выражают тот факт, что результаты живут на листьях вычислений, и способствуют компоновке и повторному использованию кода, так что вот функтор, который будет производить 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; продолжение ожидает 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, который связывает рекурсивный узел в параметре функтора и операцию "ничего не делать" 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 с ним легче работать. Вот некоторые одиночные действия PTs, которые формируют основу API монады, и некоторые синонимы образца, чтобы скрыть 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 это скорее похоже на индекс де Брейна: более недавно связанные переменные имеют меньшие индексы.
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 должно быть правильно expanded, поэтому существующие ссылки не выходят из строя, когда кортеж меняет размер. Мы заплатили за переводчика без небезопасных приведений, но мы получили ссылочную целостность для загрузки.
Для бега с места нужно PT ожидается, что вычисления начнутся с пустого банка памяти, но мы позволим ему завершиться в любом состоянии.
run :: (forall ref. Expand ref => PT ref '[] bs a) -> a
run x = interp x E
Он проверяет, но работает ли он?
ghci> run (fib 5)
5
ghci> run (fib 3)
2