{-# LANGUAGE DoRec #-} module Main where import Prelude hiding(fst, snd, succ) import System.Vacuum.OpenGL.Client import Data.IORef -- * Removing syntactic sugar -- | Choice can be represented by choosing the proper parameter as a continuation true :: a -> a -> a true = \ x y -> x false :: a -> a -> a false = \ x y -> y if_ c t e = c t e ex1 :: Char ex1 = if_ true 'a' 'b' -- | A product can be represented by a function which \"remembers\" ist components, and returns them to a continuation pair :: a -> b -> (a -> b -> r) -> r pair x y = \c -> c x y fst p = p (\ x y -> x) snd p = p (\ x y -> y) ex2 = fst (pair 'a' (3::Int)) -- ** Scott encoding (does not type check!) -- We now we combine both approaches and get the so-called Scott encoding data Nat = Zero | Succ Nat {- zero = \z c -> z succ x = \z c -> c x one = succ zero two = succ one plus x y = x y (\xm1 -> succ (plus xm1 y)) four = plus two two -} -- | In order to observe the computed integer value we map it onto a conventional integer {- foldnat z s n = n z (\p -> s (foldnat z s p)) ex4 = foldnat 0 (+1) four -} -- ** Church encoding -- We represent values by their partially applied, flipped fold function. The value n is represented by a -- a function which appies its first argument n times to it second nat2churchnat Zero = \ s z -> z nat2churchnat (Succ x) = \ s z -> s (nat2churchnat x s z) zero = \ f x -> x one = \ f x -> f x two = \ f x -> f ( f x) succ n = \ f x -> f (n f x) plus m n = \ f x -> n f (m f x) times m n = \ f x -> m (n f) x church2Int n = n (+1) 0 -- ** Let-expressions -- Non-recursive let-expresion can be mapped onto function applications -- ** Recursion -- Unfortunately we cannot represent a fixedpoint combinators in a well-typed way -- (\ f -> (\x -> f (x x)) (\x -> f (x x))) g -- -> -- (\x -> g (x x)) (\x -> g (x x)) -- -> -- g ((\x -> g (x x)) (\x -> g (x x))) -- -> -- g (g ((\x -> g (x x)) (\x -> g (x x)))) -- -- -> g (g ( g( g( ...)))) -- hence we resort to defining a single recursive function which we use to represent all other recursive functions fix :: (a -> a) -> a fix f = let fixf = f (fixf) in fixf -- ** Mutial recursion -- let f = \x -> ... g ... -- g = \y -> ... f ... -- -- is mapped onto -- -- let fg = fix (\fg -> (\x -> ... (snd fg) ... -- ,\y -> ... (fst fg) ... -- ) -- -- * How to use the module vacccuum-opengl {- \$ vacuum-opengl-server & vacuum-opengl server started - press ESC to exit. listening on port 55961 \$ ghci Prelude> :m + System.Vacuum.OpenGL Prelude System.Vacuum.OpenGL> view [1..5] Prelude System.Vacuum.OpenGL> view \$ zip "foobar" [1..6] Prelude System.Vacuum.OpenGL> :m + Data.Set Prelude System.Vacuum.OpenGL Data.Set> view \$ fromList [1..10] -} -- * SKI combinators infixl 9 :@: -- | Lambda expressions can be mapped onto variable free expressinos, -- consisting only of call to the basic combinators `S`, `K` and `I`. data SKI = S | K | I | SKI :@: SKI | Var String | Y -- | for optimising purposes we add a few extra combinators | B | C -- | and even a few more | S' | B' | C' deriving (Show) -- | step_SKI performs a single evaluation step step_SKI (S :@: f :@: g :@: x) = (f :@: x) :@: (g :@: x) step_SKI (K :@: y :@: x) = y step_SKI (I :@: x) = x step_SKI (Var s ) = Var s -- we leave global variables untouched step_SKI (Y :@: x) = let r = x :@: r in r step_SKI (B :@: f :@: g :@: x) = f :@: (g :@: x) step_SKI (C :@: f :@: g :@: x) = (f :@: x) :@: g step_SKI (S' :@: c :@: f :@: g :@: x) = c :@: (f :@: x) :@: (g :@: x) step_SKI (B' :@: c :@: f :@: g :@: x) = c :@: (f ) :@: (g :@: x) step_SKI (C' :@: c :@: f :@: g :@: x) = c :@: (f :@: x) :@: g step_SKI (l :@: r) = step_SKI l :@: r -- | The type `Lambda` represents a lambda expression data Lambda = V String | App Lambda Lambda | L String Lambda -- | l2ski compiles a `lambda`-expression into SKI form l2ski :: Lambda -> SKI l2ski (App l r) = l2ski l :@: l2ski r l2ski (V s ) = Var s l2ski (L v body) = abstract v (l2ski body) abstract :: String -> SKI -> SKI abstract v (Var s) | s == v = I | otherwise = K :@: Var s abstract v (f :@: a) = S :@: (abstract v f) :@: (abstract v a) -- (\v. f a) -> S (\v.f) (\v.a) abstract v c = K :@: c optimise (l :@: r) = optimise' (optimise l :@: optimise r) optimise' (S :@: (B :@: c :@: f) :@: g ) = optimise' (S' :@: c :@: f :@: g) optimise' (S :@: (K :@: l) :@: (K :@: r)) = K :@: (l :@: r) optimise' (S :@: ( l) :@: (K :@: r)) = C :@: l :@: r optimise' (S :@: (K :@: l) :@: r ) = B :@: l :@: r -- the S', B' and C' we leave as an exercise -- | The function `demo` performs a single outermost reduction step and shows the resulting graph on the server -- keep in mind that sharing of expressions is not visible since it gets lost during reduction demo :: SKI -> IO () demo t = do print t view t getLine demo (step_SKI t) add = V "add" x = V "x" v = V "3" t = (L "x" (add `App` x `App`x)) `App` (add `App` v `App` v) infixl 9 `App` data SKIr = IORef SKIr :@@: IORef SKIr | Varr String app f a = newIORef (f `App` a) ski2skir :: IO (IORef SKIr) -> IO (IORef SKIr) -> IO (IORef SKIr) -> IO (IORef SKIr) -> IO (IORef SKIr) -> IO (IORef SKIr) -> SKI -> IO (IORef SKIr) ski2skir s k i y b c t = toGraph t where toGraph S = s toGraph K = k toGraph I = i toGraph Y = y toGraph B = b toGraph C = c toGraph (f :@: a) = do fr <- toGraph f fa <- toGraph a newIORef (fr :@@: fa) toGraph (Var s) = newIORef (Varr s) -- Exercise: implement the reducer for SKIBCY expressions which implements the shared evaluation by overwriting applications -- with their result.