Permalink
Switch branches/tags
Find file Copy path
39b6be3 Dec 8, 2018
1 contributor

Users who have contributed to this file

719 lines (581 sloc) 29.5 KB
{-
Smalltt: minimal dependent TT implementation, intended as a demo for
high-performance elaboration. This file showcases basic language features and
contains a number of benchmarks. There is an Agda file called "Demo.agda" in
this repo, which mirror the contents of this file, for benchmarking purposes.
Installation, usage:
- install stack: https://docs.haskellstack.org/en/stable/README/
- install smalltt with "stack install" in this directory
- if you have LLVM installed, you should do "stack install --ghc-options="-fllvm"",
it gives a significant speed boost.
- make sure stack bin directory is on PATH
- hit "smalltt" in a directory with .stt files
Performance improvements over Coq/Agda should be both in constant factors and,
in many cases, asymptotics.
The asymptotic improvement results from smalltt's ability to efficiently compute
small solutions to metavariables, avoiding both classic exponential
Hindley-Milner blowups and the very frequent quadratic blowups resulting from
dependent type indexing. A simple example for the latter is length-indexed
vectors, where the implicit natural number indices make normal forms of vector
expressions quadratic-sized in the length.
Project is very WIP, implementation is ugly, CLI is crap and error reporting
is currently trash. Source locations in errors are also bugged out.
Although there are lots of unimplemented optimizations currently, the system is
already *very* fast. This file is elaborated in 43 ms on my system, and if we
remove the crazier "vecStress" and "t1" definitions, this goes down to *1* ms.
I have done preliminary (informal, manual) bechmarking comparing raw evaluation
and conversion performance and asymptotics to Agda, Coq and GHC. You can find
result and benchmarks scattered in this file. It's a TODO to make benchmarking
more automated. You can find Agda and Coq files used for benchmarking in the
"bench" directory.
Benchmarking setup:
- smalltt is compiled with GHC 8.6.2, -O2 -fllvm
- GHC 8.6.2 is likewise used for GHC/GHCI benchmarks.
- Coq 8.8.2 for Coq, with -type-in-type
- Agda 2.6.0 master built in 2018 september is used for Agda,
again with --type-in-type
- Timings and memory usage come from "time" util and process monitoring.
- System: Core i7 3770, 8GB RAM, Ubuntu 16.04
Note: smalltt does not serialize elaboration output, it just generates core
terms for all definitions. In contrast, Agda writes interface files and also
does hash-consing on it. Although we compare apples and oranges, the results are
still informative (with a fair number of out-of-memory vs. instant checking
cases). Also, I don't expect serialization to add much to elaboration time in
smalltt in the future; in particular I'll keep serialization simple and markedly
won't do hash consing (because keeping output small should be the job of
elaboration itself).
A particularly nice thing about our system is that the standard evaluator (which
despite being a "glued" AST interpter is about a third as fast as the Coq
bytecode VM!) is actually the sole default evaluator: there no is separate
"slow" and "fast" evaluator as in Agda and Coq. In Agda and Coq the "fast"
evaluators are not available for terms which contain unsolved metavariables,
which is a pretty large limitation. In smalltt, the default evaluator is used
everywhere, regardless of metas, and there are no fundamental limitations which
would prevent it from being even faster, or it being based on bytecode or
machine code.
As the current system stands, unification is already remarkably usable but
weaker than in Agda. We just have pattern unification, bidirectional elaboration
and function eta, without pruning or postponing, and we also just ignore
nonlinearity in patterns, following the Coq school of picking the innermost
nonlinear bound variables.
Eventually I would like to have approximate unification parity with Agda, but I
would really prefer to *not* have postponing (a major source of headache), while
also avoiding performance regression. My plans for this:
- Have features which work without postponing in any case:
- pruning
- intersections
- eta-contraction in patterns,
- eta-expanding metas (starts to make sense once we have unit and sigmas)
- Have slightly "evil" features which cut down on the need for postponing.
- ignore nonlinear patterns, always bind innermost nonlinear variable
- (I intuit from some testing experience that this is what we mostly want in
practice, also Coq does the same thing AFAIK)
- erasing dependencies on non-variable pattern entries. By Agda standards, this
is just plain evil.
-}
-- Basics
--------------------------------------------------------------------------------
-- We have type-in-type:
typeInType : U = U
{-
- There is a distinguished top level scope, local definitions
can be written like "let x : A = t in u" or "let x = t in u".
- Name shadowing is allowed everywhere.
-}
-- polymorphic identity, A has inferred type U
id : {A} → A → A = λ x. x
-- by default metas are inserted for implicit arguments, but
-- (!) can be used to stop insertion at any point. The (id!) expression
-- has a polymorphic type, {A} → A → A
id2 : {A} → A → A = id (id!)
id3 : {A} → A → A = λ x. id x
-- non-unicode arrow and lambda are usable as well:
id4 : {A} -> A -> A = \x. x
-- explicit id function can be used for type annotation
-- as in Idris
the : (A : _) → A → A = λ _ x. x
-- top-level definition types can be omitted
constTy = {A B} → A → B → A
const : constTy = λ x y. x
-- implicit application follows Agda convention.
namedArgTest = const {B = U} U
namedArgTest2 = the constTy (λ x y. x) {B = U} U
-- the following has inferred type {B : U} → U → B → U
-- because of (!)
constU = const {U} !
-- Church bools
--------------------------------------------------------------------------------
Bool = (B : U) → B → B → B
true : Bool = λ _ t f. t
false : Bool = λ _ t f. f
and : Bool → Bool → Bool
= λ b1 b2. b1 Bool true b2
-- Church natural numbers
--------------------------------------------------------------------------------
Nat : U
= (n : U) → (n → n) → n → n
zero : Nat
= λ n s z. z
suc : Nat → Nat
= λ a n s z. s (a n s z)
n2 : Nat = λ n s z. s (s z)
n5 : Nat = λ n s z. s (s (s (s (s z))))
mul : Nat → Nat → Nat
= λ a b n s z. a n (b n s) z
add : Nat → Nat → Nat
= λ a b n s z. a n s (b n s z)
n10 = mul n2 n5
n10b = mul n5 n2
n100 = mul n10 n10
n100b = mul n10b n10b
n10k = mul n100 n100
n10kb = mul n100b n100b
n100k = mul n10k n10
n100kb = mul n10kb n10b
n1M = mul n10k n100
n1MB = mul n10kb n100b
n10M = mul n1M n10
n10MB = mul n1MB n10b
n100M = mul n10M n10
n200M = mul n2 n100M
-- Church lists
--------------------------------------------------------------------------------
List : U → U = λ a. (l : U) → (a → l → l) → l → l
lnil : {a} → List a = λ l c n. n
lcons : {a} → a → List a → List a = λ a as l c n. c a (as l c n)
list1 = lcons true (lcons false (lcons false lnil))
map : {a b} → (a → b) → List a → List b
= λ f as l c. as l (λ a. c (f a))
-- Church vectors
--------------------------------------------------------------------------------
Vec : U → Nat → U
= λ a n. (V : Nat → U) → V zero → ({n} → a → V n → V (suc n)) → V n
vnil : {a} → Vec a zero
= λ V n c. n
vcons : {a n} → a → Vec a n → Vec a (suc n)
= λ a as V n c. c a (as V n c)
vec1 = vcons true (vcons false (vcons true vnil))
-- Note: putting [elaborate] after a top-level name will cause
-- elaboration time for that entry to be displayed on load.
-- Type checking vecStress:
-- smalltt : 3.8ms , 6.3 MB
-- Coq : 300ms , 280 MB
-- Agda : ~3s , 330 MB
vecStress [elaborate] =
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
(vcons true (vcons true
vnil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))
-- Leibniz (Church) propositional equality, useful for testing conversion.
-- Also note the implicit lambdas.
----------------------------------------------------------------------------------
Eq : {A} → A → A → U
= λ {A} x y. (P : A → U) → P x → P y
refl : {A}{x : A} → Eq x x
= λ P px. px
trans : {A}{x y z : A} → Eq x y → Eq y z → Eq x z
= λ {x = x} p q. q _ p
sym : {A}{x y : A} → Eq x y → Eq y x
= λ {x = x}{y} p. p (λ y. Eq y x) refl
ap : {A B}(f : A → B){x y : A} → Eq x y → Eq (f x) (f y)
= λ f {x}{y} p. p (λ y. Eq (f x) (f y)) refl
-- Pairs, Top, Bot
--------------------------------------------------------------------------------
Pair : U → U → U
= λ A B. (Pair : U)(pair : A → B → Pair) → Pair
pair : {A B} → A → B → Pair A B
= λ a b Pair pair. pair a b
proj1 : {A B} → Pair A B → A
= λ p. p _ (λ x y. x)
proj2 : {A B} → Pair A B → B
= λ p. p _ (λ x y. y)
Top : U
= (Top : U)(tt : Top) → Top
tt : Top
= λ Top tt. tt
Bot : U
= (Bot : U) → Bot
-- Dependent function composition (higher-order unification example)
--------------------------------------------------------------------------------
comp :
{A}
{B : A → U}
{C : {a} → B a → U}
(f : {a}(b : B a) → C b)
(g : (a : A) → B a)
(x : A)
→ C (g x)
= λ f g a. f (g a)
compTest1 : Nat → Nat
= comp suc suc
compTest2 : {m A} → A → Vec A m → Vec A (suc (suc m))
= λ a. comp (vcons a) (vcons a)
-- Some stress tests
--------------------------------------------------------------------------------
-- computing an N-sized function type for testing purposes
nfun : Nat → U
= λ n. n U (λ A. U → A) U
-- Tests for approximate equality, i.e. the ability to tell terms equal
-- without fully reducing them.
-- smalltt : approx check succeds
-- Coq : approx check succeds
-- Agda : approx check fails
synEqTest1 [elaborate] : nfun n10k → nfun n10k = λ x. x
-- Coq : approx check succeeds
-- Agda : approx check succeeds
-- smalltt : approx check fails
synEqTest2 [elaborate] : Eq n1M n1M = refl
{- I note: approx check failed above in smalltt because of the following: the
inferred type of refl is Eq {?1} ?2 ?2, we need to unify (Eq {?1} ?2 ?2) with
(Eq {Nat} n1M n1M). smalltt then tries to approximately ("locally") unify the
two spines, but gets stuck, because it doesn't know that Eq is generative,
and refuses to solve metas when unifying the spines to avoid losing possible
solutions. So smalltt switches to full conversion check, thereby forcing
n1M. Coq on the other hand is happy to take approximate solutions.
Of course, if Eq were defined as a rigid type constructor, there wouldn't be
an issue. I demonstrate this in the next benchmark below.
Alternatively, we could try to do injectivity/generativity analysis on
definitions, which I suspect would be a good thing overall.
I prefer to not use the Coq solution, nor any backtracking or non-trivially
bounded unfolding in approximate conversion check. A key principle of my
approximate conversion checker is to not do significant computation, because
that's effectively call-by-name and without any sharing. Hence, I give up
approximate checks relatively quickly and bring in the heavy-duty
call-by-need machine.
At this stage, it's only a conjecture that this approach is faster than Coq
in practice; we need more and larger benchmarks. It will be, however, much
easier to compare performance of Coq-style approximate checking with
smalltt-style, if both are implemented in smalltt, because a Coq-smalltt
comparison would be too muddled by asymptotic differences.
-}
-- approximate equality works in smallt if Eq is postulated:
assume Eq2 : {A} → A → A → U
assume refl2 : {A x} → Eq2 {A} x x
-- smalltt : approx check succeeds
-- Agda : approx check succeeds
-- Coq : approx check succeeds
synEqTest3 [elaborate] : Eq2 n1M n1M = refl2
-- Classic examples for exponential-time Hindley-Milner checking.
--------------------------------------------------------------------------------
-- Suprisingly, Agda-2018-sept manages the following fine, although in 2018-jan
-- it also failed.
-- smalltt: instant
-- Agda : instant
-- Coq : doesn't finish
idStress [elaborate] : {A} → A → A
= id id id id id id id id id id id id id id id id id id id id
id id id id id id id id id id id id id id id id id id id id
-- smalltt : instant
-- Agda : doesn't finish
-- Coq : doesn't finish
pairStress [elaborate] : Top
= let x0 = pair tt tt in
let x1 = pair x0 x0 in
let x2 = pair x1 x1 in
let x3 = pair x2 x2 in
let x4 = pair x3 x3 in
let x5 = pair x4 x4 in
let x6 = pair x5 x5 in
let x7 = pair x6 x6 in
let x8 = pair x7 x7 in
let x9 = pair x8 x8 in
let x10 = pair x9 x9 in
let x11 = pair x10 x10 in
let x12 = pair x11 x11 in
let x13 = pair x12 x12 in
let x14 = pair x13 x13 in
let x15 = pair x14 x14 in
let x16 = pair x15 x15 in
let x17 = pair x16 x16 in
let x18 = pair x17 x17 in
let x19 = pair x18 x18 in
let x20 = pair x19 x19 in
tt
-- Raw compute performance
--------------------------------------------------------------------------------
-- A simple way to force a Church Nat.
forceNat : Nat → Bool
= λ n. n _ (λ x. x) true
-- Note: [normalize] prints normalization time for definition on load
-- GHC -O2 -fllvm : 14ms , 0 MB
-- Coq (Eval vm_compute) : 0.23s , 82 MB
-- smalltt : 0.53s , 6.3 MB
-- runghc : 1.1s , 22 MB
-- Coq (Eval cbv) : 1.1s , 270 MB
-- Coq (Eval lazy) : 2.8s , 290 MB
-- Agda : ~5.5s , ~635 MB
-- Coq (Eval native_compute) : compilation failure
compute10M [normalize] = forceNat n10M
-- Lazy/call-by-need evaluation
--------------------------------------------------------------------------------
-- smalltt : instantly normalized
-- Agda : instantly normalized
-- Coq (Eval lazy) : instantly normalized
lazyU = const U (forceNat n10M)
-- call-by-need local definitions
-- local cbn works if "localCBN n10" runs roughly as fast as
-- "forceNat (mul n10 n100k)"
localCBN : Nat → Bool
= λ n. let m = forceNat (mul n n100k) in
n _ (λ b. and m b) true
-- smalltt : local cbn works
-- Coq (Eval lazy) : local cbn works
-- Agda : local cbn works
cbnReference [normalize] = forceNat (mul n10 n100k)
localCBNtest [normalize] = localCBN n10
-- Conversion checking
--------------------------------------------------------------------------------
-- smalltt : 27ms , 6.2 MB
-- Agda : 0.6s , 57 MB
-- Coq : 1s , 340 MB
conv100k [elaborate] : Eq n100k n100kb = refl
-- smalltt : 0.31s , 6.2 MB
-- Agda : 3.5s , 1 GB
-- Coq : stack overflow
conv1M [elaborate] : Eq n1M n1MB = refl
-- smalltt : 2.7s, 6.2 MB
-- Coq : stack overflow
-- Agda : out of memory
conv10M [elaborate] : Eq n10M n10MB = refl
-- smalltt : 3.5ms, 6 MB
-- Coq : 0.1s , 220 MB
-- Agda : out of memory
conv10kmeta [elaborate] : Eq n10k (add n10kb _) = refl
-- smalltt : 0.31s, 6 MB
-- Agda : out of memory
-- Coq : stack overflow
conv1Mmeta [elaborate] : Eq n1M (add n1M _) = refl
-- smalltt : 0.9s, 900 MB
-- Agda : 8.5s , 3.5 GB
-- Coq : stack overflow
convNfun1M [elaborate] : Eq (nfun n1M) (nfun n1MB) = refl
-- Church-coded simply typed lambda calculus
--------------------------------------------------------------------------------
Ty : U
= (Ty : U)
(ι : Ty)
(fun : Ty → Ty → Ty)
→ Ty
ι : Ty
= λ _ ι _. ι
fun : Ty → Ty → Ty
= λ A B Ty ι fun. fun (A Ty ι fun) (B Ty ι fun)
Con : U
= (Con : U)
(nil : Con)
(cons : Con → Ty → Con)
→ Con
nil : Con
= λ Con nil cons. nil
cons : Con → Ty → Con
= λ Γ A Con nil cons. cons (Γ Con nil cons) A
Var : Con → Ty → U
= λ Γ A.
(Var : Con → Ty → U)
(vz : {Γ A} → Var (cons Γ A) A)
(vs : {Γ B A} → Var Γ A → Var (cons Γ B) A)
→ Var Γ A
vz : {Γ A} → Var (cons Γ A) A
= λ Var vz vs. vz
vs : {Γ B A} → Var Γ A → Var (cons Γ B) A
= λ x Var vz vs. vs (x Var vz vs)
Tm : Con → Ty → U
= λ Γ A.
(Tm : Con → Ty → U)
(var : {Γ A} → Var Γ A → Tm Γ A)
(lam : {Γ A B} → Tm (cons Γ A) B → Tm Γ (fun A B))
(app : {Γ A B} → Tm Γ (fun A B) → Tm Γ A → Tm Γ B)
→ Tm Γ A
var : {Γ A} → Var Γ A → Tm Γ A
= λ x Tm var lam app. var x
lam : {Γ A B} → Tm (cons Γ A) B → Tm Γ (fun A B)
= λ t Tm var lam app. lam (t Tm var lam app)
app : {Γ A B} → Tm Γ (fun A B) → Tm Γ A → Tm Γ B
= λ t u Tm var lam app. app (t Tm var lam app) (u Tm var lam app)
-- Well-typed interpreter for Church-coded STLC
--------------------------------------------------------------------------------
EvalTy : Ty → U
= λ A. A _ Bot (λ A B. A → B)
EvalCon : Con → U
= λ Γ. Γ _ Top (λ Δ A. Pair Δ (EvalTy A))
EvalVar : {Γ A} → Var Γ A → EvalCon Γ → EvalTy A
= λ x. x (λ Γ A. EvalCon Γ → EvalTy A)
(λ env. proj2 env)
(λ rec env. rec (proj1 env))
EvalTm : {Γ A} → Tm Γ A → EvalCon Γ → EvalTy A
= λ t. t (λ Γ A. EvalCon Γ → EvalTy A)
EvalVar
(λ t env α. t (pair env α))
(λ t u env. t env (u env))
-- Large embedded STLC term
--------------------------------------------------------------------------------
-- smalltt : 37ms , 6 MB
-- Coq : 270ms , 240 MB
-- Agda : 2.5s , 120 MB
STLCStress [elaborate] : Tm nil (fun (fun ι ι) (fun ι ι))
= lam (lam (
app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
(var vz))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))
))
-- smalltt : 50 ms , 46 MB
-- Coq, Agda : can't benchmark precisely (too fast to measure by hand)
-- Coq seems subjectively as fast as smalltt, Agda a bit slower
STLCEvalTest [normalize] = EvalTm STLCStress tt