Many Factorials in Lambda Calculus

Summary

I’m on a 16h flight to the ICFP SRC in Singapore right now, so here are many ways to calculate a factorial in bruijn, a syntactic sugar for the untyped lambda calculus using de Bruijn indices. It may be fun to view some of the programs as puzzles. (try clicking definitions or hovering indices/abstractions!) classic :import std/Combinator . :import std/Tuples . :import std/Number . :import std/Logic . fac y [[if (zero? 0) case-zero case-else]] case-zero (+1) case-else 0 ⋅ (1 --0) # (+5) = [[[[2 (2 (1 3))]]]] :test ((fac (+5)) =? (+120)) (true) classic, minified fac y [[=?0 (+1) (0 ⋅ (1 --0))]] up! fac y [[[(1 =? 0) 0 (1 ⋅ (2 ++1 0))]]] (+1) accu fac y [[[=?0 1 (2 (1 ⋅ 0) --0)]]] (+1) trampolined :import std/Result R # R.ok ⇒ callable fac* y [[[=?0 (R.err [2]) (R.ok [3 (2 ⋅ 1) --1])]]] (+1) bounce y [[1 (0 i)] : [0 i]] fac fac* → bounce kont # CPS'd fak y [[[=?1 (0 (+1)) (2 --1 [1 (2 ⋅ 0)])]]] fac \fak i why? fac why [[=?0 (+1) (0 ⋅ (1 i --0))]] Ω fac ω [[=?0 (+1) (0 ⋅ (1 1 --0))]] mutually (rosetta code) fac y [(0 lo) : (0 hi)] (+1d) (+1) lo [[[[(1 =? 0) 1 (0 ⋅ (2 1 --0))]]]] hi [[[[(1 =? 0) 0 (1 ⋅ (3 ++1 0))]]]] more mutual :import std/Number/Conversion . fac ∂((\mod (+4)) → ternary→unary → (select (+3u)) → f0) f4 [[[[[(0 =? (+0)) (+1) (0 ⋅ (1 --0))]]]]] f3 [[[[[(0 =? (+1)) (+1) (0 ⋅ (4 --0))]]]]] f2 [[[[[(0 =? (+2)) (+2) (0 ⋅ (3 --0))]]]]] f1 [[[[[(0 =? (+3)) (+6) (0 ⋅ (2 --0))]]]]] f0 y [(0 f1) : (0 f2) : (0 f3) : (0 f4)] increasingly mutual :import std/List . y* y [[&(1 0) <$> 0]] # this is so stupid fac ^(y* (head : tail)) head [[=?0 (+1) (0 ⋅ (^(~1) 0))]] tail y [[[[0 =? 2 (^1 --2) (1 !! ++2 0)]] : (1 ++0)]] (+1) sugared :import std/Math . fac [∏ (+1) → 0 | i] folded :import std/List . fac [foldr mul (+1) ({ (+1) → 0 })] scanned fac index (scanl mul (+1) →(+1)) pointfree fac (\take →(+1)) → product imperative (monad blog post) :import std/Imperative . …;… …→… fac i=1 ; (while (i≠0) n*=i;i-=1) ; return-n i=1 [0 : (+1)] i≠0 gets &[[1 ≠? (+0)]] n*=i;i-=1 get >>= &...