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

Question

Я пытаюсь повторить в Haskell этот кусок Идрис кода, который обеспечивает соблюдение правильной последовательности действий по типам:

data DoorState = DoorClosed | DoorOpen 
data DoorCmd : Type -> 
       DoorState -> 
DoorState -> 
       Type where 
     Open : DoorCmd () DoorClosed DoorOpen 
     Close : DoorCmd () DoorOpen DoorClosed 
     RingBell : DoorCmd() DoorClosed DoorClosed 
     Pure : ty -> DoorCmd ty state state 
     (>>=) : DoorCmd a state1 state2 -> 
       (a -> DoorCmd b state2 state3) -> 
       DoorCmd b state1 state3 

Благодаря перегрузки (>>=) оператора, можно написать одноместную код, как:

do Ring 
    Open 
    Close 

но компилятор отвергает неправильные переходы как:

do Ring 
    Open 
    Ring 
    Open 

Я пытался следовать этому образцу в следующем фрагменте: Haskell

data DoorState = Closed | Opened 

data DoorCommand (begin :: DoorState) (end :: DoorState) a where 
    Open :: DoorCommand 'Closed 'Opened() 
    Close :: DoorCommand 'Opened 'Closed() 
    Ring :: DoorCommand 'Closed 'Closed() 

    Pure :: x -> DoorCommand b e x 
    Bind :: DoorCommand b e x -> (x -> DoorCommand e f y) -> DoorCommand b f y 

instance Functor (DoorCommand b e) where 
    f `fmap` c = Bind c (\ x -> Pure (f x)) 

-- instance Applicative (DoorCommand b e) where 
-- pure = Pure 
-- f <*> x = Bind f (\ f' -> Bind x (\ x' -> Pure (f' x'))) 

-- instance Monad (DoorCommand b e) where 
-- return = Pure 
-- (>>=) = Bind 

Но, конечно, это не удается: В Applicative и Monad экземпляров не могут быть определены правильно, так как они требуют два разных экземпляра правильно последовательности операций. Конструктор Bind может использоваться для обеспечения правильной последовательности, но я не могу использовать «более приятную» нотацию.

Как я могу написать этот код, чтобы использовать do-notation, например. для предотвращения недействительных последовательностей Command?

Answer 1

Что вам нужно, так это parameterised monad Аткина, теперь более известный как индексированная монада .

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 и путь от до 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 это позволяет перегружать список литералов), но строительные расчеты с (.) выглядит как последовательность чистых функций, что я считаю довольно хорошей аналогией того, что вы делаете. Для меня это требует дополнительных умственных способностей - редкого и драгоценного природного ресурса - для использования индексированных монадов. Лучше избегать сложности монадов, когда будет работать более простая структура.