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

If anyone is interested in the "fleshed out version" of the 'ceiling gives us a monad':

We are thinking of building 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]. This gives us the following types:

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

That's the data for out adjunction above. Now, 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]