← Back to archive

Posts tagged fp

3

Lean: introduction fp · 29/10 · ⌗

In this series of posts, I want to put a few things in order in my own head, create a simple reference, and help people appreciate the system if, for some unfathomable reason, they cannot be bothered to read the book—even though they absolutely should.

Encoding natural numbers (part 1) fp · 30/10

The classic inductive definition of natural numbers is well known: zero is a natural number, and the successor of a natural number is a natural number. The simplest way to encode such numbers in the lambda calculus is Church encoding, which seems to have no direct connection to the intuitive inductive type.

Untyped Lambda Calculus fp · 29/08 · ⌗ ▦

An attempt to explain the lambda calculus while implementing it in Haskell.

↑↓ navigate ↵ open esc close