Coder Social home page Coder Social logo

functional-benchmarks's Introduction

Functional Benchmarks

This repository contains a collection of benchmarks of functional programming languages and proof assistants. It is split in two categories, Checker and Runtime, which measure the time it takes to type-check and run a program, respectivelly. The main goal of this repository is to track Kind's performance compared to alternatives.

Type Checker

The tests below measure type-checking and theorem proving performance.

nat_exp

Proof that is-even (2 ^ N) == true. Measures type-level evaluation speed.

add (a: Nat) (b: Nat) : Nat
add x zero     = x
add x (succ y) = succ (add x y)

mul (a: Nat) (b: Nat) : Nat
mul a zero     = zero
mul a (succ b) = add a (mul a b)

exp (a: Nat) (b: Nat) : Nat
exp a zero     = succ zero
exp a (succ b) = mul a (exp a b)

Main : Equal (is_even (exp N2 N)) true
Main = refl

Comments: Kind is many times faster than alternatives, due to HVM's raw speed.

tree_fold

Proof that (tree-fold (full-tree N) and true) == true. Measures type-level evaluation speed.

full_tree (d: Nat) : Tree
full_tree zero     = leaf
full_tree (succ d) = let branch = full_tree d; node branch branch

tree_fold (a: Tree) (p: Type) (n: p -> p -> p) (l: p) : p
tree_fold leaf       p n l = l
tree_fold (node a b) p n l = n (tree_fold a p n l) (tree_fold b p n l)

force_tree (a: Tree) : Bool
force_tree t = tree_fold t Bool (a => b => and a b) true

Main : Equal (force_tree (full_tree N)) true
Main = refl

Comments: Kind is many times faster than some alternatives, due to HVM's raw speed.

nat_exp_church

Proof that is-even (2 ^ N) == true, Church encoded. Measures type-level evaluation asymptotics.

Church.add (a: Church.Nat) (b: Church.Nat) : Church.Nat
Church.add a b = p => f => z => a p f (b p f z)

Church.mul (a: Church.Nat) (b: Church.Nat) : Church.Nat
Church.mul a b = p => f => a p (b p f)

Church.exp (a: Church.Nat) (b: Church.Nat) : Church.Nat
Church.exp a b = p => b (p -> p) (a p)

Main : Equal (Church.is_even (Church.exp Church.N2 N)) Church.true
Main = refl

Comments: Kind is exponentially faster than alternatives, due to HVM's optimal reduction.

tree_fold_church

Proof that (tree-fold (full-tree N) and true) == true, Church encoded. Measures type-level evaluation asymptotics.

Church.full_tree (d: Church.Nat) : Church.Tree
Church.full_tree d = p => n => l => d p (t => n t t) l

Church.tree_fold (a: Church.Tree) (p: Type) (n: p -> p -> p) (l: p) : p
Church.tree_fold t p n l = t p n l

Church.force_tree (a: Church.Tree) : Church.Bool
Church.force_tree t = Church.tree_fold t Church.Bool (a => b => Church.and a b) Church.true

Main : Equal (Church.force_tree (Church.full_tree N)) Church.true
Main = refl

Comments: Kind is exponentially faster than alternatives, due to HVM's optimal reduction.

vector

Type-checks a huge vector with several meta variables. Measures parser and elaborator performance.

TODO

STLC

Type-checks a simply typed λ-calculus interpreter. Measures parser and elaborator performance.

TODO

RLP

Type-checks a RLP identity proof. Measures performance of heavy-weight equational reasoning.

TODO

Runtime

The tests below measure runtime performance.

list_fold

Creates a large list and folds over it with uint64 addition. Measures runtime evaluation speed for sequential recursion.

Fold <t: Type> (list: List t) <p: Type> (cons: t -> p -> p) (nil: p) : p
Fold t Nil         p c n = n
Fold t (Cons x xs) p c n = c x (Fold xs c n)

Range (n: U60) (list: List U60) : List U60
Range 0 xs = xs
Range n xs = let m = (- n 1); Range m (Cons m xs)

Comments: Kind and Haskell have similar performance on sequential recursive algorithms.

tree_fold

Creates a large list and folds over it with uint64 addition. Measures runtime evaluation speed for parallel recursion.

Gen (n: U60) : Tree
Gen 0 = Leaf 1
Gen n = Node (Gen (- n 1)) (Gen (- n 1))

Sum (tree: Tree) : U60
Sum (Leaf x)   = x
Sum (Node a b) = (+ (Sum a) (Sum b))

Comments: Kind outperforms Haskell on parallel recursive algorithms.

quicksort

Creates a large list of uint64's and sorts it. Measures runtime evaluation speed for parallel recursion.

TODO

Note: benchmark already available on HVM's repo. Will be ported to Kind soon.

composition

Composes a function an exponential amount of times. Measures runtime asymptotics.

TODO

Note: benchmark already available on HVM's repo. Will be ported to Kind soon.

lambda_arithmetic

Performs arithmetic with λ-encoded ints. Measures runtime asymptotics.

TODO

Note: benchmark already available on HVM's repo. Will be ported to Kind soon.

Replicating

To replicate these benchmarks, just run:

ulimit -s unlimited # give unlimited stack space
node benchmark.js

For specific commands, check the contents of benchmark.js.

Notes

The original sources are available on Checker and Runtime. We attempt to make the test cases as identical as possible. These tests are focused in comparing pure functional programming workloads, which mostly consist of datatype allocation, pattern-matching, functions, closures and recursion. As such, it doesn't cover low-level algorithms that are heavy on mutable array manipulation and in-place loops with mostly numeric workloads.

These benchmarks are focused on runtime and type-level evaluation performance. They do not cover elaboration (yet), which is commonly a significant source of slowdown. Kind doesn't have a complex elaborator, thus, it doesn't suffer from this problem; but, in turn, it is slightly more verbose than alternatives in certain areas. For a brilliantly designed elaborator, check smalltt by András Kovács. Kind aims to, in a future, incorporate insights from this work. Also, Kind does not have a totality checker (yet), so, it is arguably doing less than alternatives; although the cost of the totality checker should be negligible in comparison to general evaluation, but it is still worth noting.

Finally, these the type-checker all use Kind's Rust interpreter. In theory, Kind could be compiled to machine code, which would make it 3-4 faster, but the cost of C compilation would overshadow that. In a future, once we implement incremental compilation, we might be able to pre-compile the type-checker, allowing only user-defined functions to be injected. That would immediately make Kind's numbers 3-4x lower. There are other incoming optimizations on the making, including a complete GPU runtime!

functional-benchmarks's People

Contributors

algebraic-sofia avatar hargonix avatar kings177 avatar victortaelin avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar

functional-benchmarks's Issues

Lean results?

Can you post the Lean proof checking and runtime results to the charts in the README?

GPU numbers?

curious how these look now. if there's a straightforward way to compile something like set.mm for testing, i'd be very curious

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.