Skip to content

Instantly share code, notes, and snippets.

Last active November 4, 2022 04:41
What would you like to do?
Non-deterministic normalization-by-evaluation in Olle Fredriksson's flavor.
{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:
The main idea is that during elaboration, we need different evaluation
strategies for different tasks; here in particular we have a distinction
between top and local scope, and we want to have control over unfolding
of top-level definitions.
- For generating terms (for error displaying, serialization, metavariable
solutions), we want to avoid unfolding as much as possible, to avoid size
- For conversion checking, we want to have an efficient, preferably call-by-need
evaluator which unfolds everything.
We want evaluation to be as fast as possible, and we also want to avoid
duplicating computation between the two unfolding modes which could be shared.
The solution here is to use normalization-by-evaluation extended with
lazy non-deterministic choice in the semantic domain. We extend values with
... | VTop Name Spine ~Val
where Name and Spine constitute a neutral expression whose head is a top-level
definition name, and ~Val is the lazy result of evaluating the same netural
expression, but with the top definition unfolded.
Hence, when we hit VTop during processing Val-s, we can choose between
unfolding and not unfolding.
We also have to implement the semantic action of projections and eliminations
on VTop. In our case, we only have function application:
vapp :: Val -> Val -> Val
vapp (VLam _ t) ~u = t u
vapp (VLoc x sp) ~u = VLoc x (SApp sp u)
vapp (VTop x sp t) ~u = VTop x (SApp sp u) (vapp t u)
vapp acts on both branches of VTop. The neutral part is eagerly computed,
since the computation there is trivial, delaying it would be more costly
than just performing it. In contrast, the "vapp t u" can be arbitrarily costly,
so it is delayed.
Note that "u" is duplicated in "VTop x (SApp sp u) (vapp t u)". This means
that "u" is computed at most once regardless of which evaluation branch we
compute (of course, we can compute both too).
import Data.Maybe
type Name = String
data Tm
= Loc Name -- local var
| Top Name -- top-level var
| App Tm Tm
| Let Name Tm Tm
| Lam Name Tm
deriving Show
data Spine = SNil | SApp Spine ~Val
data Val = VLam Name (Val -> Val) | VLoc Name Spine | VTop Name Spine ~Val
type TopEnv = [(Name, Val)]
type LocalEnv = [(Name, Val)]
eval :: TopEnv -> LocalEnv -> Tm -> Val
eval top loc = \case
Loc x -> fromJust $ lookup x loc
Top x -> VTop x SNil (fromJust $ lookup x top)
App t u -> vapp (eval top loc t) (eval top loc u)
Let x t u -> eval top ((x, eval top loc t) : loc) u
Lam x t -> VLam x \u -> eval top ((x, u):loc) t
vapp :: Val -> Val -> Val
vapp (VLam _ t) ~u = t u
vapp (VLoc x sp) ~u = VLoc x (SApp sp u)
vapp (VTop x sp t) ~u = VTop x (SApp sp u) (vapp t u)
fresh :: LocalEnv -> Name -> Name
fresh env x = case lookup x env of
Nothing -> x
Just{} -> fresh env (x ++ "'")
type UnfoldTop = Bool
quoteSp :: LocalEnv -> UnfoldTop -> Tm -> Spine -> Tm
quoteSp loc unf h = \case
SNil -> h
SApp sp u -> App (quoteSp loc unf h sp) (quote loc unf u)
quote :: LocalEnv -> UnfoldTop -> Val -> Tm
quote loc unf = \case
VLoc x sp -> quoteSp loc unf (Loc x) sp
VLam x t -> let x' = fresh loc x
v = VLoc x' SNil
in Lam x' (quote ((x, v):loc) unf (t v))
VTop x sp t -> if unf then quote loc unf t
else quoteSp loc unf (Top x) sp
evalTop :: [(Name, Tm)] -> Tm -> Val
evalTop top t = eval topvals [] t where
topvals = foldl (\top (x, t) -> (x, eval top [] t) : top) [] top
nfTop :: UnfoldTop -> [(Name, Tm)] -> Tm -> Tm
nfTop unf top t = quote [] unf (evalTop top t)
($$) = App
infixl 8 $$
top :: [(Name, Tm)]
top = [
("zero", Lam "s" $ Lam "z" $ Loc "z")
, ("suc", Lam "n" $ Lam "s" $ Lam "z" $
Loc "s" $$ (Loc "n" $$ Loc "s" $$ Loc "z"))
, ("add", Lam "a" $ Lam "b" $ Lam "s" $ Lam "z" $
Loc "a" $$ Loc "s" $$ (Loc "b" $$ Loc "s" $$ Loc "z"))
, ("mul", Lam "a" $ Lam "b" $ Lam "s" $ Lam "z" $
Loc "a" $$ (Loc "b" $$ Loc "s") $$ Loc "s" $$ Loc "z")
, ("5", Top "suc" $$ (Top "suc" $$ (Top "suc" $$ (Top "suc" $$
(Top "suc" $$ Top "zero")))))
, ("10", Top "add" $$ Top "5" $$ Top "5")
, ("100", Top "mul" $$ Top "10" $$ Top "10")
tm = Let "five" (Top "suc" $$ (Top "suc" $$ (Top "suc" $$ (Top "suc" $$
(Top "suc" $$ Top "zero"))))) $
Top "mul" $$ Loc "five" $$ Top "5"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment