Skip to content

Lean Basics

Functional Programming in Lean

Features

  • types themselves are objects, each of them also has to have a type.
#check Nat
-- Nat : Type

def \a : Type := Nat
def F : Type -> Type := List

def cons (\a : Type) (a : \a) (as : List \a) : List \a :=
    List.cons a as
  • every expression in Lean has a type, what type does Type itself have? - Lean's underlying foundation has an infinite hierarchy of types
#check Type
-- Type : Type 1
  • universe level - Type 0 is a universe of "small" or "ordinary" types. Type 1 is then a larger universe of types, which contains Type 0 as an element. - a universe at level u can only classify universes that are at levels lower than u
#check List
-- List.{u} (\a : Type u) : Type u

#check Prod
-- Prod.{u, v} (\a : Type u) (\b : Type v) : Type (max u v)

def F.{u} (\a : Type u) : Type u := Prod \a \a
#check F
-- F.{u} (\a : Type u) : Type u
  • theorem proving

Datatypes

  • structure is used to introduce a product type (that is, a type with just one constructor that takes any number of arguments)
structure Point where
    point :: -- override the default constructor name
    x : Float
    y : Float

-- standard initializer
{ x := 1.5, y := 2.8 } : Point

-- update structures
def zeroX (p : Point) : Point :=
    { p with x := 0 }
  • inductive is used to introduce a sum type (that is, a type with many distinct constructors)
inductive Nat where
    | zero : Nat
    | succ (n : Nat) : Nat

inductive List (\a : Type) where
    | nil : List \a
    | cons : \a -> List \a -> List \a

Pattern Matching

-- def by pattern-matching
def drop : Nat -> List a -> List a
    | Nat.zero, xs => xs
    | _, [] => []
    | Nat.succ, x :: xs => drop n xs

-- pattern matching
def isZero (n : Nat) : Bool :=
    match n with
    | Nat.zero => true
    | Nat.succ k => false

-- extract structure
def depth (p : Point3D) : Float :=
    match p with
    | { x := h, y := w, z := d } => d

-- recursion
def even (n : Nat) : Bool :=
    match n with
    | Nat.zero => true
    | Nat.succ k => not (even k)

Built-in Datatypes

Option (Sum String (Prod Nat String))

Functions

  • anonymous functions
fun (x : Nat) => x + 5

Recursion

  • recursive calls are all performed on a structually-smaller piece of the input
  • user must provide evidence that the function always terminates

Monads