Logic, Types and Spaces

Towards homotopy type theory

A Program : Lattice Points in a Circle

We now give a program (i.e., a function) that, given a natural number $n$, lists all points in the plane with co-ordinates natural numbers, which are contained in the circle of radius $n$. This illustrates how we can implement a combination of nested loops and conditions using map, flatMap and filter.

We first define a function $leq$, denoting less than or equal to, for natural number. We have reserved $\leq$ for something nicer. This is a recursive definition.

_leq_ :     Bool
zero leq _ = true
(succ n) leq zero = false
(succ n) leq (succ m) = n leq m

We can now construct the function we promised. For each $a \in \mathbb{N}$, we can define a function associating to it a list by filtering $b\in \mathbb{N}$ by requiring the pair $(a , b)$ to lie in the circle, and then map to the pair $(a, b)$. We flatMap using this list-valued function.

points :   List ( × )
points n = (upto (succ n)) flatMap (λ a  ((upto (succ n)) filter (λ b  ((a * a) + (b * b)) leq (n * n)points )) map (λ b  [ a , b ]))

We have used map, flatMap and filter to replace nested loops and control statements (if in this case) in older programming languages. In imperative code we would have started with an empty list, used a loop for $a$, an inner one for $b$ and added to the list pairs that satisfy the condition of lying in the circle.