PHOAS Call-by-push-value... Kind of!

CBPV.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE LambdaCase #-}

-- Code obviously based on <http://andrej.com/plzoo/html/levy.html>

-- This is right now *not really* CBPV. In particular, the Rec binder
-- is both less well-behaved and far more complex than it ought to
-- be. Instead of passing a computation back (which should never be
-- possible as variables do not have computation types) it should pass
-- back a thunk.
--
-- But I'm a little hesitant to change it because this is a very
-- pretty example of PHOAS with two differently typed binders.

module CBPV where

import Control.Applicative
import Control.Monad

data Vty
  = TInt
  | TBool
  | TForget Cty
  deriving ( Eq, Show )

data Cty
  = TFree Vty
  | TArr Vty Cty
  deriving ( Eq, Show )

data Valf c v 
  = Var   v
  | Int   Int
  | Bool  Bool
  | Times (Valf c v) (Valf c v)
  | Plus  (Valf c v) (Valf c v)
  | Minus (Valf c v) (Valf c v)
  | Equal (Valf c v) (Valf c v)
  | Less  (Valf c v) (Valf c v)
  | Thunk (Compf v c)

data Compf v c
  = Self c
  | Force (Valf c v)
  | Return (Valf c v)
  | To (Compf v c) (v -> Compf v c)
  | Let (Valf c v) (v -> Compf v c)
  | If (Valf c v) (Compf v c) (Compf v c)
  | Abs Vty (v -> Compf v c)
  | App (Compf v c) (Valf c v)
  | Rec Cty (c -> Compf v c)
  | Then (Compf v c) (Compf v c)

newtype Val  = Val  { runVal  :: forall c v . Valf  c v }
newtype Comp = Comp { runComp :: forall c v . Compf v c }

--------------------------------------------------------------------------------

type VCtx = forall c v. Valf  c v -> Valf  (Compf v c) (Valf c v)
type CCtx = forall c v. Compf v c -> Compf (Valf c v)  (Compf v c)

substV :: VCtx -> (Val -> Val)
substV f (Val v) = Val (squashV (f v))

substC :: CCtx -> (Comp -> Comp)
substC f (Comp c) = Comp (squashC (f c))

squashV :: Valf (Compf v c) (Valf c v) -> Valf c v
squashV x = case x of
  Var v     -> v
  Int i     -> Int i
  Bool b    -> Bool b
  Times l r -> Times (squashV l) (squashV r)
  Plus  l r -> Plus  (squashV l) (squashV r)
  Minus l r -> Minus (squashV l) (squashV r)
  Equal l r -> Equal (squashV l) (squashV r)
  Less  l r -> Less  (squashV l) (squashV r)
  Thunk c   -> Thunk (squashC c)

squashC :: Compf (Valf c v) (Compf v c) -> Compf v c
squashC x = case x of
  Self   c -> c
  Force  v -> Force  (squashV v)
  Return v -> Return (squashV v)
  To  c f  -> To  (squashC c) (\v -> squashC (f (Var v)))
  Let v f  -> Let (squashV v) (\v -> squashC (f (Var v)))
  If c t e -> If (squashV c) (squashC t) (squashC e)
  Abs ty f -> Abs ty (\v -> squashC (f (Var v)))
  App c v  -> App (squashC c) (squashV v)
  Rec ty f -> Rec ty (\c -> squashC (f (Self c)))
  Then l r -> Then (squashC l) (squashC r)

--------------------------------------------------------------------------------

typeOfV :: Val  -> Maybe Vty
typeOfV = typeOfVf . runVal

typeOfC :: Comp -> Maybe Cty
typeOfC = typeOfCf . runComp

typeOfVf :: Valf Cty Vty -> Maybe Vty
typeOfVf x = case x of
  Var v     -> return v
  Int _     -> return TInt
  Bool _    -> return TBool
  Times l r -> do
    TInt <- typeOfVf l
    TInt <- typeOfVf r
    return TInt
  Plus l r -> do
    TInt <- typeOfVf l
    TInt <- typeOfVf r
    return TInt
  Minus l r -> do
    TInt <- typeOfVf l
    TInt <- typeOfVf r
    return TInt
  Equal l r -> do
    TInt <- typeOfVf l
    TInt <- typeOfVf r
    return TBool
  Less l r -> do
    TInt <- typeOfVf l
    TInt <- typeOfVf r
    return TBool
  Thunk c ->
    TForget <$> typeOfCf c

typeOfCf :: Compf Vty Cty -> Maybe Cty
typeOfCf x = case x of
  Self c   -> return c
  Force v  -> do
    TForget cty <- typeOfVf v
    return cty
  Return v -> TFree <$> typeOfVf v
  To c f -> do
    TFree vty <- typeOfCf c
    typeOfCf (f vty)
  Let v f -> do
    vty <- typeOfVf v
    typeOfCf (f vty)
  If c t e -> do
    TBool <- typeOfVf c
    ctyt  <- typeOfCf t
    ctye  <- typeOfCf e
    guard (ctyt == ctye)
    return ctyt
  Abs vty f -> TArr vty <$> typeOfCf (f vty)
  App c v -> do
    TArr vtyExp resTy <- typeOfCf c
    vty <- typeOfVf v
    guard (vtyExp == vty)
    return resTy
  Rec cty f -> do
    typeOfCf (f cty)
  Then c1 c2 -> do
    typeOfCf c1
    typeOfCf c2

--------------------------------------------------------------------------------

interpV :: Val -> Run
interpV = interpVf . runVal

interpC :: Comp -> Run
interpC = interpCf . runComp

data Run
  = VInt   Int
  | VBool  Bool
  | VThunk (Compf Run Run)
  | VFun   (Run -> Compf Run Run)
  | VRet   Run

instance Show Run where
  show r = case r of
    VInt   i -> show i
    VBool  b -> show b
    VThunk _ -> "<<thunk>>"
    VFun   _ -> "<<func>>"
    VRet   r -> "ret { " ++ show r ++ " }"

interpVf :: Valf Run Run -> Run
interpVf x = case x of
  Var r    -> r
  Int i    -> VInt i
  Bool b   -> VBool b
  Thunk c  -> VThunk c
  Times l r ->
    let VInt li = interpVf l
        VInt ri = interpVf r
    in VInt (li * ri)
  Plus l r ->
    let VInt li = interpVf l
        VInt ri = interpVf r
    in VInt (li + ri)
  Minus l r ->
    let VInt li = interpVf l
        VInt ri = interpVf r
    in VInt (li - ri)
  Equal l r ->
    let VInt li = interpVf l
        VInt ri = interpVf r
    in VBool (li == ri)
  Less l r ->
    let VInt li = interpVf l
        VInt ri = interpVf r
    in VBool (li < ri)

interpCf :: Compf Run Run -> Run
interpCf x = case x of
  Self r -> r
  Abs _ f -> VFun f
  If c t e ->
    let VBool bb = interpVf c
    in if bb
       then interpCf t
       else interpCf e
  App e1 e2 ->
    let VFun f = interpCf e1
    in interpCf (f (interpVf e2))
  Let v f -> interpCf (f (interpVf v))
  To c f ->
    let VRet v = interpCf c
    in interpCf (f v)
  Return v -> VRet (interpVf v)
  Force v ->
    let VThunk c = interpVf v
    in interpCf c
  Rec _ f ->
    let c = interpCf (f c)
    in c
  Then c1 c2 ->
    case interpCf c1 of
      VRet r -> VRet r
      _      -> interpCf c2

--------------------------------------------------------------------------------

fact :: Compf v c
fact =
  Rec (TArr TInt (TFree TInt)) $ \fact ->
    Abs TInt $ \n ->
      If (Less (Var n) (Int 1))
         (Return (Int 1))
         (To (App (Self fact) (Minus (Var n) (Int 1)))
             (\v -> Return (Times (Var v) (Var n))))


-- λ> typeOfCf fact
-- Just (TArr TInt (TFree TInt))