We use the

"Yielding IO" construction for the FFI from our programming language Ermine.

That sits atop a free monad.

In

"PHOAS for Free" I show PHOAS is also just a free monad, when you look at it right, so much of the syntax manipulation in agda/coq can be viewed as just another application of a free monad. Moreover,

bound uses something that is "almost free", which is how I handle the rest of my syntax trees. ;)

I use similar free/operational monads for manipulating systems of equations for stochastic differential algebraic equations.

An example of using it to model circuits:

type Real = Signal Double

type Resistance = Real

type Inductance = Real

type Capacitance = Real

type Current = Real

type Voltage = Real

data Pin = Pin { __v :: Voltage, __i :: Current }

makeLenses ''Pin

instance Connector Pin where

cap = Pin <$> cap <*> cap

equate (Pin v1 i1) (Pin v2 i2) = do

v1 := v2

i1 := i2

flop :: (Connector a, Connector b) => (a -> Model b) -> b -> Model a

flop f b = do

top <- cap

b' <- f top

equate b b'

return top

twoPin :: Pin -> Model (Pin, Voltage)

twoPin p = do

n <- cap

p^._i + n^._i := 0

return (n, p^._v - n^._v)

basic :: Pin -> (Voltage -> Model ()) -> Model Pin

basic p k = do

(n,u) <- twoPin p

k u

return n

resistor :: Resistance -> Pin -> Model Pin

resistor r p = basic p $ \u -> r * p^._i := u

inductor :: Inductance -> Pin -> Model Pin

inductor l p = basic p $ \u -> l * der (p^._i) := u

capacitor :: Capacitance -> Pin -> Model Pin

capacitor c p = basic p $ \u -> c * der u := p^._i

conductor :: Conductance -> Pin -> Model Pin

conductor g p = basic p $ \u -> p^._i := g * p^._v

-- | <at> transformer l1 m l2 <at> represents a transformer with

-- primary inductance <at> l1 <at> , coupling inductance <at> m <at> , and secondary inductance <at> l2 <at>

transformer :: Inductance -> Inductance -> Inductance -> Pin -> Model Pin

transformer l1 m l2 p <at> (Pin v1 i1) = do

(n <at> (Pin v2 i2),u) <- twoPin

v1 := l1 * der i1 + m * der i2

v2 := m * der i1 + l2 * der i2

return n

Then I can fold together circuits with things like:

circuit = do

p <- cap

cn <- capacitor 0.00047 =<< resistor 1000 p

ind <- inductor 0.01 =<< resistor 2200 p

acn <- acVoltageSource 12 p

gn <- ground

cup [cn,ind,acn,gn]

or I can model stocks:

type Real = Signal Double

type Rate = Real

data Stock = Stock { _price, _drift, _volatility :: Real }

makeLenses ''Stock

instance Connector Stock where

cap = Stock <$> cap <*> cap <*> cap

equate (Stock p d v) (Stock p d2 v2) = do

p1 := d1

d1 := d2

v1 := v2

stock :: Model Stock

stock = do

model <at> (Stock s mu sigma) <- cap

w <- brownianMotion

der s := mu * s + sigma * der w

assume (<=) s 0

return model

-- <at> forward t r s <at> calculate the forward price of a stock <at> s <at> at time <at> t <at> assuming a risk free rate <at> r <at>

forward :: Time -> Rate -> Stock -> Model Price

forward end rate stock = do

t <- now

assume (<=) t end

return $ stock^.price * exp (rate * (end - now))

I also use the free monad as part of a variant on Tim Sheard's 2-level unifier. If you look Wren Thornton's version of

unification-fd the UTerm type is a free monad.

My machines package uses a CPS'd free monad (Plan) to build up an explicit fixed point (Machine).

wl-pprint-extras uses a free-monad based Doc to permit me to sprinkle annotations about color or whatever I want into the document.

That's most of what I can come up with off the top of my head.

-Edward