A Haskell implementation of the categorical semantics for the effectful CBN lambda calculus

CBNLambdaEff.hs

{-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls #-}

{-

A Haskell-based implementation of the monadic semantics for the
simply-typed Call-By-Name computational lambda calculus, following
Moggi's 'Computational lambda-calculus and monads' (1989) (technical report version)
but for the typed calculus (rather than untyped as in this paper).

Category theory seminar, Programming Languages and Systems group,
University of Kent, 12/01/2018

-}

module Main where

import Control.Monad
import Control.Category hiding (id, (.))

-- Types for the lambda calculus
data Fun a b
data Z
data Unit

-- Syntax and typing derivations
data Lambda ctxt result where

  -- Simply-typed lambda calculus core

  Var ::
      --------------------
       Lambda (gam, a) a

  App ::
       Lambda gam (Fun a b)
   ->  Lambda gam a
   -> ---------------------
       Lambda gam b

  Abs ::
       Lambda (gam, a) b
   -> ---------------------
       Lambda gam (Fun a b)

   -- Explicit structural rule

  Perm :: Perm gam' gam
       -> Lambda gam t
       -> Lambda gam' t

   -- Strict sequential composition

  Let ::
       Lambda gam sigma           -- gam |- e1 : sigma
   ->  Lambda (gam, sigma) tau    -- gam, x : sigma |- e2 : tau
   -> -------------------------
       Lambda gam tau             -- gam |- let x = e1 in e2 : tau

   -- Some bonuses: integers and addition, and effectful primitives

  Const :: Int -> Lambda gam Z

  Plus :: Lambda gam Z
        -> Lambda gam Z
        -> Lambda gam Z

  Bing :: Lambda gam Unit
  Bong :: Lambda gam Unit

-- Representation of context permutations

data Perm gam' gam where
      Weaken      :: Perm (gam, a) gam
      Contract    :: Perm (gam, a) ((gam, a), a)
      Exchange    :: Perm ((gam, a), b) ((gam, b), a)
      Congruence  :: Perm gam' gam -> Perm (gam', a) (gam, a)

-- ***** Various constructions for our underlying Cartesian-closed Category

-- *** Terminal object
type One = ()

-- *** Products

-- <f, g> : a -> b * c
pair :: (a -> b) -> (a -> c) -> (a -> (b, c))
pair f g x = (f x, g x)

-- (f * g) : (a * c) -> (b * d)
cross :: (a -> b) -> (c -> d) -> (a, c) -> (b, d)
cross f g (x, y) = (f x, g y)

-- *** Exponents

-- the universal construction of exponents
lam :: ((a, b) -> c) -> (a -> (b -> c))
lam = curry

-- with the 'app' (or 'ev') map
-- such that app . (lam g `cross` id) = g
app :: (a -> b, a) -> b
app (f, x) = f x

-- *** A strong monad

type T = IO

eta :: a -> T a
eta = return

mu :: T (T a) -> T a
mu = join

-- Tensorial strength
strengthR :: (a, T b) -> T (a, b)
strengthR (x, y) = do
  y' <- y
  return (x, y')

-- The swapped version of tensorial strength derived by commutativity of products
strengthL :: (T a, b) -> T (a, b)
strengthL = fmap c . strengthR . c
  where c (x, y) = (y, x)

-----------------------------------------------------------------
-- The CBN model of the computational lambda calculus

-- model types as objects in our base category
type family Model t where
            Model Z         = Int
            Model (Fun a b) = T (Model a) -> T (Model b)
            Model Unit      = One

-- model contexts as products in our base category, with T on
-- each model variable assumption
type family ModelContext gam where
            ModelContext () = ()
            ModelContext (gam, a) = (ModelContext gam, T (Model a))

-- Denotational model as a morphism in our base category
model :: Lambda gam t -> (ModelContext gam -> T (Model t))

-- Semantics of core lambda calculus

model Var =
   -- Variables by projection
   snd

model (App e1 e2) =
   -- Inductive steps
  (model e1 `pair` model e2)
   -- Prioritise effects of the left expression (the function)
 >>> strengthL
   -- Apply the function
 >>> fmap app
   -- Sequential compose the effects of the left-hande side and the
   -- resulting expression after substitution
 >>> mu

model (Abs e) =
   -- Transfer an assumption to the parameter of an exponent
   lam (model e)
   -- Wrap in trivial effect because lambdas have no side effects
 >>> eta

-- Semantics of additional sequential composition

model (Let e1 e2) =
   (id `pair` model e1)
   -- Prioritise effects of first expression
  >>> strengthR
   -- then prmote the pure value to trivially effectful
  >>> fmap (id `cross` eta)
   -- substitute into the body of the 'let'
  >>> fmap (model e2)
   -- sequentially compose the effects of the first expression and the substited
   -- body
  >>> mu

-- Semantics of structural rules

model (Perm c e) = modelPerm c >>> model e

-- Semantics of extra bits

model Bing =
   const (putStrLn "Bing")

model Bong =
   const (putStrLn "Bong")

model (Const x) =
   const (eta x)

model (Plus e1 e2) =
   (model e1 `pair` model e2)
   -- Prioritisse effects of the left of a +
 >>> strengthL
 >>> fmap strengthR
   -- Sequentially compose effects of left with effects of right
 >>> mu
   -- Actually do the addition
 >>> fmap (uncurry (+))

-- model of explicit structural rules (context permutations)
modelPerm :: Perm gam' gam -> (ModelContext gam' -> ModelContext gam)
modelPerm Weaken    (gam, _)      = gam
modelPerm Contract  (gam, a)      = ((gam, a), a)
modelPerm Exchange  ((gam, a), b) = ((gam, b), a)
modelPerm (Congruence s) (gam, a) = (modelPerm s gam, a)


-----------------------------------------
-- Some examples

-- (\x -> x + x) (let z = bing in y)
example :: Lambda ((), Z) Z
example = App (Abs (Plus Var Var)) (Let Bing (Perm Exchange Var))

-- > model example ((), eta 42)
-- Bing
-- Bing
-- 84

-- (\x -> x + (y + x)) (let z = bing in y)
example2 :: Lambda ((), Z) Z
example2 = App (Abs (Plus Var (Plus (Perm Exchange Var) Var))) (Let Bing (Perm Exchange Var))

-- > model example2 ((), eta 42)
-- Bing
-- Bing
-- 126

-- x + (y + z)
example0 :: Lambda ((((), Z), Z), Z) Z
example0 = Plus Var (Plus (Perm Exchange Var) (Perm Weaken (Perm Exchange Var)))

-- > model example0 ((((), eta 1), eta 4), eta 9)
-- 14

-- (\z -> x + (y + z)) (let a = bong in 10)
example3 :: Lambda (((), Z), Z) Z
example3 = App (Abs (Perm Exchange (Perm (Congruence Exchange) (Plus Var (Plus (Perm Exchange Var) (Perm Weaken (Perm Exchange Var)))))))
             (Let Bong (Const 10))

-- > model example3 (((), eta 5), eta 7)
-- Bong
-- 22

main :: IO Int
main = model example ((), eta 42)