Конечные преобразователи состояний в Haskell?

Машина Mealy попеременно считывает a из потока входов a и выводит b в поток выходов. Сначала он читает, а затем выводит один раз после каждого чтения.

newtype Mealy a b = Mealy { runMealy :: a -> (b, Mealy a b) }

Машина Moore поочередно выводит b потоку выходов и считывает вход a из потока входов. Он начинается с вывода b, а затем считывается один раз после каждого вывода.

data Moore a b = Moore b (a -> Moore a b)

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

data FST a b
    = Read  (a -> FST a b)
    | Write (b,   FST a b)
    | Stop

Эквивалентом FST от компьютеров является Process. Его определение немного расплывчато. Чтобы упростить обсуждение, мы пока забудем о Process и исследуем его изнутри.

Базовый функтор

Чтобы описать, что такое Process, мы сначала заметим закономерность во всех трех машинах. Каждый из них рекурсивно обращается к самому себе для того, «что делать дальше». Мы собираемся заменить «что делать дальше» на любой тип next. Машина Mealy, сопоставляя вход с выходом, также обеспечивает работу машины next.

newtype MealyF a b next = MealyF { runMealyF :: a -> (b, next) }

Машина Moore после вывода и запроса ввода вычисляет машину next для запуска.

data MooreF a b next = MooreF b (a -> next)

Мы можем написать FST таким же образом. Когда мы Read из ввода, мы выясним, что делать next в зависимости от ввода. Когда мы Write перейдем к выводу, мы также сообщим, что делать next после вывода. Когда мы Stop дальше делать нечего.

data FSTF a b next
    = Read  (a -> next)
    | Write (b,   next)
    | Stop

Этот шаблон устранения явной рекурсии неоднократно появляется в коде Haskell и обычно называется «базовым функтором». В пакете machine базовым функтором является Step. По сравнению с нашим кодом, Step переименовал переменную типа для вывода в o, что делать дальше с r, читать в Await и записывать в Yield.

data Step k o r
  = forall t. Await (t -> r) (k t) r
  | Yield o r
  | Stop

Awaiting немного сложнее, чем Read, потому что Machine может читать из нескольких источников. Для Processes, которые могут читать только из одного источника, k — это Is применяется к определенному типу, который является доказательством второго типа Is первого типа. Для чтения Process входы a, k будут Is a.

data Step (Is a) o r
  = forall t. Await (t -> r) (Is a t) r
  | Yield o r
  | Stop

Экзистенциальная количественная оценка forall t. — это деталь реализации для работы с Sources. Увидев, что a ~ t это становится.

data Step (Is a) o r
  = forall t ~ a. Await (t -> r) Refl r
  | Yield o r
  | Stop

Если мы объединим t с a и удалим конструктор Refl, который всегда один и тот же, это будет выглядеть как наш FSTF.

data Step (Is a) o r
  = Await (a -> r) r
  | Yield  o    r
  | Stop

Дополнительный r для того, что делать дальше в Await, — это то, что делать дальше, когда больше нет входных данных.

Машина трансформер `МашинаТ`

Преобразователь машины, MachineT, делает Step почти таким же, как наш FST. В нем говорится: «Машина, работающая над некоторой монадой m, — это то, что нужно сделать в этой монаде, чтобы получить следующую Step. next вещь, которую нужно сделать после каждого шага, — это еще одна MachineT».

newtype MachineT m k o = MachineT { runMachineT :: m (Step k o (MachineT m k o)) }

newtype MachineT m (Is a) o = 
    MachineT m (
        Await (a -> MachineT m (Is a) o) (MachineT m (Is a) o)
      | Yield  o   (MachineT m (Is a) o)
      | Stop
    )

type Machine k o = forall m. Monad m => MachineT m k o

Универсальная квантификация по всем Monads m — это еще один способ сказать, что вычисления не нуждаются ни в чем из базового Monad. Это можно увидеть, заменив Identity для m.

type Machine k o = 
    MachineT Identity (
        Await (a -> MachineT Identity k o) (MachineT Identity k o)
      | Yield  o   (MachineT Identity k o)
      | Stop
    )

Процессы

Process или ProcessT — это Machine или MachineT, которые считывают только один тип ввода a, Is a.

type Process    a b = Machine    (Is a) b
type ProcessT m a b = MachineT m (Is a) b

Process имеет следующую структуру после удаления всех промежуточных конструкторов, которые всегда одинаковы. Эта структура точно такая же, как наша FST, за исключением того, что в нее добавлено «что делать дальше» в случае, если ввода больше нет.

type Process a b =
    Await (a -> Process a b) (Process a b)
  | Yield  b   (Process a b)
  | Stop

Вариант ProcessT окружен m, так что он может действовать в монаде на каждом шаге.

Process модели датчиков состояния.