Tardis

Программируем на монаде машине времени

Этот пост написан по материалам митапа, прошедшего 26 февраля в Lambda.

Tardis - монада, которая позволяет вычислять, используя путешествия во времени. Она представляет собой объединение монады State и монады RState, которая «протягивает» состояние в обратном направлении. Далее мы рассмотрим простые примеры, немного поговорим о научных исследованиях в области Computer Science и не только, увидим Tardis изнутри и узнаем, что эта библиотека пригодна не только для написания эзотерических программ, но и для полезных в хозяйстве трюков.

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

Простые бессмысленные примеры

Простейший пример работы с Tardis выглядит так:

ex1 :: Tardis Int Double String
ex1 = do
  a <- getFuture
  sendFuture 0.5
  b <- getPast
  sendPast 10
  return $ show a ++ " " ++ show b

Здесь мы получаем a из будущего, отправляем 0.5 в будущее, получаем b из прошлого (т.е. 0.5) и отправляем в прошлое 10 (т.е. a получает значение 10). В итоге будет возвращено "10 0.5".

ex2 :: Tardis [Int] () [Int]
ex2 = do
  -- получаем числа Фибоначчи из будущего
  fibs <- getFuture
  -- меняем то, что движется из будущего на кумулятивные суммы:
  -- 1, 0, 1, 2, 3, 5, 8, 13 -> 1, 2, 3, 5, 8, 13
  modifyBackwards $ scanl (+) 0
  -- отправляем в прошлое числа Фибоначчи:
  -- 1, 2, 3, 5, 8, 13
  sendPast $ 1:fibs
  return fibs

Ещё пример:

ex3 :: [Double] -> Tardis Double (Double,Int) [Double]
ex3 [] = return []
ex3 (x:xs) = do
  -- получаем среднее из будущего
  avg <- getFuture
  -- меняем то, что отправлено в будущее,
  -- добавив к сумме элемент и к количеству единицу
  modifyForwards $ \(s, n) -> (s+x, n+1)
  -- повторяем рекурсивно оставшегося списка
  rest <- ex3 xs
  -- получаем из прошлого сумму и количество
  (s,n) <- getPast
  -- отправляем в прошлое среднее
  sendPast $ s/fromIntegral n
  -- возвращаем список с элементами, уменьшенными на среднее
  return $ (x-avg) : rest

Немного науки

Хотя может показаться, что Tardis — просто игрушка и годится только для написания эзотерических программ для смущения неокрепших умов, но на самом деле возможности компьютеров при наличии путешествий во времени — интересная математическая задача, конечно, не столь близкая к практике как квантовые компьютеры, но всё же стоящая рассмотрения.

По мировым линиям…

Дорогие читатели, вам, конечно же, известно, что специальная теория относительности запрещает движение со скоростью, большей скорости света. Поэтому не все прямые линии в четырёхмерном пространстве Минковского описывают движение материальных частиц — некоторые из них наклонены сильнее, чем линии света, т.е. сдвигаясь на одну секунду по временно́й координате, мы сдвигаемся более, чем на 300000 м в пространственных координатах. Соответственно, все линии делятся на времениподобные (находятся внутри светового конуса), светоподобные (на световом конусе), пространственноподобные (вне светового конуса). Поскольку все взаимодействия распространяются не быстрее скорости света, мы можем повлиять только на те события, которые находятся внутри светового конуса будущего, и наоборот, только те события, которые находятся внутри светового конуса прошлого, могли влиять на нас.

В общей теории относительности всё становится ещё более интересным. Четырёхмерное пространство может быть искривлено распределением масс, которое само меняется по геометрии пространства. Для нас важно то, что в результате световые конусы в разных точках могут отличаться: быть наклонёнными друг относительно друга или иметь разный раствор конуса.

Демонстрация на странице https://en.wikipedia.org/wiki/World_line

Демонстрация на странице https://en.wikipedia.org/wiki/World_line

В некоторых решениях уравнений Эйнштейна пространство искривлено так, что некоторые мировые линии могут быть замкнутыми. Таким образом, для тел на этих линиях прошлое — это и будущее. Можно сказать, у них там бесконечный день сурка.

Замкнутая времениподобная гифка

Замкнутая времениподобная гифка

…к путешествиям во времени…

Достаточно логичной позицией является принцип самосогласованности Новикова, который утверждает, что допустимы лишь самосогласованные решения уравнений. Например, нельзя запустить бильярдный шар в кротовую нору так, чтобы он вылетел из неё и ударил себя в прошлом, чтобы он не попал в кротовую нору и т.д. После того, как мы запустим шар, он вылетит из кротовой норы и ударит себя так, чтобы попасть в кротовую нору под углом, необходимым для того, чтобы вылететь из кротовой норы и ударить себя в прошлом так, как нужно. В общем, убить своего собственного дедушку нельзя. Получается что-то вроде самосбывающихся пророчеств. Например, Акрисию говорят, что его внук его убьёт, поэтому Акрисий бросает в море внука в ящике, но тот выживает, вырастает, возвращается в город и убивает Акрисия на соревнованиях. Такие дела.

…и вычислениям

В общем, получается, что пространство-время само вычисляет неподвижную точку какого-нибудь преобразования. Это разумеется, можно использовать для вычислений, так же, как квантовый компьютер использует быстрое «вычисление» каких-либо гамильтонианов природой. Например, Дэвид Дойч показал 1, что замкнутую времениподобную кривую можно использовать для решения задач из NP за полиномиальное время.

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

DISCLAIMER! Это не решает P=NP

Разумеется, наличие Tardis не «доказывает», что P=NP. Если бы и удалось промоделировать вычисления выше, они бы выполнялись полным перебором, за экспоненциальное время.

Tardis изнутри

Давайте посмотрим, как устроен Tardis. Мы начнём с монад, увидим работу монад State и Reverse State, рассмотрим класс MonadFix и неподвижные точки и, наконец, перейдём к Tardis.

Монада — это моноид в категории эндофункторов (фольклор)

Монада — это класс типов с операциями return, которая оборачивает «чистое» значение в монаду, и bind, которая позволяет преобразовывать значения внутри монады, используя функцию, получающую «чистое» значение и возвращающую монадическое.

return :: (Monad m) => a -> m a
(>>=) :: (Monad m) => m a -> (a -> m b) -> m b

Рассмотрим, например, монаду State, которая используется для представления состояния в функциональном языке. Здесь определение монады из пакета transformers немного упрощено.

newtype State s a = State { runState :: s -> (a,s) }

Мы можем определить операции так:

instance Monad (State s) where
  return a = State $ \s -> (a,s)
  m >>= f = State $ \s -> let
    (a,s') = runState m s
    (b,s'') = runState (f a) s'
    in (b, s'')

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

Но что, если мы будет передавать состояние не вниз по коду, а вверх?

Заработает ли это?

newtype RState s a = RState { runRState :: s -> (a,s) }

instance Monad (RState s) where
    return x = RState $ (,) x
    RState sf >>= f = RState $ \s ->
        let (a,s'') = sf s'
            (b,s') = runRState (f a) s
        in (b,s'')

Да, потому что связывания в let выполняются лениво. Рассмотрим простейший пример.

f = do
  a <- get
  put 1
  return a

Если этот пример записать без синтаксического сахара, получим

f = get >>= \a -> put 1 >>= \_ -> return a

Заменив (>>=) и return на их определения, получаем

f = RState $ \s -> let
  (a,s'') = (\s -> (s,s)) s'
  (b,s')  = runRState ((\a -> put 1 >>= \_ -> RState (\s -> (a,s))) a) s
  in (b,s'')

Преобразуя, получаем

f = RState $ \s -> let
  (a,s'') = (s',s')
  (b,s')  = runRState (put 1 >>= \_ -> RState (\s -> (a,s))) s
  in (b,s'')

Заменив внутреннию (>>=), получаем

f = RState $ \s -> let
  (a,s'') = (s',s')
  (b,s')  = runRState (RState $ \t -> let
                          (c,t'') = (\_ -> ((),1)) t'
                          (d,t') = runRState ((\_ -> RState (\s -> (a,s))) c) t
                      in (d,t'')) s
  in (b,s'')

Упрощая, получаем

f = RState $ \s -> let
  (a,s'') = (s',s')
  (b,s')  = runRState (RState $ \t -> let
                          (c,t'') = ((),1)
                          (d,t') = runRState (RState (\s -> (a,s))) t
                      in (d,t'')) s
  in (b,s'')

И далее

f = RState $ \s -> let
  (a,s'') = (s',s')
  (b,s')  = (\t -> let
                (c,t'') = ((),1)
                (d,t') = (\s -> (a,s)) t
                in (d,t'')) s
  in (b,s'')

В итоге получаем следующее определение

f = RState $ \s -> let
  (a,s'') = (s',s')
  (b,s')  = (a,1)
  in (b,s'')

Здесь уже видно, что b = a и a = s' = s'' = 1. Поэтому вызов runRState f 0 вернёт (1,1)

На самом деле всё чуть сложнее. Tardis не просто монада, а трансформер монад. Это означает, что наши функции (runState и runRState) могут работать не над чистыми значениями, а в какой-то другой монаде. Поэтому мы не можем использовать let, поскольку внутри должны быть монадические вычисления.

Для того, чтобы всё заработало, служит класс типов MonadFix. В нём есть операция mfix, которая позволяет за один шаг получить неподвижную точку преобразования a -> m a.

Класс MonadFix в свою очередь основан на классе ArrowLoop с функцией loop. Её можно представить себе как схему из функциональных элементов, в которой некоторые выходы могут поданы обратно на входы. То, что (стабильно) получается на остальных выходах — результат работы функции loop.

Tardis — просто объединение монад State и RState, работающих над монадой m, являющейся монадой с неподвижной точкой:

instance MonadFix m => Monad (TardisT bw fw m) where
  return x = tardis $ \s -> (x, s)
  m >>= f  = TardisT $ \ ~(bw, fw) -> do
    rec (x,  ~(bw'', fw' )) <- runTardisT m (bw', fw)
        (x', ~(bw' , fw'')) <- runTardisT (f x) (bw, fw')
    return (x', (bw'', fw''))

Ключевое слово rec — такой же синтаксический сахар для MonadFix, как do — синтаксический сахар для Monad. Здесь значение типа fw движется вниз по коду, как состояние в монаде State, а значение типа bw — вверх, как в RState.

Сложный, но практический пример

Рассмотрим язык обычных формул

data Term = Add Term Term
          | Mul Term Term
          | Const Int
          deriving (Eq,Show)
type Value = Int

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

interp0 :: Term -> Identity Value
interp0 (Add f g) = do
  x <- interp0 f
  y <- interp0 g
  return $ x+y
interp0 (Mul f g) = do
  x <- interp0 f
  y <- interp0 g
  return $ x*y
interp0 (Const x) = return x

Никаких нетривиальных монад тут нет, только Identity, которая, как и понятно из её названия, ничего не делает. Если формула — сложение двух подформул, мы вычисляем их значения и складываем, если умножение — вычисляем и умножаем, если константа — возвращаем её.

runIdentity (interp0 $
	Mul
		(Add
			(Add (Const 1) (Const 1))
			(Const 1))
		(Const 3))
9

Теперь добавим подсчёт шагов. Один шаг — это выполнение одного сложения или умножения.

interp1 :: Term -> Tardis () Int Value
interp1 (Add f g) = do
  x <- interp1 f
  y <- interp1 g
  modifyForwards (+1)
  return $ x+y
interp1 (Mul f g) = do
  x <- interp1 f
  y <- interp1 g
  modifyForwards (+1)
  return $ x*y
interp1 (Const x) = return x

По сути, мы используем монаду State для хранения количества выполненных шагов и для этого после вычисления значения подформул мы добавляем единицу к хранимому в состоянии числу. Пока всё просто, даже для императивных языков. Можно добавить терм для получения количества шагов из кода:

data Term = ...
          | Count

interp1 :: Term -> Tardis () Int Value
...
interp1 Count = getPast

Мы просто возвращаем в качестве значения формулы Count количество шагов на данный момент.

runTardis (interp1 $
	Mul
		(Add
			(Add (Const 1) (Const 1))
			(Const 1))
		(Const 3))
	((),0)
9

Теперь добавим хитрую магию RState: подсчитаем количество шагов до завершения вычисления.

interp2 :: Term -> Tardis Int () Value
interp2 (Add f g) = do
  x <- interp2 f
  y <- interp2 g
  modifyBackwards (+1)
  return $ x+y
interp2 (Mul f g) = do
  x <- interp2 f
  y <- interp2 g
  modifyBackwards (+1)
  return $ x*y
interp2 (Const x) = return x
interp2 Count = getFuture

Практически ничего не изменилось, а наш код считает количество шагов до завершения вычисления! Как пишет Уодлер [Wadler 1991], «реализацию этого на императивном языке программирования мы оставляем мазохистичному читателю». Там же он указывает, что этот способ был найден при реализации «одного строкового алгоритма», т.е. эта задача не специфична для компиляторов.

runTardis (interp2 $
	Mul
		(Add
			(Add (Const 1) (Const 1))
			(Const 1))
		(Const 3))
	(0,())
12

Библиография

Код, которые стоит посмотреть:

При написании я использовал материалы:

Видео с выступления находится здесь. Фото здесь. Полный код (здесь)[https://github.com/lambdakazan/tardis-demo]

Научные статьи о вычислениях при наличии замкнутых времениподобных кривых:

  1. David Deutsch. Quantum mechanics near closed timelike lines // Phys. Rev. D 44, 3197. –– 1991.↩

  2. Scott Aaronson. The Limits of Quantum Computers // Scientific American — 298.3 — 2008↩

  3. Scott Aaronson, John Watrous. Closed Timelike Curves Make Quantum and Classical Computing Equivalent // Proceedings of the Royal Society of London A: Mathematical, Physical and Engineering Sciences. — Vol. 465. — No. 2102. — 2009.↩

fp, tardis, meetup

Мансур Зиятдинов

5 марта 2016