Как закодировать возможные переходы состояний в типе?

То, что вы ищете, действительно является параметризованной монадой Аткея, теперь более широко известный как индексированная монада.

class IFunctor f where
    imap :: (a -> b) -> f i j a -> f i j b
class IFunctor m => IMonad m where
    ireturn :: a -> m i i a
    (>>>=) :: m i j a -> (a -> m j k b) -> m i k b

IMonad — это класс монадоподобных вещей, m :: k -> k -> * -> * описывающих пути через ориентированный граф типов, принадлежащих виду k. >>>= связывает вычисление, которое переводит состояние уровня типа из i в j, в вычисление, которое переводит его из j в k, возвращая большее вычисление из i в k. ireturn позволяет вам преобразовать чистое значение в монадическое вычисление, которое не изменяет состояние уровня типа.

Я собираюсь использовать индексированную свободную монаду, чтобы зафиксировать структуру этого типа действия запрос-ответ, главным образом потому, что я не хочу выяснять, как написать экземпляр IMonad для вашего набери сам:

data IFree f i j a where
    IReturn :: a -> IFree f i i a
    IFree :: f i j (IFree f j k a) -> IFree f i k a

instance IFunctor f => IFunctor (IFree f) where
    imap f (IReturn x) = IReturn (f x)
    imap f (IFree ff) = IFree $ imap (imap f) ff
instance IFunctor f => IMonad (IFree f) where
    ireturn = IReturn
    IReturn x >>>= f = f x
    IFree ff >>>= f = IFree $ imap (>>>= f) ff

Мы можем бесплатно построить вашу монаду Door из следующего функтора:

data DoorState = Opened | Closed
data DoorF i j next where
    Open :: next -> DoorF Closed Opened next
    Close :: next -> DoorF Opened Closed next
    Ring :: next -> DoorF Closed Closed next

instance IFunctor DoorF where
    imap f (Open x) = Open (f x)
    imap f (Close x) = Close (f x)
    imap f (Ring x) = Ring (f x)

type Door = IFree DoorF

open :: Door Closed Opened ()
open = IFree (Open (IReturn ()))
close :: Door Opened Closed ()
close = IFree (Close (IReturn ()))
ring :: Door Closed Closed ()
ring = IFree (Ring (IReturn ()))

Вы можете open дверь, из-за которой закрытая в данный момент дверь становится открытой, close дверь, открытая в данный момент, или ring звонок двери, которая остается закрытой, предположительно потому, что обитатель дома не хочет вас видеть.

Наконец, языковое расширение RebindableSyntax означает, что мы можем заменить стандартный класс Monad нашим собственным IMonad.

(>>=) = (>>>=)
m >> n = m >>>= const n
return = ireturn
fail = undefined

door :: Door Open Open ()
door = do
    close
    ring
    open

Однако я заметил, что вы на самом деле не используете структуру привязки своей монады. Ни один из ваших стандартных блоков Open, Close или Ring не возвращает значение. Поэтому я думаю, что вам действительно нужен следующий, более простой тип списка, выровненного по типу:

data Path g i j where
    Nil :: Path g i i
    Cons :: g i j -> Path g j k -> Path g i k

Функционально Path :: (k -> k -> *) -> k -> k -> * подобен связному списку, но имеет дополнительную структуру на уровне типов, снова описывающую путь через ориентированный граф, узлы которого находятся в k. Элементами списка являются ребра g. Nil говорит, что вы всегда можете найти путь от узла i к самому себе, а Cons напоминает нам, что путешествие в тысячу миль начинается с одного шага: если у вас есть ребро от i до j и путь от j до k, вы можете объедините их, чтобы сделать путь от i до k. Он называется списком с выравниванием по типу, потому что конечный тип одного элемента должен совпадать с начальным типом следующего.

На другой стороне улицы Карри-Ховард, если g является бинарным логическим отношением, то Path g строит свое рефлексивное транзитивное замыкание. Или, категорически, Path g — это тип морфизмов в свободной категории графа g. Составление морфизмов в свободной категории — это просто (перевернутое) добавление списков, выровненных по типу.

instance Category (Path g) where
    id = Nil
    xs . Nil = xs
    xs . Cons y ys = Cons y (xs . ys)

Тогда мы можем записать Door через Path:

data DoorAction i j where
    Open :: DoorAction Closed Opened
    Close :: DoorAction Opened Closed
    Ring :: DoorAction Closed Closed

type Door = Path DoorAction

open :: Door Closed Opened
open = Cons Open Nil
close :: Door Opened Closed
close = Cons Close Nil
ring :: Door Closed Closed
ring = Cons Ring Nil

door :: Door Open Open
door = open . ring . close

Вы не получаете нотацию do (хотя я думаю, что RebindableSyntax позволяет вам перегружать литералы списков), но построение вычислений с помощью (.) выглядит как последовательность чистых функций, что, как мне кажется, является довольно хорошей аналогией того, что ты все равно делаешь. Для меня требуются дополнительные умственные способности — редкий и ценный природный ресурс — для использования индексированных монад. Лучше избегать сложности монад, когда подойдет более простая структура.