How to encode possible state transitions in type?

haskell, idris, types

Solution

What you're looking for is indeed Atkey's parameterised monad, now more commonly known as the indexed 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` is the class of monad-like things `m :: k -> k -> * -> *` describing paths through a directed graph of types belonging to the kind `k`. `>>>=` binds a computation which takes the type-level state from `i` to `j` into a computation which takes it from `j` to `k`, returning a bigger computation from `i` to `k`. `ireturn` allows you to lift a pure value into a monadic computation which doesn't change the type-level state.

I'm going to use the indexed free monad to capture the structure of this sort of request-response action, largely because I don't want to have to figure out how to write the `IMonad` instance for your type myself:

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

We can build your `Door` monad for free from the following functor:

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 ()))

You can `open` a door, which causes a currently-closed door to become open, `close` a currently-open door, or `ring` the bell of a door which remains closed, presumably because the house's occupant doesn't want to see you.

Finally, the `RebindableSyntax` language extension means we can replace the standard `Monad` class with our own custom `IMonad`.

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

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

However I notice that you're not really using the binding structure of your monad. None of your building blocks `Open`, `Close` or `Ring` return a value. So I think what you really need is the following, simpler type-aligned list type:

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

Operationally, `Path :: (k -> k -> *) -> k -> k -> *` is like a linked list, but it has some extra type-level structure, once again describing a path through a directed graph whose nodes are in `k`. The elements of the list are edges `g`. `Nil` says you can always find a path from a node `i` to itself and `Cons` reminds us that a journey of a thousand miles begins with a single step: if you have an edge from `i` to `j` and a path from `j` to `k`, you can combine them to make a path from `i` to `k`. It's called a type-aligned list because the ending type of one element must match the starting type of the next.

On the other side of Curry-Howard Street, if `g` is a binary logical relation then `Path g` constructs its reflexive transitive closure. Or, categorically, `Path g` is the type of morphisms in the free category of a graph `g`. Composing morphisms in the free category is just (flipped) appending type-aligned lists.

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

Then we can write `Door` in terms of `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

You don't get `do` notation (though I think `RebindableSyntax` does allow you to overload list literals), but building computations with `(.)` looks like sequencing of pure functions, which I think is a rather good analogy for what you're doing anyway. For me it requires extra brainpower - a rare and precious natural resource - to use indexed monads. It's better to avoid the complexity of monads when a simpler structure will do.

Problem

Original source

Related problems

• What is indexed monad?