ceilmonad.hs

{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RebindableSyntax #-}
-- | to define <*> in terms of monad.
import Control.Monad (ap)
import Control.Category
import GHC.Types (Int, Float)
import GHC.Float 
import GHC.Real hiding (fromIntegral, floor, Real)
import qualified GHC.Real
import GHC.Num
import GHC.Base (($))

-- | allows us to use f for function and r for real w/o confusion
type Real = Float;

-- | inject(floor(r)) <= r for r real
inject :: Int -> Real; inject = GHC.Real.fromIntegral
-- | floor(inject(i)) = i
floor :: Real -> Int; floor = GHC.Real.floor

-- | Programs on an analog machine
type Prog = (Float -> Float)

-- | Run an analog machine pipeline with discrete inputs and outputs
runProgram :: Prog -> (Int -> Int)
runProgram p = floor . p . inject

-- | sequence two analog machines with a digital wire. Data will
-- be discretized between [machine f] and [machine g]
(>=>) :: Prog -> Prog -> Prog
(>=>) f g = (g . inject . floor . f)

return :: Float -> Prog; return r = \ignore -> r

-- | identity analog machine, does nothing.
idProg :: Prog; idProg = (\r -> r)


(>>=) :: Prog -> (Float -> Prog) -> Prog
p >>= r2prog = p >=> (\r -> (r2prog r) r)


point_7_5 = (int2Float 3) / (int2Float 4)

prog1 :: Prog
prog1 = do
  y <- sin
  z <- cos
  return z
 


-- Monad laws in terms of (>=>)
-- 1. Left identity: runProgram (idProg >=> p) i = runProgram p i
--
-- runProgram (idProg >=> p) i
-- [substitute >=>, runProgram]
--   := floor . (idProg . inject . floor . p) . inject i
-- [idProg = identity function]
--   := floor . (inject . floor . p) . inject i
-- [idProg = identity function]
--   := floor . (inject . floor . p) . inject i
-- [associativity]
--   := (floor . inject) . floor . p . inject i
-- [floor(inject(i)) = i]
--   :=  floor . p . inject i
-- [defn of runProgram]
--   :=  runProgram p i


-- Monad laws in terms of (>=>)
-- 2. Right identity: runProgram (p >=> idProg) i = runProgram p i
-- runProgram (p >=> idProg) i
-- [substitute >=>, runProgram]
--   := floor . (p . inject . floor . idProg) . inject i
-- [idProg = identity function, can be removed]
--   := floor . (p . inject . floor) . inject i
-- [associativity]
--   := (floor . p . inject) . (floor . inject) i
-- [floor(inject(i)) = i]
--   := (floor . p . inject) i
-- [defn of runProgram]
--   :=  runProgram p i

-- (>=>) is associative: 
-- immediate from definition of function composition, because `>=>` is
-- defined in terms of function composition

explanation.md

We are told that monads come from these mysterious things called "adjunctions". Even if we know what an adjunction is, we may not have a clear idea of we get a monad from it. So let's pick an adjunction, build a monad from it, and study its computational content.

Let's pick the adjunction that is between integers and floating point numbers:

-- | naming convention
-- |allows us to use f for function
-- | and r for real w/o confusion
type Real = Float;

-- | inject the integers into the reals
-- | inject(floor(r)) <= r for real
-- | inject(floor(i)) <= i for int
inject :: Int -> Real
inject = GHC.Real.fromIntegral
-- | floor(inject(i)) = i
floor :: Real -> Int
floor = GHC.Real.floor

This will give analog machines, which run on analog data [pure]. Unfortunately, the world is digital, so we can only interact with them by discretizing input and output [impure I/O]. The collection of analog programs is represented by:

-- | Programs on an analog machine
type Prog = (Float -> Float)

To run an analog machine, we give it an Int input, and expect an Int output.

-- | Run an analog machine pipeline
-- | with discrete inputs and outputs
runProgram :: Prog -> (Int -> Int)
runProgram p = floor . p . inject

We need to be able to sequence these analog machines together [the hallmark of a monad, after all]. But we can't sequence them in any old way: we need to connect them with digital wires which will discretize their outputs. Such is the structure of our world, since being able to run code perfectly on analog machines allows us to solve the halting problem!

-- | sequence two analog machines
-- with a digital wire. 
-- Data will
-- be discretized between
-- [machine f] and [machine g]
(>=>) :: Prog -> Prog -> Prog
(>=>) f g = (f . inject . floor . g)

Note that the discretization is given by inject . floor: That is, floor down a real valued input to an int, and then make it a Real again with an inject.

Finally, we implement the odds and ends a Monad asks us for:

return :: Float -> Prog; return r = \ignore -> r

a return analog machine ignores whatever input you feed it, and just outputs a constant value.

-- | identity analog machine, does nothing.
idProg :: Prog; idProg = (\r -> r)

The identity analog machine outputs whatever input was fed into it.

We can check that the monad laws are satisfied (in terms of >=>). See that associativity is immediately satisfied, because we have defined >=> using function composition ((.)) which is associative.

1. Left identity:
runProgram (idProg >=> p) i = runProgram p i

runProgram (idProg >=> p) i
[substitute >=>, runProgram]
  := floor . (idProg . inject . floor . p) . inject i
[idProg = identity function]
  := floor . (inject . floor . p) . inject i
[idProg = identity function]
  := floor . (inject . floor . p) . inject i
[associativity]
  := (floor . inject) . floor . p . inject i
[floor(inject(i)) = i]
  :=  floor . p . inject i
[defn of runProgram]
  :=  runProgram p i

Similarly, we can prove right identity:

2. Right identity
runProgram (p >=> idProg) i = runProgram p i

runProgram (p >=> idProg) i
[substitute >=>, runProgram]
  := floor . (p . inject . floor . idProg) . inject i
[idProg = identity function, can be removed]
  := floor . (p . inject . floor) . inject i
[associativity]
  := (floor . p . inject) . (floor . inject) i
[floor(inject(i)) = i]
  := (floor . p . inject) i
[defn of runProgram]
  :=  runProgram p i

So, we have a monoid >=> with identity idProg. Hence, we have a monad. Our monad is the monad of analog computations, with impurity coming from the discretization given by the external world. We can check that this is indeed the case:

*Main> [runProgram (sin >=> cos) x | x <- [0..10]]
[1,1,1,1,0,0,0,1,1,1,0]
*Main> [(floor.cos.inject.floor.sin.inject$x) | x <- [0..10]]
[1,1,1,1,0,0,0,1,1,1,0]

This is the poset adjunction inject -| floor : Z -> R, not quite the "ceiling monad", which refers to the adjunction ceil -| inject : R -> Z. Together, they form an adjoint triple ceil -| inject -| floor of posets!

https://ncatlab.org/nlab/show/floor#AsAdjointFunctors

@emilypi: Yes, thanks! I started writing about ceil, switched to floor, didn't change the name of the short post ;)

(@davean asked for this)
The categories between which the adjunction happens are posets, hence thin. Morphisms in them carry no computational content. Neither do natural transformations (a monad's unit and join).
As @emilypi pointed out, it's hard to illustrate non-concrete categories in Haskell, but it can be done easily in a language with dependent types, e.g. Coq: https://gist.github.com/mniip/a9fd80c7f33d0450c99106847c815004