bound-2.0.4: examples/Imperative.hs
{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, RankNTypes, ScopedTypeVariables #-}
module Main where
-- It's possible to use bound "sideways" in order to support terms which do not
-- have a Monad instance. A typical situation in which this would happen is when
-- modelling an imperative language: variables are bound by statements, but they
-- are used in positions where it would make no sense to replace them by another
-- statement.
import Bound.Scope -- .Simple
import Bound.Var
import Control.Monad (ap)
import Data.Functor.Identity
import Data.IORef
import Data.Void (Void, absurd)
-- PART 1: We want to model a tiny assembly language.
--
-- %0 = add 1 2
-- %1 = add %0 %0
-- ret %1
--
-- Add binds a fresh variable, and its operands can either be literals or
-- previously-bound variables. Ret must be the last instruction.
--
-- Operand is monadic, traversable, and satisfies all the other requirements in
-- order to be used with bound. But this is not sufficient, since Operand is
-- not the whole language: we also need to define Prog, the sequence of
-- instructions.
data Operand a
= Lit Int
| Var a
deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
instance Applicative Operand where
pure = Var
(<*>) = ap
instance Monad Operand where
return = pure
Lit i >>= _ = Lit i
Var x >>= f = f x
-- The following definition correctly models the instructions and their free
-- variables. But since the Var in Operand cannot be replaced with a Prog, this
-- definition is not monadic, and so we cannot manipulate the (Scope () Prog a)
-- using bound's functions. This defeats the point of using Scope at all!
--
-- data Prog a
-- = Ret (Operand a)
-- | Add (Operand a) (Operand a)
-- (Scope () Prog a) -- one more bound variable, available
-- -- in the rest of the program
--
-- The sideways trick is to replace the Operand constructor with a (* -> *) type
-- parameter. Instantiating this with the real Operand will allow Operand to
-- access the same free variables as Prog. But if we instantiate this with
-- (Scope () Operand) instead, then the operands will have access to one extra
-- bound variable! This way, we can bind fresh variables which can only be used
-- inside the operands, and not in Prog.
data Prog operand a
= Ret (operand a)
| Add (operand a) (operand a)
(Prog (Scope () operand) a)
deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
-- The fact that the variables are not available in Prog after they are bound
-- might seem strange, and we'll fix this in part 2, but it is actually a good
-- thing. We want to be able to replace those variables with operand values, and
-- that would not be possible if variables were allowed to appear inside Prog
-- but outside of an operand.
pInstantiate1 :: forall operand b a. (Applicative operand, Monad operand)
=> operand a
-> Prog (Scope b operand) a
-> Prog operand a
pInstantiate1 = go instantiate1
where
-- A value of type (Prog (Scope b operand) a) contains operands of type
-- (Scope b operand a), on which we can call instantiate1:
--
-- instantiate1 :: operand a -> Scope b operand a -> operand a
--
-- In the function below, (Scope b operand) and operand become o and o',
-- and instantiate1 is called f:
--
-- f :: operand v -> o v -> o' v
go :: forall o o' u. (Monad o, Monad o')
=> (forall v. operand v -> o v -> o' v)
-> operand u -> Prog o u -> Prog o' u
go f x (Ret o) = Ret (f x o)
go f x (Add o1 o2 cc) = Add (f x o1) (f x o2)
$ go f' x cc
where
-- The rest of the program has access to one extra variable:
--
-- cc :: Prog (Scope () (Scope b operand)) a
--
-- In there, the operands have type (Scope () (Scope b operand) a), and
-- this time we cannot call instantiate1 because it would instantiate ()
-- instead of instantiating b. Instead, we create a function f' which
-- preserves the outer (Scope ()):
--
-- f' :: operand a -> Scope () (Scope b operand) a -> Scope () operand a
-- f' :: operand a -> Scope () o a -> Scope () o' a
--
-- In the recursive call to go, (Scope () (Scope b operand)) and
-- (Scope () operand) become o and o', and f' is called f.
f' :: operand v -> Scope () o v -> Scope () o' v
f' v = toScope . f (fmap F v) . fromScope
pAbstract1 :: forall operand a. (Applicative operand, Monad operand, Eq a)
=> a
-> Prog operand a
-> Prog (Scope () operand) a
pAbstract1 = go abstract1
where
go :: forall o o' u. (Eq u, Monad o, Monad o')
=> (forall v. Eq v => v -> o v -> o' v)
-> u -> Prog o u -> Prog o' u
go f x (Ret o) = Ret (f x o)
go f x (Add o1 o2 cc) = Add (f x o1) (f x o2)
$ go f' x cc
where
f' :: forall v. Eq v => v -> Scope () o v -> Scope () o' v
f' v = toScope . f (F v) . fromScope
evalOperand :: Operand Void -> Int
evalOperand (Lit i) = i
evalOperand (Var void) = absurd void
-- |
-- >>> :{
-- let Just prog = closed
-- $ Add (Lit 1) (Lit 2) $ pAbstract1 "%0"
-- $ Add (Var "%0") (Var "%0") $ pAbstract1 "%1"
-- $ Ret (Var "%1")
-- :}
--
-- >>> evalProg prog
-- 6
evalProg :: Prog Operand Void -> Int
evalProg (Ret o) = evalOperand o
evalProg (Add o1 o2 cc) = evalProg cc'
where
result :: Int
result = evalOperand o1 + evalOperand o2
cc' :: Prog Operand Void
cc' = pInstantiate1 (Lit result) cc
-- PART 2: Here's a slightly more complicated language.
--
-- %0 = add 1 2
-- %1 = add %0 %0
-- swp %0 %1
-- ret %1
--
-- The new swp command swaps the contents of two variables, so the two arguments
-- must be previously-bound variables, they cannot be literals. This time the
-- naïve definition looks like this:
--
-- data Prog' a
-- = Ret' (Operand a)
-- | Swp' a a
-- (Prog' a)
-- | Add' (Operand a) (Operand a)
-- (Scope () Prog' a)
--
-- If we apply the sideways trick to this definition, the newly-bound variables
-- will only be available in the operands, and so it won't be possible to call
-- swp on them. The first step towards a solution is to add seemingly-useless
-- Identity wrappers:
--
-- data Prog' a
-- = Ret' (Operand a)
-- | Swp' (Identity a) (Identity a)
-- (Prog' a)
-- | Add' (Operand a) (Operand a)
-- (Scope () Prog' a)
--
-- We can now apply the sideways trick twice: once for Operand, and once for
-- Identity. This gives us a lot of control: we can bind fresh variables which
-- can only be used inside the operands, we can bind fresh variables which can
-- be used inside Prog but not inside the operands, and as required for this
-- example, we can bind fresh variables which can be used in both.
data Prog' operand identity a
= Ret' (operand a)
| Swp' (identity a) (identity a)
(Prog' operand identity a)
| Add' (operand a) (operand a)
(Prog' (Scope () operand) (Scope () identity) a)
deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
-- Bound variables can now occur in both operand and identity, so we can no
-- longer instantiate them with operands. Instead, we'll have to instantiate
-- them with a value which both (Operand a) and (Identity a) can contain:
-- a free variable.
pInstantiate1' :: ( Applicative operand, Monad operand
, Applicative identity, Monad identity
)
=> a
-> Prog' (Scope () operand) (Scope () identity) a
-> Prog' operand identity a
pInstantiate1' = go (instantiate1 . pure) (instantiate1 . pure)
where
go :: forall o o' i i' u. (Monad i, Monad i', Monad o, Monad o')
=> (forall v. v -> o v -> o' v)
-> (forall v. v -> i v -> i' v)
-> u -> Prog' o i u -> Prog' o' i' u
go fo fi x = go'
where
go' (Ret' o) = Ret' (fo x o)
go' (Swp' i1 i2 cc) = Swp' (fi x i1)
(fi x i2)
(go' cc)
go' (Add' o1 o2 cc) = Add' (fo x o1)
(fo x o2)
(go fo' fi' x cc)
fo' :: v -> Scope () o v -> Scope () o' v
fo' v = toScope . fo (F v) . fromScope
fi' :: v -> Scope () i v -> Scope () i' v
fi' v = toScope . fi (F v) . fromScope
pAbstract1' :: ( Applicative operand, Monad operand
, Applicative identity, Monad identity
, Eq a
)
=> a
-> Prog' operand identity a
-> Prog' (Scope () operand) (Scope () identity) a
pAbstract1' = go abstract1 abstract1
where
go :: forall o o' i i' u. (Eq u, Monad i, Monad i', Monad o, Monad o')
=> (forall v. Eq v => v -> o v -> o' v)
-> (forall v. Eq v => v -> i v -> i' v)
-> u -> Prog' o i u -> Prog' o' i' u
go fo fi x = go'
where
go' (Ret' o) = Ret' (fo x o)
go' (Swp' i1 i2 cc) = Swp' (fi x i1)
(fi x i2)
(go' cc)
go' (Add' o1 o2 cc) = Add' (fo x o1)
(fo x o2)
(go fo' fi' x cc)
fo' :: Eq v => v -> Scope () o v -> Scope () o' v
fo' v = toScope . fo (F v) . fromScope
fi' :: Eq v => v -> Scope () i v -> Scope () i' v
fi' v = toScope . fi (F v) . fromScope
evalOperand' :: Operand (IORef Int) -> IO Int
evalOperand' (Lit i) = return i
evalOperand' (Var ref) = readIORef ref
-- |
-- >>> :{
-- let Just prog' = closed
-- $ Add' (Lit 1) (Lit 2) $ pAbstract1' "%0"
-- $ Add' (Var "%0") (Var "%0") $ pAbstract1' "%1"
-- $ Swp' (Identity "%0") (Identity "%1")
-- $ Ret' (Var "%1")
-- :}
--
-- >>> evalProg' prog'
-- 3
evalProg' :: Prog' Operand Identity (IORef Int) -> IO Int
evalProg' (Ret' o) = evalOperand' o
evalProg' (Swp' (Identity ref1) (Identity ref2) cc) = do
x <- readIORef ref1
y <- readIORef ref2
writeIORef ref1 y
writeIORef ref2 x
evalProg' cc
evalProg' (Add' o1 o2 cc) = do
result <- (+) <$> evalOperand' o1 <*> evalOperand' o2
ref <- newIORef result
evalProg' (pInstantiate1' ref cc)
main :: IO ()
main = return ()