Functional Pipelines

Chain function calls left-to-right with the forward pipeline operator |>
Compose functions into new functions with ∘
Build data transformation pipelines using filter, map, and fold
Import libraries and organize code with namespaces

Functions are the verbs of programming
Pipelines let you chain them into readable data flows

Forward Pipeline

def double (x : Int) : Int := x * 2
def addOne (x : Int) : Int := x + 1

-- without pipes: nested calls read inside-out
#eval double (addOne 3)

-- with |> : left-to-right, step by step
#eval 3 |> addOne |> double

-- works with any data type
def greet (name : String) : String := s!"Hello, {name}"
def shout (s : String) : String := s.toUpper

#eval "world" |> greet |> shout

8
8
"HELLO, WORLD"

x |> f means "apply f to x"
- Like Unix pipes: echo world | wc flows data left to right
Without |>, nested calls read inside-out: f (g (h x))
- With |>, they read left to right: x |> h |> g |> f
|> is just syntactic sugar: x |> f is exactly f x
- But it puts the data first and the transformation second, which is easier to scan
Works with any function: named, anonymous, library, your own

Anonymous Functions in Pipelines

-- |> works with anonymous functions too
def numbers : List Int := [1, 2, 3, 4, 5]

#eval numbers
  |> List.map (· * 2)
  |> List.filter (· > 5)

[6, 8, 10]

Anonymous functions work naturally in pipelines
The · placeholder (from basics) makes them compact
List.map and List.filter use the fully-qualified List. prefix
- We'll explain List. vs plain map shortly (DEBT)

Function Composition

def double (x : Int) : Int := x * 2
def addOne (x : Int) : Int := x + 1

-- compose two functions with ∘ (type \comp)
def addThenDouble : Int → Int := double ∘ addOne

-- the composed function is a new function
#eval addThenDouble 3

-- compose more than two with parentheses
def shout (s : String) : String := s.toUpper
def greet (name : String) : String := s!"Hello, {name}"

def excitedGreeting : String → String := shout ∘ greet

#eval excitedGreeting "world"

8
"HELLO, WORLD"

∘ (type \comp) composes two functions into a new function
- (f ∘ g) x means "apply g, then apply f"
Like |> but without the data: you're building a function, not applying one
Composition reads right-to-left: shout ∘ greet means "greet then shout"
- This matches math notation: (f ∘ g)(x) = f(g(x))
Use parentheses to compose more than two: f ∘ (g ∘ h) or (f ∘ g) ∘ h

Composition vs. Pipeline

def double (x : Int) : Int := x * 2
def addOne (x : Int) : Int := x + 1

-- pipe: apply functions to a value
#eval 3 |> addOne |> double

-- composition: combine functions without a value
def addThenDouble : Int → Int := double ∘ addOne
#eval addThenDouble 3

8
8

|> feeds data through functions: 3 |> addOne |> double
- Use when you have a value
∘ builds a new function from two existing ones: double ∘ addOne
- Use when you want to name the combined operation and reuse it
x |> f |> g is equivalent to (g ∘ f) x
- But |> is usually clearer when you have the data in hand

Point-Free Style

def double (x : Int) : Int := x * 2
def addOne (x : Int) : Int := x + 1

-- point-ful: the argument is named explicitly
def doubleAfterAdd (x : Int) : Int := double (addOne x)

-- point-free: the argument is never mentioned
def doubleAfterAddPF : Int → Int := double ∘ addOne

#eval doubleAfterAdd 3
#eval doubleAfterAddPF 3

-- point-free with anonymous functions
def squareAll : List Int → List Int := List.map (· ^ 2)
#eval squareAll [1, 2, 3]

8
8
[1, 4, 9]

Point-free style omits the argument names entirely
- The argument is implicit: "double after adding one"
doubleAfterAdd names x explicitly; doubleAfterAddPF never mentions it
- Both produce the same result
Point-free is concise for simple pipelines
- For complex logic, naming the arguments is usually clearer
Python equivalent: compose(double, add_one) instead of lambda x: double(add_one(x))

Filter-Map-Fold Pipelines

-- pipeline: a chain of |> operations
-- like Python: [x for x in data if ...] with transformations

def numbers : List Int := [1, 3, 5, 2, 8, 4, 7]

-- filter, then map, then fold — in one pipeline
#eval numbers
  |> List.filter (· > 2)
  |> List.map (· * 3)
  |> List.filter (· < 20)
  |> List.foldl (· + ·) 0

-- same computation as a pipeline of partial results
def step1 : List Int := List.filter (· > 2) numbers
def step2 : List Int := List.map (· * 3) step1
def step3 : List Int := List.filter (· < 20) step2
def result : Int := List.foldl (· + ·) 0 step3

#eval result

36
36

Filter-map-fold chains are the bread and butter of functional pipelines
Instead of naming intermediate results, thread data through transformations
Each |> feeds the previous result into the next function
Like Python list comprehensions with chained operations
- [x*3 for x in data if x > 2] is a filter-then-map in one expression
- But pipelines separate concerns and can chain more steps

Pipelines vs. Imperative Loops

-- imperative style: accumulate in mutable variables
-- (Python equivalent shown in comment)

-- Lean version with explicit recursion:
def sumOfSquaresOfEvens (xs : List Int) : Int :=
  match xs with
  | [] => 0
  | x :: rest =>
    let restResult := sumOfSquaresOfEvens rest
    if x % 2 == 0 then x*x + restResult else restResult

#eval sumOfSquaresOfEvens [1, 2, 3, 4]

-- pipeline style: describe what you want, not how
#eval [1, 2, 3, 4]
  |> List.filter (· % 2 == 0)
  |> List.map (· ^ 2)
  |> List.foldl (· + ·) 0

20
20

The recursive version spells out how: loop, accumulate, test, branch
The pipeline version describes what: filter evens, square them, sum
Both produce the same result; pipelines are usually easier to read
In Python, you'd write a for loop with if and an accumulator variable
- The pipeline is the same idea as sum(x*x for x in xs if x % 2 == 0)

Pipelines with Strings

-- pipelines work with strings too
def words : List String := ["hello", "world", "from", "lean"]

#eval words
  |> List.filter (fun w => w.length > 4)
  |> List.map String.toUpper
  |> String.intercalate " | "

"HELLO | WORLD"

Pipelines work with any type, not just numbers
String.toUpper is a function you can pass to List.map
String.intercalate joins list elements with a separator
- Like Python's " | ".join(["HELLO", "WORLD"])
Notice the pipeline uses fun w => w.length > 4 because we need to name w
- (·.length > 4) is not valid Lean syntax, so we fall back to explicit fun

Importing Libraries

-- import a module from the standard library
-- the prelude is always available, but for extra utilities you need imports

-- example: List already has many functions without importing
#eval List.range 5
#eval List.zip [1, 2] ["a", "b"]

-- for more advanced operations, import Std
-- (shown later when you need it)

[0, 1, 2, 3, 4]
[(1, "a"), (2, "b")]

import ModuleName brings a library module into scope
- Like Python's import module
The Lean prelude is always available without imports
- It includes List, String, Option, Nat, Int, and basic operations
Everything we've used so far comes from the prelude
For more advanced features, you import additional modules
- import Std gives you the extended standard library
- We'll see more import examples in later lessons (DEBT)

Namespaces

-- namespaces prevent name collisions
-- like Python's modules: math.sin vs math.cos

namespace Greeting

def hello (name : String) : String := s!"Hello, {name}"

end Greeting

namespace Farewell

def hello (name : String) : String := s!"Goodbye, {name}"

end Farewell

-- use the fully-qualified name
#eval Greeting.hello "world"
#eval Farewell.hello "world"

"Hello, world"
"Goodbye, world"

namespace Name … end Name wraps definitions in a named scope
- Like Python modules or C++ namespaces
Two namespaces can define the same function name without collision
- Greeting.hello and Farewell.hello are different functions
Use Namespace.name to refer to a definition from outside
- Like Python's module.function after import module

Opening Namespaces

namespace Colors

def red : String := "#FF0000"
def green : String := "#00FF00"

end Colors

-- open brings all names into scope
-- like Python's: from module import *
open Colors

#eval red
#eval green

"#FF0000"
"#00FF00"

open NamespaceName brings all names into the current scope
- Like Python's from module import *
After open Colors, you can write red instead of Colors.red
Use sparingly: it can make code harder to understand
- Where did red come from? You have to scan upward to find the open

Standard Library Examples

-- List has many useful functions in the prelude
def nums : List Int := [10, 20, 30, 40, 50]

-- take first n elements
#eval nums.take 3

-- drop first n elements
#eval nums.drop 2

-- range from 0 to n-1
#eval List.range 5

-- zip two lists together
#eval List.zip [1, 2, 3] ["a", "b", "c"]

-- use them in a pipeline
#eval List.range 10
  |> List.filter (· % 3 == 0)
  |> List.map (· * 10)

[10, 20, 30]
[30, 40, 50]
[0, 1, 2, 3, 4]
[(1, "a"), (2, "b"), (3, "c")]
[0, 30, 60, 90]

List has many functions beyond map, filter, and foldl
take n keeps the first n elements
drop n discards the first n elements
List.range n generates [0, 1, …, n-1]
- Like Python's range(n) but returns a list, not an iterator
List.zip pairs elements from two lists into tuples
- Like Python's zip(list1, list2)
All of these compose naturally in pipelines

Arrays vs. Lists

-- Arrays: contiguous memory, O(1) indexed access, fixed-size after creation
def nums : Array Int := #[10, 20, 30, 40, 50]
#eval nums[2]!          -- 30, direct O(1) access
#eval nums.size         -- 5

-- Lists: singly-linked, O(1) head/tail, O(n) indexed access
def items : List Int := [10, 20, 30, 40, 50]
#eval items.head!       -- 10, O(1)
#eval items.length      -- 5, O(n): traverses the whole list

-- Converting between them
#eval items.toArray     -- List → Array
#eval nums.toList       -- Array → List

-- Use Array when you need random access or interop with IO functions
-- Use List when you need pattern matching with :: or cons-style recursion

30
5
10
5
#[10, 20, 30, 40, 50]
[10, 20, 30, 40, 50]

Lean has two sequence types with different performance characteristics
List (e.g. [1, 2, 3]) is a singly-linked list
- Adding to the front with :: is O(1)
- Pattern matching on head/tail is idiomatic and efficient
- List.length and indexed access list[i]! are O(n)
Array (e.g. #[1, 2, 3]) stores elements contiguously in memory
- Indexed access arr[i]! is O(1)
- Appending is amortized O(1) (like Python's list.append)
- Cannot be pattern-matched with ::
Python's list is closer to Lean's Array in performance
- If you're porting Python that uses xs[i], use Array in Lean
- If you're writing idiomatic Lean with map/filter/foldl, List is the natural choice
Most IO functions (like IO.FS.readDir) return Array; pipeline functions work on List
- Convert with arr.toList or lst.toArray as needed

Exercises

Fix: Missing Pipeline Step

-- Fix: this pipeline is missing a step
-- it should double numbers, keep even results, then sum them
#eval [1, 2, 3, 4, 5]
  |> List.map (· * 2)
  |> List.foldl (· + ·) 0

hint

The pipeline doubles every number and sums the result
But the instructions say to keep only even results before summing
Add |> List.filter (· % 2 == 0) between the map and the foldl

Fix: Wrong Composition Order

-- Fix: the composition order is wrong
-- should add 1 then double, not double then add 1
def addOne (x : Int) : Int := x + 1
def double (x : Int) : Int := x * 2

def wrong : Int → Int := addOne ∘ double

#eval wrong 3
#guard wrong 3 == 8

hint

addOne ∘ double means "double first, then add one"
The #guard expects wrong 3 == 8, which is (3+1)*2 = 8
Swap the functions so addOne runs first, then double

Write: Word Pipeline

-- Write: pipeline that selects words with more than 3 letters,
-- uppercases them, and joins with " + "
def words : List String := ["hi", "hello", "yo", "world", "a"]

#eval words
  |> List.filter (fun w => 0 == 0)  -- replace with real filter
  |> List.map (fun w => w)          -- replace with uppercase
  |> String.intercalate ""          -- replace with " + "

hint

Replace fun w => 0 == 0 with a filter that keeps words with more than 3 letters: fun w => w.length > 3
Replace fun w => w with String.toUpper to uppercase each word
Replace "" with " + " as the intercalation separator
The expected output is "HELLO + WORLD"

Write: Compose Three

-- Write: compose three functions with ∘
-- create a pipeline that: uppercases, reverses, then adds "!!"
def upper (s : String) : String := s.toUpper
def reverse (s : String) : String :=
  String.ofList (s.toList.reverse)
def exclaim (s : String) : String := s ++ "!!"

-- replace with composition of all three
def shoutReverse : String → String := upper

#eval shoutReverse "hello"
#guard shoutReverse "hello" == "OLLEH!!"

hint

Replace upper with a composition of all three functions
exclaim ∘ reverse ∘ upper means "uppercase, then reverse, then add !!"
Remember that ∘ reads right-to-left, so the first transformation goes on the right
The #guard expects "OLLEH!!" for the input "hello"

Write: Wrap in a Namespace

-- Write: put the definition in a namespace and use it
-- 1. wrap 'pi' in a namespace called 'Math'
-- 2. uncomment and fix the last line

def pi : Float := 3.14159

#eval Math.pi

hint

Wrap the def pi line with namespace Math (before) and end Math (after)
Then Math.pi will be a valid reference
The output should be 3.141590

Fix: Type Mismatch in Pipeline

-- Fix: this pipeline has a type mismatch
-- the shout function expects a String, but it's being fed an Int
def double (x : Int) : Int := x * 2
def shout (s : String) : String := s.toUpper

#eval 5 |> double |> shout

hint

double returns an Int, but shout expects a String
The pipeline 5 |> double |> shout tries to feed an Int into a String function
Either change shout to work on Int, or remove it from the pipeline

Fix: `open` Before Namespace

-- Fix: the 'open' must come after the namespace definition
-- right now, open Colors happens before Colors exists

open Colors

namespace Colors
def red : String := "#FF0000"
end Colors

#eval red

hint

open Colors is on line 4, but the namespace is defined on line 6
Lean reads top to bottom: you can't open a namespace before it exists
Move open Colors after the end Colors line

Fix: Wrong Number of Placeholders

-- Fix: the · placeholder usage is wrong
-- used as subtract-from: but there are two placeholders for a one-arg function
def numbers : List Int := [5, 10, 15]

-- (· - 2) subtracts 2 from each; (· - ·) is a two-argument function
def subtractAll : List Int := numbers |> List.map (· - ·)

hint

List.map expects a function that takes one argument
(· - ·) is a two-argument function (subtraction with two placeholders)
Use (· - 2) to subtract 2 from each element, or write an explicit fun x => x - 2

Fix: `drop` vs. `take`

-- Fix: drop and take are swapped — this discards the first 2 and keeps the rest
-- it should keep the first 2 and drop the rest
#eval List.range 5
  |> List.drop 2
  |> List.map (· * 10)
#guard (List.range 5 |> List.drop 2 |> List.map (· * 10)) == [0, 10]

hint

List.drop 2 removes the first 2 elements and keeps the rest
The #guard expects [0, 10], which are the first two elements of [0,1,2,3,4] after doubling
Replace drop with take to keep the first 2 elements

Write: Number Pipeline from Scratch

-- Write: use a pipeline to generate numbers 0..9,
-- keep multiples of 3, double them, and sum the result
-- expected output: 36 (multiples: 0,3,6,9; doubled: 0,6,12,18; sum: 36)
#eval 0  -- replace with pipeline

hint

Start with List.range 10 to get [0, 1, …, 9]
Pipe through List.filter to keep numbers divisible by 3: (· % 3 == 0)
Pipe through List.map to double each: (· * 2)
Pipe through List.foldl to sum: (· + ·) 0
Expected output is 36

Write: Make It Point-Free

-- Write: convert this point-ful function to point-free using ∘
def addExcitement (s : String) : String :=
  let upper := s.toUpper
  upper ++ "!!!"

-- replace with: addExcitement should use ∘ and not name 's'
def addExcitementPF : String → String := addExcitement

#eval addExcitementPF "hello"
#guard addExcitementPF "hello" == "HELLO!!!"

hint

addExcitement does two things: uppercases, then appends "!!!"
Define an exclaim helper: def exclaim (s : String) : String := s ++ "!!!"
Then addExcitementPF is exclaim ∘ String.toUpper
The argument s disappears entirely: that's point-free

Write: Zip and Format

-- Write: zip two lists into pairs, then use a pipeline
-- to format each pair as "name: age"
def names : List String := ["Alice", "Bob", "Carol"]
def ages : List Int := [25, 30, 35]

-- zip the lists, then map each pair to a formatted string
#eval [""]  -- replace with pipeline

hint

Use List.zip names ages to get [("Alice", 25), ("Bob", 30), ("Carol", 35)]
Pipe through List.map with a function that destructures each pair
Use fun (name, age) => s!"{name}: {age}" to format each pair
Expected output is ["Alice: 25", "Bob: 30", "Carol: 35"]

Functional Pipelines

Forward Pipeline

Anonymous Functions in Pipelines

Function Composition

Composition vs. Pipeline

Point-Free Style

Filter-Map-Fold Pipelines

Pipelines vs. Imperative Loops

Pipelines with Strings

Importing Libraries

Namespaces

Opening Namespaces

Standard Library Examples

Arrays vs. Lists

Exercises

Fix: Missing Pipeline Step

Fix: Wrong Composition Order

Write: Word Pipeline

Write: Compose Three

Write: Wrap in a Namespace

Fix: Type Mismatch in Pipeline

Fix: open Before Namespace

Fix: Wrong Number of Placeholders

Fix: drop vs. take

Write: Number Pipeline from Scratch

Write: Make It Point-Free

Write: Zip and Format

Fix: `open` Before Namespace

Fix: `drop` vs. `take`