Моделирование домена как типа GADT и предоставление для него do-sugar - PullRequest
Новая
       11

Моделирование домена как типа GADT и предоставление для него do-sugar

0 голосов
/ 30 мая 2018

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

newtype IntPtr = IntPtr { ptr :: Int } deriving (Eq, Ord, Show)

data Op r where 
  OpRead :: IntPtr -> Op Int
  OpWrite :: IntPtr -> Int -> Op ()

  OpCAS :: IntPtr -> Int -> Int -> Op Bool

В идеале, мы хотели бы представить некоторые алгоритмы в этой модели, используяудобную do -обозначение, например (при условии, что read = OpRead и cas = OpCAS для эстетических соображений) следующий почти буквальный перевод примера Википедии : 

import Prelude hiding (read)
import Control.Monad.Loops

add :: IntPtr -> Int -> Op Int
add p a = snd <$> do
  iterateUntil fst $ do
    value <- read p
    success <- cas p value (value + a)
    pure (success, value + a)

Как могмы достигаем этого?Давайте добавим еще пару конструкторов к Op для представления чистых введенных значений и монадической привязки: 

  OpPure :: a -> Op a
  OpBind :: Op a -> (a -> Op b) -> Op b

Итак, давайте попробуем написать экземпляр Functor.OpPure и OpBind легко, например: 

instance Functor Op where
  fmap f (OpPure x) = OpPure (f x)

Но конструкторы, которые определяют тип GADT, начинают плохо пахнуть: 

  fmap f (OpRead ptr) = do
    val <- OpRead ptr
    pure $ f val

Здесь мы предполагаем, что 'Я все равно напишу экземпляр Monad позже, чтобы избежать уродливых вложенных OpBind s.

Это правильный способ обработки таких типов, или мой дизайн просто ужасно неправильный, это признак этого?

1 Ответ

0 голосов
/ 30 мая 2018

Этот стиль использования примечания do для построения синтаксического дерева, которое будет интерпретироваться позже, моделируется свободной монадой .(На самом деле я собираюсь продемонстрировать так называемую более свободную или операционную монаду, потому что она ближе к тому, что у вас есть.)

Ваш оригинальный Op datatype - без OpPure и OpBind - представляет собой набор атомарных типизированных инструкций (а именно read, write и cas).На императивном языке программа - это, в основном, список инструкций, поэтому давайте разработаем тип данных, который представляет список Op с.

Одной из идей может быть использование фактического списка, то есть type Program r = [Op r].Понятно, что это не сработает, поскольку ограничивает каждую инструкцию в программе одним и тем же типом возврата, что не может быть очень полезным языком программирования.

Ключевое понимание заключается в том, что в любой разумной операционной семантикеВ интерпретируемом императивном языке поток управления не следует за инструкцией, пока интерпретатор не вычислил возвращаемое значение для этой инструкции.То есть, n -ая инструкция программы в общем случае зависит от результатов инструкций от 0 до n -1.Мы можем смоделировать это, используя стиль передачи продолжения. 

data Program a where
    Return :: a -> Program a
    Step :: Op r -> (r -> Program a) -> Program a

A Program - это своего рода список инструкций: это либо пустая программа, которая возвращает одно значение, либо это одна инструкция, за которой следует списокинструкций.Функция внутри конструктора Step означает, что интерпретатор, выполняющий Program, должен найти значение r, прежде чем он сможет возобновить интерпретацию остальной части программы.Таким образом, последовательность обеспечивается типом.

Чтобы собрать ваши атомарные программы read, write и cas, вам нужно поместить их в одноэлементный список.Это включает в себя помещение соответствующей инструкции в конструктор Step и передачу продолжения без операции. 

lift :: Op a -> Program a
lift i = Step i Return

read ptr = lift (OpRead ptr)
write ptr val = lift (OpWrite ptr val)
cas ptr cmp val = lift (OpCas ptr cmp val)

Program отличается от вашего настроенного Op тем, что на каждом Step есть только когда-либоодна инструкция.Левый аргумент OpBind потенциально был целым деревом Op s.Это позволило бы вам различать ассоциированные по-разному >>= s, нарушая закон ассоциативности монад.

Вы можете сделать Program монадой. 

instance Monad Program where
    return = Return
    Return x >>= f = f x
    Step i k >>= f = Step i ((>>= f) . k)

>>= в основномвыполняет конкатенацию списка - он переходит к концу списка (путем составления рекурсивных вызовов к себе при продолжениях Step) и прививает новый хвост.Это имеет смысл - это соответствует интуитивно понятной семантике «запустить эту программу, затем запустить эту программу» >>=.

С учетом того, что экземпляр Program Monad не зависит отOp, очевидным обобщением является параметризация типа инструкции и превращение Program в список любого старого набора команд. 

data Program i a where
    Return :: a -> Program i a
    Step :: i r -> (r -> Program i a) -> Program a

instance Monad (Program i) where
    -- implementation is exactly the same

Таким образом, Program i является монадой бесплатно, несмотря ни на чтоi есть.Эта версия Program является довольно общим инструментом для моделирования императивных языков.

...