Defunctionalized and Monadic - without existential types

[gampleman]

This is something that I recently discovered (thanks to @Janiczek and @pd-andy), but would like to write down to remember myself and potentially share it with everyone.

The problem is that you want to have a type, that has some operations (perhaps that you want to evaluate in some context, perhaps stateful, or at least requiring their own UI, etc), but that should also have a monadic interface (basically support andThen + succeed; which also implies having map - so basically a powerful way to structure computations in dynamic sequences).

For our example we’re going to presuppose 2 operations: Op1 returns an Int, and Op2 returns a String. The natural way to think about modelling these requirements would be:

type Operation a
    = Op1 (Float -> a)
    | Op2 (String -> a)
    | Succeed a
    | AndThen (b -> Operation a) (Operation b)

op1 : Operation Float
op1 = 
    Op1 identity

andThen : (b -> Operation a) -> Operation b -> Operation a
andThen = 
    AndThen

This won’t compile, since the AndThen case has an undeclared type variable b. Declaring it won’t help:

type Operation inp out
    = Op1 (Float -> out)
    | Op2 (String -> out)
    | Succeed a
    | AndThen (inp -> Operation ?? out) (Operation ?? inp)

Since we’re still missing an appropriate type variable.

Now for languages that support existential types and explicit quantification, we could write this as:

type Operation a
    = Op1 (Float -> a)
    | Op2 (String -> a)
    | Succeed a
    | forall b. AndThen (b -> Operation a) (Operation b)

Unfortunately, Elm doesn’t support this. For years I thought this was plain impossible in Elm’s type system and have changed designs correspondingly. However, recently I was inspired by @jhbrown Interface ideas to try again.

After much fiddling, I arrived at the following formulation:

type Operation a
    = Op1 (Int -> Operation a)
    | Op2 (String -> Operation a)
    | Succeed a

op1 : Operation Int
op1 = 
    Op1 Succeed

andThen : (a -> Operation b) -> Operation a -> Operation b
andThen fn op =
    case op of
        Succeed res ->
            fn res

        Op1 cont ->
            Op1 (\int -> andThen fn (cont int))

        Op2 cont ->
            Op2 (\str -> andThen fn (cont str))

You’ll notice that the AndThen case is no longer present in the type explicitly, however each operation looks a bit like an AndThen. The definition of our andThen function is recursive as it needs to get to the “end of the chain” of operations where it can apply the relevant function and thus elongate the chain. Fundamentally this operation always flattens out into a nice chain of:

(Pseudocode)

Op (\arg1 -> Op (\arg2 -> Op (\arg3 -> Op (\arg4 -> Succeed someReturnValue))))

For example:

andThen
   (\someReturnValue -> Op3 (\arg3 -> Succeed foo))
  (Op1 (\arg1 -> Op2 (\arg2 -> Succeed someReturnValue)))
---
Op1 (\arg1 -> 
    andThen 
        (\someReturnValue -> Op3 (\arg3 -> Succeed foo))
        (Op2 (\arg2 -> Succeed someReturnValue))
)
---
Op1 (\arg1 -> 
   Op2 (\arg2 -> 
       andThen 
          (\someReturnValue -> Op3 (\arg3 -> Succeed foo))
          (Succeed someReturnValue)
   )
)
--
Op1 (\arg1 -> 
   Op2 (\arg2 -> 
      Op3 (\arg3 -> 
          Succeed foo
      )
   )
)

Evaluation is fairly straightforward. For instance to simply compute the result synchronously and purely, one can write:

pureEval : Operation b -> b
pureEval op =
    case op of
        Op1 fun ->
            pureEval (fun 3)

        Op2 fb ->
            pureEval (fun "foo")

        Succeed res ->
            res

Here's a slightly more involved evaluator if you want an asynchronous effectful one

type Model b
    = InProgress (Operation b)
    | DoneComputation b


type Msg
    = MsgOp1 Int
    | MsgOp2 String


getNextCmd : Operation b -> Cmd Msg
getNextCmd op =
    case op of
        Op1 _ ->
            Random.generate MsgOp1 (Random.int 1 5)

        Op2 _ ->
            Random.generate MsgOp2 (Random.uniform "foo" [ "bar", "baz", "qux" ])

        Succeed _ ->
            Cmd.none

wrap : Operation a -> Model a
wrap op =
    case op of
        Succeed v ->
            DoneComputation v

        _ ->
            InProgress op


effectfulEval : Msg -> Model b -> ( Model b, Cmd Msg )
effectfulEval msg op =
    case ( msg, op ) of
        ( MsgOp1 int, InProgress (Op1 fb) ) ->
            let
                next =
                    fb int
            in
            ( wrap next, getNextCmd next )

        ( MsgOp2 str, InProgress (Op2 fb) ) ->
            let
                next =
                    fb str
            in
            ( wrap next, getNextCmd next )

        _ ->
            ( op, Cmd.none )

One can easily then define some more common “library” functions:

map : (a -> b) -> Operation a -> Operation b
map fn =
    andThen (fn >> Succeed)


map2 : (a -> b -> c) -> Operation a -> Operation b -> Operation c
map2 combiner op1 op2 =
    op1
        |> andThen
            (\v1 ->
                map (combiner v1) op2
            )

And that’s it. You can see this in action in this Ellie:

https://ellie-app.com/kw8JjkNKhtba1

[pit]

Thanks for sharing this, Jakub.

Your final implementation of Operation reminded me of something I had seen before, and now I found it: the “Free Monad”. If you have a functor, this gives you a monad for free.

Here’s something like your initial Operation type:

type Operation a
    = Op1 (Float -> a)
    | Op2 (String -> a)

This clearly is a functor:

map : (a -> b) -> Operation a -> Operation b
map ab opA =
    case opA of
        Op1 fa ->
            Op1 (fa >> ab)

        Op2 sa ->
            Op2 (sa >> ab)

From this we can get a monadic Operation type using the “Free Monad” (I used slightly different names for the constructors than in the Haskell definition to better resemble your code):

type OpM a
    = Succeed a
    | AndThen (Operation (OpM a))

with the monad functions

succeed : a -> OpM a
succeed =
    Succeed


andThen : (a -> OpM b) -> OpM a -> OpM b
andThen amb ma =
    case ma of
        Succeed a ->
            amb a

        AndThen oma ->
            AndThen (map (andThen amb) oma)

You managed to implement something very similar using only one type