Notes on normalization-by-evaluation modulo monad laws for monadic language

MonadicNbE.hs

{-

-- Compiler: staging, memory layout control, etc  (small + self-hosting + useful soon)

-- Surface language:
   1. CBV + side effects (ML)
   2. CBV + typed effect system:
        - Eff monad
        - Eff monad, row of effects
           f : Int -> Eff [IO, Exc e, MutRef a, MutRef b] Int
        - (extensible / algebraic / resumable effect handlers)


-- Intermediate language:

Assume CBV + printing

   pure language:       admissible substitution (beta-reduce, inline, delta-contraction (CSE))
   effectful language:  doesn't work

   issue: partial evaluation + effects: don't work together
          (effectful things cannot be substituted, (reordered, dropped))

   - effects are in a monad
      - GHC doesn't have a monad in Core, uses token passing to compile IO
         - unsound
         - only linear token-passing models (some) IO
              State hack, runST performance, unsafeInlineIO, ...
              (mandatory late inlining runST, runRW# etc.)


1. Monad in core for everything which is effectful  (M)
   - guarantees: partial eval + NBE still works, conversion checking modulo laws (efficiently, and in a sound way)
   - I don't know anything about the intension of my effects

   Optimization: could be State transformer (locally)

      finite number of mutable locations used in lexical

   put x; get     ~ pure x
   put x; put x;  ~ put x

   throw e; e2 ~ throw e

   limitation of usual State monad: (ST has stronger interface than State)
          - I formalized ST monad in Agda: (requires parametricity to prove heap well-typed)

       refs : List (MutRef Int)
       n    : Int

       do
         write (lookup n refs) 100
         f refs foo bar             -- out-of-line call
                                    -- erase all info in symbolic state

       -- ("symbolic" state,    lookup n refs ↦ 100)

   Exceptions:
      -- something similar

   Call-by-need:
     implementation: CBV + Eff + mutable refs

     interface for call-by-need:

         Lazy  : Type -> Type
         delay : A -> Eff (Lazy A)
                            (delay foo, delay foo)   =/   let x = delax foo in (x, x)
                            "strengthening for delay" : (let x = delay foo in e) ~ e    if   x ∉ FV(e)

         force : Lazy A -> IO A
         result : A -> Lazy A        -- returns an already force value  (useful for compiler opt)

Stuff I looked at:

  - 97: partial eval with side effects     (monadic translation) ("preactions")

   - administrative normal form only for effectful computations
     (monadic program: the same thing!)


   res <- f (g(x, y), h(y, z))
   ...

       to

   res1 <- g(x, y)
   res  <- f (res1, h(y, z))
   ...

   x <- foo
   y <- x

   f

     surface (f : () -> Int)   --->   f : () -> M Int
     let f() = print "foo"
     f();
     f();


  CBV monadic translation:
    - limitation: unknown functions are always monadic

  higher-order function:

    comp : (B -> C) -> (A -> B) -> A -> C
    comp f g x = f (g x)

    comp : (B -> M C) -> (A -> M B) -> A -> M C
    comp f g x = do
      gx <- g x
      f gx

   annoying with curried unknown functions


   foo : (Int -> Int -> Int) -> (Int, Int)
   foo f = (f 0 1, f 0 2)

   foo' : (Int -> Int -> Int) -> (Int, Int)
   foo' f = let f0 = f 0 in (f0 1, f0 2)

   foo : (Int -> M (Int -> M Int)) -> M (Int, Int)
   foo f = do
     f0 <- f 0
     f01 <- f0 1
     f0' <- f 0
     f02 <- f0' 2
     return (f01, f02)

   -- cheating : assume that unknown functions are only M in the return type

   foo : (Int -> Int -> M Int) -> M (Int, Int)
   foo f = do
     f01 <- f 0 1
     f02 <- f 0 2
     return (f01, f12)

   -- not the same program!

   foo : (Int -> Int -> M Int) -> M (Int, Int)
   foo f = do
     let f0 = f 0;
     f01 <- f0 1
     f02 <- f0 2
     return (f01, f12)

  -- CBV --> monadic   (optimize unknown function calls?)
  --                   (just write functions from tuples to result?)

  --  (use n-ary function in surface language, but allow partial application via currying subtyping)

  --  (+) : (Int, Int) -> Int
  --  (+) 10 : Int -> Int           --> elaborated to \y -> (+) (10, y)

   surface: foo : ((Int, Int) -> Int) -> (Int, Int)
   monadic: foo : ((Int, Int) -> M Int) -> M (Int, Int)

            foo f = let f0 = f 0 in (f0 1, f0 1)
      elab: foo f = let f0 = \y. f (0, y) in (f0 1, f0 2)


CBPV (call-by-push-value)

   - point: combine effects + by-value + by-name
      - lots of noise arising from CBV and CBN (by-name!)
      - by-name is practically useless!

   - Extended CBPV : extending CBPV with call-by-need evaluation

   CBV (by default) + effects + some delimited call-by-need



Intermediate lang, opt, PE, side effects, monadic, CBPV, CBPVE, subst
Surface lang: monadic or plain cbv,
monadic thunks
deeply embedded monadic effect for PR

-}


{-# language Strict, LambdaCase, BangPatterns, ViewPatterns, BlockArguments,
             EmptyCase, OverloadedStrings #-}

{-# options_ghc -Wincomplete-patterns #-}

import Data.Maybe
import Data.String

{-
First: monadic term language + effect + NbE + conversion checking

   - normal forms modulo monad laws
   - conversion checking with definitional monad laws

     - potential issue: "quadratic binding"  (Haskell: CPS)

  - conversion checking for monadic expressions?
    - dep. typed language + M : we need conversion checking (unification etc)
    - simply typed language + M + dependently typed static stage language (prove equality of runtime expressions)
       (lots of research questions about proving equality of runtime programs in static stage)

-}


-- "untyped" language
-- typed, just don't have types

type Name = String

data Tm
  = Var Name
  | App Tm Tm
  | Lam Name Tm
  | Let Name Tm Tm
  | Bind Name Tm Tm       -- monadic bind
  | Return Tm             -- monadic return
  | Hello                 -- Hello : M ()
  | Tt                    -- Tt : Unit
  deriving (Eq, Show)

data Val
  = VVar Name
  | VApp Val Val
  | VLam Name (Val -> Val)
  | VBind Name Val (Val -> Val)
  | VReturn Val
  | VHello
  | VTt

type Env = [(Name, Val)]

-- open evaluation of programs, performs pure computation, keeps effects in the same order
--------------------------------------------------------------------------------

vVar :: Env -> Name -> Val
vVar e x = fromJust $ lookup x e

vApp :: Val -> Val -> Val
vApp t u = case t of
  VLam _ t -> t u
  t        -> VApp t u

vBind :: Name -> Val -> (Val -> Val) -> Val
vBind x t u = case t of
  VReturn t    -> u t
  VBind y t t' -> vBind y t (\vy -> vBind x (t' vy) u)
  t            -> VBind x t u

eval :: Env -> Tm -> Val
eval e = \case
  Var x      -> vVar e x
  App t u    -> vApp (eval e t) (eval e u)
  Lam x t    -> VLam x (\vx -> eval ((x, vx):e) t)
  Let x t u  -> case eval e t of t -> eval ((x, t):e) u
  Bind x t u -> vBind x (eval e t) (\vx -> eval ((x, vx):e) u)
  Return t   -> VReturn (eval e t)
  Hello      -> VHello
  Tt         -> VTt

fresh :: [Name] -> Name -> Name
fresh ns "_" = "_"
fresh ns x | elem x ns = fresh ns (x ++ ",")
           | otherwise = x

quote :: [Name] -> Val -> Tm
quote ns = \case
  VVar x                    -> Var x
  VApp t u                  -> App (quote ns t) (quote ns u)
  VLam (fresh ns -> x) t    -> Lam x (quote (x:ns) (t (VVar x)))
  VBind (fresh ns -> x) t u -> case quote (x:ns) (u (VVar x)) of
                                 Return (Var x') | x == x' -> quote ns t
                                 u                         -> Bind x (quote ns t) u
  VReturn t                 -> Return (quote ns t)
  VHello                    -> Hello
  VTt                       -> Tt

nf0 :: Tm -> Tm
nf0 = quote [] . eval []

instance IsString Tm where fromString = Var


-- Execution only for closed values with type IO a
--------------------------------------------------------------------------------

infixr 4 >>>
(>>>) :: Tm -> Tm -> Tm
t >>> u = Bind "_" t u

-- closed value, with (M a) type
exec :: Val -> IO Val
exec = \case
  VReturn t   -> pure t
  VBind x t u -> do {t <- exec t; exec (u t)}
  VHello      -> VTt <$ putStrLn "hello"
  _           -> undefined

run :: Tm -> IO Val
run = exec . eval []

test1 =
  nf0 ((((((Hello >>> Hello) >>> Hello) >>> Hello) >>> ((Hello >>> Hello) >>> Hello)) >>> Hello) >>> Hello)
  ==
  (Hello >>> Hello >>> Hello >>> Hello >>> Hello >>> Hello >>> Hello >>> Hello >>> Hello)