Simplify and document

Author: mstewartgallus

README.md

@@ -1 +1,6 @@
-# hoas
+# HOAS
+
+A simple tagless final style compiler from a simple lambda calculus
+using Higher Order Abstract Syntax to first a point free/categorical
+representation and then to a simple call by push value representation
+using call by name.

app/Main.hs

@@ -10,7 +10,6 @@ import qualified Id
 import Lambda
 import Lambda.AsBound
 import Lambda.AsPointFree
-import Lambda.AsReified
 import Lambda.AsView
 import Lambda.Exp
 import Lambda.Hoas
@@ -31,17 +30,13 @@ main = do
   putStrLn "Point-Free Program"
   putStrLn (view (compiled y))
 
-  putStrLn ""
-  putStrLn "Program Result"
-  putStrLn (show (result z))
-
   putStrLn ""
   putStrLn "Cbpv Program"
   putStrLn (AsViewCbpv.view (cbpv w))
 
   putStrLn ""
-  putStrLn "Cbpv Result"
-  putStrLn (show (cbpvResult u))
+  putStrLn "Result"
+  putStrLn (show (result u))
 
 program :: (Lambda k, Hoas k) => k Unit U64
 program =
@@ -56,11 +51,8 @@ bound str = bindPoints str program
 compiled :: Lambda k => Id.Stream -> k Unit U64
 compiled str = pointFree (bound str)
 
-result :: Id.Stream -> Word64
-result str = reify (compiled str)
-
 cbpv :: Cbpv c d => Id.Stream -> d (Cbpv.Sort.U (Cbpv.Sort.F Cbpv.Sort.Unit)) (Cbpv.Sort.U (AsAlgebra U64))
 cbpv str = toCbpv (compiled str)
 
-cbpvResult :: Id.Stream -> Word64
-cbpvResult str = AsEval.reify (cbpv str)
+result :: Id.Stream -> Word64
+result str = AsEval.reify (cbpv str)

hoas.cabal

@@ -4,7 +4,7 @@ cabal-version: 1.12
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: a75cb00ad3e76787779dab2e87dc7f48cba6cfc779ecf4b1784f08e14b351d94
+-- hash: aad680befe2c5d1871e747b2a2d9b568b2a2da878057a3ed205b4918b62dc6c6
 
 name:           hoas
 version:        0.1.0.0
@@ -36,7 +36,6 @@ library
       Lambda
       Lambda.AsBound
       Lambda.AsPointFree
-      Lambda.AsReified
       Lambda.AsView
       Lambda.Exp
       Lambda.Hoas

src/AsCallByName.hs

@@ -17,7 +17,7 @@ import qualified Lambda.Exp as Exp
 import qualified Lambda.Product as Product
 import qualified Lambda.Sum as Sum
 import qualified Lambda.Type as Type
-import Prelude hiding (id, (.), (<*>))
+import Prelude hiding (curry, id, return, uncurry, (.), (<*>))
 
 newtype Expr c a b = Expr (c (U (AsAlgebra a)) (U (AsAlgebra b)))
 
@@ -37,23 +37,34 @@ instance Cbpv c d => Category (Expr d) where
   Expr f . Expr g = Expr (f . g)
 
 instance Cbpv c d => Product.Product (Expr d) where
-  unit = Expr (thunk (returns unit))
+  unit = Expr (thunk (return unit))
 
   first = Expr (thunk (force first . force id))
   second = Expr (thunk (force second . force id))
-  Expr f # Expr g = Expr (thunk (returns f `to` ((returns g . returns first) `to` returns ((second . first) # second))))
+  Expr f &&& Expr g = Expr (thunk (return f `to` ((return g . return first) `to` return ((second . first) &&& second))))
 
 instance Cbpv c d => Sum.Sum (Expr d) where
   absurd = Expr (thunk (force absurd . force id))
 
-  left = Expr (thunk (returns left))
-  right = Expr (thunk (returns right))
-  Expr f ! Expr g = Expr (thunk (force id . force (thunk (returns f) ! thunk (returns g)) . force id))
+  left = Expr (thunk (return left))
+  right = Expr (thunk (return right))
+  Expr f ||| Expr g = Expr (thunk (force id . force (thunk (return f) ||| thunk (return g)) . force id))
 
 instance Cbpv c d => Exp.Exp (Expr d) where
-  lambda (Expr f) = Expr (thunk (lambda (force f . returns (thunk id))))
-  Expr f <*> Expr x = Expr (thunk (force f <*> x))
+  curry (Expr f) = Expr (thunk (lambda (force f . return (thunk id))))
+  uncurry (Expr f) = Expr (thunk (eval (force f) . return shuffle . force id))
+    where
+      shuffle :: Cbpv c d => d (b * a) (a * b)
+      shuffle = second &&& first
+
+eval :: Cbpv stk d => stk (F env) (a ~> b) -> stk (F (a * env)) b
+eval f = uncurry f . assocIn
+
+lambda :: Cbpv stk d => stk (F (env * a)) b -> stk (F env) (a ~> b)
+lambda f = curry (f . return shuffle . assocOut)
+  where
+    shuffle = second &&& first
 
 instance Cbpv c d => Lambda.Lambda (Expr d) where
-  u64 x = Expr (thunk (returns (u64 x)))
+  u64 x = Expr (thunk (return (u64 x)))
   add = Expr (thunk (addLazy . force id))

src/Cbpv.hs

@@ -9,8 +9,17 @@ module Cbpv (Cbpv (..)) where
 import Cbpv.Sort
 import Control.Category
 import Data.Word (Word64)
-import Prelude hiding (id, (.), (<*>))
-
+import Prelude hiding (curry, id, return, uncurry, (.), (<*>))
+
+-- |
+-- As opposed to the usual monadic interface call by push value is based
+-- around adjoint functors on two different categories.
+--
+-- There is a different formulation using oblique morphisms and an
+-- indexed category instead of using the asymmetric tensor but was
+-- difficult to work with.
+--
+-- Paul Blain Levy. "Call-by-Push-Value: A Subsuming Paradigm".
 class (Category stk, Category dta) => Cbpv stk dta | stk -> dta, dta -> stk where
   thunk ::
     stk (F x) y ->
@@ -19,7 +28,7 @@ class (Category stk, Category dta) => Cbpv stk dta | stk -> dta, dta -> stk wher
     dta x (U y) ->
     stk (F x) y
 
-  returns ::
+  return ::
     dta env a ->
     stk (F env) (F a)
   to ::
@@ -28,24 +37,27 @@ class (Category stk, Category dta) => Cbpv stk dta | stk -> dta, dta -> stk wher
     stk (env & k) b
 
   unit :: dta x Unit
-  (#) :: dta env a -> dta env b -> dta env (a * b)
+  (&&&) :: dta env a -> dta env b -> dta env (a * b)
   first :: dta (a * b) a
   second :: dta (a * b) b
 
   absurd :: dta Void x
-  (!) :: dta a c -> dta b c -> dta (a + b) c
+  (|||) :: dta a c -> dta b c -> dta (a + b) c
   left :: dta a (a + b)
   right :: dta b (a + b)
 
-  lambda :: stk (F (env * a)) b -> stk (F env) (a ~> b)
-  (<*>) :: stk (F env) (a ~> b) -> dta env a -> stk (F env) b
+  assocOut :: stk (a & (b & c)) ((a * b) & c)
+  assocIn :: stk ((a * b) & c) (a & (b & c))
+
+  curry :: stk (a & env) b -> stk env (a ~> b)
+  uncurry :: stk env (a ~> b) -> stk (a & env) b
 
   u64 :: Word64 -> dta x U64
 
   -- fixme.. have optimized version...
   add :: dta Unit (U (U64 ~> F (U (U64 ~> F U64))))
   addLazy :: stk (F Unit) (U (F U64) ~> U (F U64) ~> F U64)
 
-infixl 9 #
+infixl 9 &&&
 
-infixl 9 !
+infixl 9 |||

src/Cbpv/AsEval.hs

@@ -7,80 +7,84 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE NoStarIsType #-}
 
-module Cbpv.AsEval (reify, Stack, DataM, Code, Data) where
+module Cbpv.AsEval (reify, Stack, Code, Action, Data) where
 
 import Cbpv
 import Control.Category
 import Data.Word
 import Cbpv.Sort
 import Prelude hiding ((.), id)
 
-reify :: DataM (U (F Unit)) (U (F U64)) -> Word64
-reify (D f) = case f (Thunk $ \w -> Unit :& Effect w) of
+reify :: Code (U (F Unit)) (U (F U64)) -> Word64
+reify (C f) = case f (Thunk $ \w -> Unit :& Effect w) of
   Thunk t -> case t 0 of
     (U64 y :& _) -> y
 
-newtype DataM a b = D (Data a -> Data b)
+newtype Code a b = C (Data a -> Data b)
 
-newtype Stack a b = C (Code a -> Code b)
+newtype Stack a b = S (Action a -> Action b)
 
 data family Data (a :: Set)
 
-data instance Data (U a) = Thunk (Int -> Code a)
+data instance Data (U a) = Thunk (Int -> Action a)
 
 data instance Data Unit = Unit
 data instance Data Void
 data instance Data (a * b) = Pair { firstOf :: (Data a), secondOf :: (Data b) }
 data instance Data (a + b) = L (Data a) | R (Data b)
 newtype instance Data U64 = U64 Word64
 
-data family Code (a :: Algebra)
-data instance Code Initial = Effect Int
-data instance Code (a & b) = Data a :& Code b
-newtype instance Code (a ~> b) = Lam (Data a -> Code b)
+-- | Actions are CBPVs computations but we use a different name for brevity
+data family Action (a :: Algebra)
+data instance Action Initial = Effect Int
+data instance Action (a & b) = Data a :& Action b
+newtype instance Action (a ~> b) = Lam (Data a -> Action b)
 
-instance Category DataM where
-  id = D id
-  D f . D g = D (f . g)
-
-instance Category Stack where
+instance Category Code where
   id = C id
   C f . C g = C (f . g)
 
-instance Cbpv Stack DataM where
-  to (C f) (C g) = C $ \x@(env :& _) -> case f x of
+instance Category Stack where
+  id = S id
+  S f . S g = S (f . g)
+
+instance Cbpv Stack Code where
+  to (S f) (S g) = S $ \x@(env :& _) -> case f x of
     (y :& k) -> g ((Pair env y) :& k)
-  returns (D f) = C $ \(x :& w) -> f x :& w
+  return (C f) = S $ \(x :& w) -> f x :& w
 
-  thunk (C f) = D $ \x -> Thunk $ \w -> f (x :& Effect w)
-  force (D f) = C $ \(x :& Effect w) -> case f x of
+  thunk (S f) = C $ \x -> Thunk $ \w -> f (x :& Effect w)
+  force (C f) = S $ \(x :& Effect w) -> case f x of
     Thunk t -> t w
 
-  absurd = D $ \x -> case x of {}
-  D x ! D y = D $ \env -> case env of
+  absurd = C $ \x -> case x of {}
+  C x ||| C y = C $ \env -> case env of
     L l -> x l
     R r -> y r
-  left = D L
-  right = D R
+  left = C L
+  right = C R
+
+  unit = C $ const Unit
+  C x &&& C y = C $ \env -> Pair (x env) (y env)
+  first = C firstOf
+  second = C secondOf
 
-  unit = D $ const Unit
-  D x # D y = D $ \env -> Pair (x env) (y env)
-  first = D firstOf
-  second = D secondOf
+  curry (S f) = S $ \env -> Lam $ \x -> f (x :& env)
+  uncurry (S f) = S $ \(x :& env) -> case f env of
+     Lam y -> y x
 
-  lambda (C f) = C $ \(env :& w) -> Lam $ \x -> f ((Pair env x) :& w)
-  C f <*> D x = C $ \(env :& w) -> case f (env :& w) of
-     Lam y -> y (x env)
+  assocOut = S $ \(a :& (b :& c)) -> (Pair a b) :& c
+  assocIn = S $ \((Pair a b) :& c) -> a :& (b :& c)
 
-  u64 x = D $ const (U64 x)
-  add = D $ \Unit ->
+  u64 x = C $ const (U64 x)
+  add = C $ \Unit ->
     Thunk $ \w0 ->
     Lam $ \(U64 x) ->
     (:& Effect w0) $ Thunk $ \w1 ->
     Lam $ \(U64 y) ->
     U64 (x + y) :& Effect w1
 
-  addLazy = C $ \(Unit :& Effect w0) ->
+  addLazy = S $ \(Unit :& Effect w0) ->
     Lam $ \(Thunk x) -> Lam $ \(Thunk y) -> case x w0 of
        U64 x' :& Effect w1 -> case y w1 of
          U64 y' :& Effect w2 -> U64 (x' + y') :& Effect w2

src/Cbpv/AsView.hs

@@ -26,23 +26,26 @@ instance Category Code where
 
 instance Cbpv Stack Code where
   to (Stack f) (Stack x) = Stack ("(to " ++ f ++ " " ++ x ++ ")")
-  returns (Code f) = Stack ("(return " ++ f ++ ")")
+  return (Code f) = Stack ("(return " ++ f ++ ")")
 
   thunk (Stack f) = Code ("(thunk " ++ f ++ ")")
   force (Code f) = Stack ("(force " ++ f ++ ")")
 
   unit = Code "unit"
-  Code f # Code x = Code ("⟨" ++ f ++ " , " ++ x ++ "⟩")
+  Code f &&& Code x = Code ("⟨" ++ f ++ " , " ++ x ++ "⟩")
   first = Code "π₁"
   second = Code "π₂"
 
   absurd = Code "absurd"
-  Code f ! Code x = Code ("[" ++ f ++ " , " ++ x ++ "]")
+  Code f ||| Code x = Code ("[" ++ f ++ " , " ++ x ++ "]")
   left = Code "i₁"
   right = Code "i₂"
 
-  lambda (Stack f) = Stack ("(λ " ++ f ++ ")")
-  Stack f <*> Code x = Stack ("(" ++ f ++ " " ++ x ++ ")")
+  assocOut = Stack "out"
+  assocIn = Stack "in"
+
+  curry (Stack f) = Stack ("(λ " ++ f ++ ")")
+  uncurry (Stack f) = Stack ("(! " ++ f ++ ")")
 
   u64 x = Code (show x)
   add = Code "add"

src/Cbpv/Sort.hs

@@ -1,5 +1,4 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE NoStarIsType #-}
 
@@ -19,8 +18,6 @@ module Cbpv.Sort
   )
 where
 
-import Data.Typeable ((:~:) (..))
-
 type Set = SetImpl
 
 type Unit = 'Unit

src/Id.hs

@@ -1,3 +1,8 @@
+-- |
+--
+-- Use the trick from functional pearl "On generating unique names by
+-- Lennart Augustsson, Mikael Rittri and Dan Synek" to generate a unique
+-- stream of ids.
 module Id (Id, stream, Stream (..)) where
 
 import Data.Atomics.Counter

src/Lambda.hs

@@ -1,5 +1,10 @@
 {-# LANGUAGE TypeOperators #-}
 
+-- |
+--
+-- Export the final type class of the simple lambda calculus language.
+-- Here we finish the Lambda type class off with some basic operations on
+-- integers.
 module Lambda (Lambda (..)) where
 
 import Data.Word (Word64)
@@ -9,5 +14,5 @@ import Lambda.Sum
 import Lambda.Type
 
 class (Sum k, Product k, Exp k) => Lambda k where
-  u64 :: Word64 -> Value k U64
-  add :: Value k (U64 ~> U64 ~> U64)
+  u64 :: Word64 -> k Unit U64
+  add :: k Unit (U64 ~> U64 ~> U64)