Church encoded Free monad in F#

Question

I am trying to express the Church encoding of the Free monad in F#. Free is specialized to a particular functor, Effect.

I am able to write both return_ : 'T -> Free<'T> and bind: ('T -> Free<'U>) -> Free<'T> -> Free<'U> without any problems.

A sketch of my implementation is given below.

type Effect<'T>
    = GetStr of (string -> 'T)
    | PutStr of string * 'T


module Effect = 

    let map (f: 'a -> 'b) : Effect<'a> -> Effect<'b> = function
        | GetStr k -> 
            GetStr(f << k)

        | PutStr (s,t) -> 
            PutStr(s, f t)


type Free<'T> =
    abstract Apply : ('T -> 'R) -> (Effect<'R> -> 'R) -> 'R

module Free = 
    let inline runFree (f:Free<'T>) (kp: 'T -> 'R) (kf: Effect<'R> -> 'R) : 'R = 
        f.Apply kp kf

    let return_ (x: 'a) : Free<'a> = 
        { new Free<'a>
            with
                member __.Apply kp _ = 
                    kp x
        }

    let bind (f: 'a -> Free<'b>) (m: Free<'a>) : Free<'b> = 
        { new Free<'b>
            with
                member __.Apply kp kf = 
                    runFree m
                        (fun a -> 
                            runFree (f a) kp kf
                        )
                        kf
        }

When I try to write an interpreter for this encoding, I hit a problem.

Given the following code:

module Interpret = 

    let interpretEffect = function 
        | GetStr k -> 
            let s = System.Console.ReadLine()             
            (k s , String.length s)

        | PutStr(s,t) -> 
            do System.Console.WriteLine s 
            (t , 0) 

    let rec interpret (f: Free<string * int>) = 
        Free.runFree
            f
            (fun (str,len) -> (str,len))
            (fun (a: Effect<Free<string*int>>) -> 
                let (b,n) = interpretEffect a 
                let (c,n') = interpret b 
                (c, n + n')
            )

I get a type error in the third argument to Free.runFree within the interpret function:

...

(fun (a: Effect<Free<string*int>>) -> 
      ^^^^^^^^^^^^^^^^^^ ------ Expecting a Effect<string * int> but given a Effect<Free<string*int>>

I understand why this is happening (the result type of the first function determines 'R === string*int) and suspect that can be solved using a rank-2 function (which can be encoded in F# e.g. http://eiriktsarpalis.github.io/typeshape/#/33) but I am not sure how to apply it.

Any pointers would be much appreciated.

Michael

Can you review your code samples? Second argument to `Apply` doesn't type check. — scrwtp, Oct 20 '17 at 08:48

score 1 · Answer 1 · answered Oct 22 '17 at 16:54

You do not need to do anything there, the compiler suggested type is in fact correct (and in line with the type of runFree).

It seems that what you're thinking of there is Scott encoding (ripped from this Haskell question):

runFree :: Functor f => (a -> r) -> (f (F f a) -> r) -> F f a -> r

where F f a would be your Effect-specialised Free<'a>, and f (F f a) would be Effect<Free<'a>>, which is what you're trying to use.

Whereas Church encoding would be:

runFree :: Functor f => (a -> r) -> (f r -> r) -> F f a -> r

where f r is Effect<'a> - thus making it easier to express in F# (which is why I assume you're using it in the first place.

This is what I had for interpret:

let rec interpret (f: Free<string * int>) = 
    Free.runFree
        f
        (fun (str,len) -> (str,len))
        (fun (a: Effect<_>) -> 
            let (b,n) = interpretEffect a 
            let (c,n') = interpret (Free.pureF b)
            (c, n + n')
        )

where pureF is

let pureF (x: 'a) : Free<'a> = 
    { new Free<'a> with member __.Apply kp _ = kp x }

i.e. your return_ function.

I think defining the corresponding freeF function would clear some things (like why is Effect<'a> a functor - you're not making use of this fact anywhere in the code you pasted).

Church encoded Free monad in F#

1 Answers1