Basic Operations

What distinguishes Lean from many other programming languages is that Lean is so called dependently typed programming language. This allows us to work with arrays that have their dimensions specified in their type. For example, vector dot product can be defined as

This function accepts the size of the array as an argument n : Nat and then two arrays of the same size n. The meaning of dependently typed is that the type of function argument can depend on the value of another argument. Here the type of x and y is Float^[n] which depends on the first argument n. This is really not possible in ordinary programming languages, some of them allow you to provide the dimension at compile time. In Lean this is not the case, the dimension n can be determined completly at runtime.

As you can see, one of the nice advantages is that we didn't have to specify the range over which we want to sum at it is automatically infered it should sum over the numbers 0..(n-1).

We can test the function with

2.000000

When calling a function, you have to provide only the arguments with normal braces, such as (x y : Float^[n]). Arguments with the curly braces {n : Nat} are implicit and will be infered automatically from the other arguments, from x and y in this case. Lean prevents us from providing arrays of different lenghts

application type mismatch
  dot ⊞[1.0, 1.0] ⊞[1.0, 1.0, 1.0]
argument
  ⊞[1.0, 1.0, 1.0]
has type
  Float^[3] : Type
but is expected to have type
  Float^[2] : Type

Let's back up and talk about the notation Float^[n] and how it connects to DataArray we talked about previously. An array x : Float^[n] has length n and thus can be indexed with number 0..(n-1). The type expressing all natural numbers smaller then n is denoted with Fin n. It is defined as a structure:

which holds the value val and a proof isLt that the value is infact smaller then n.

Float^[n] is just a syntactic sugar for DataArrayN Float (Fin n) which is DataArray Float together with a proof that the size of the array is n. In general, Fin n can be replaced with an arbitrary index type I. The definition of DataArrayN is:

which is an array data with a proof that the array size it equal to the size of the index set I. In the case of I = Fin n we have size (Fin n) = n.

Having the flexibility using an arbitrary type I as index is already sufficient to support arbitrary n-dimensional array. To get matrices we pick I = Fin n × Fin m. In other words matrix is just an array indexed by pair of indices (i,j) where 0≤i<n and 0≤j<m. Thus DataArrayN Float (Fin n × Fin m) is just a n×m matrix and the syntactic sugar for it is Float^[n,m]. We can generalize this and pick I = Fin n₁ × ... × Fin nᵣ which yields r-dimensional array with dimensions n₁, ..., nᵣ. The syntactic sugar for DataArrayN Float (Fin n₁ × ... × Fin nᵣ) is Float^[n₁, ..., nᵣ].

Have a look at chapter 1.4. Structures in Functional Programming in Lean to learn more about structures

Let's go over the basic operations on arrays in SciLean. As we mentioned previously you can create List with [1.0,2.0,3.0] or Array with #[1.0,2.0,3.0]. Here we will mainly focus on DataArray that uses ⊞[1.0,2.0,3.0] so let's create one

we can access its elements with bracket notation u[i]

1.000000

2.000000

3.000000

Lean can leverage the index information in the type of u so we can easily sum all the elements of u

6.000000

or convert an array to a function from the index type to array values

fun i => u[i] : Fin 3 → Float

Lean automatically infers the type of i

Similarly we can create a matrix

and we can access its elements

2.000000

Because matrix A is just an array indexed by Fin 2 × Fin 2 we can also write it as

3.000000

which might look like an odd quirk of our definition of matrix but hopeful later on you will see that this generality allows us to work with indices that have a proper meaning rather being a meaningless number.

Popular method for creating arrays in Python is list comprehension. To some capacity this can be viewed as process turning a function, f : Idx → Elem, into an array DataArraN Elem Idx. The notation is very similar to lambda notation fun x => f x

⊞ i => f i : Float^[10]

Unlike lambda notation, array notation uncurries all of its arguments. This means that ⊞ i j => f i j creates and matrix indexed by (i,j). For example outer product of two arrays can be defines as

If you want an array of arrays instead of matrix you would write ⊞ i => (⊞ j => x[i]*y[j]) or ⊞ j => (⊞ i => x[i]*y[j]) depending whether you want the matrix stored as an array of rows or columns.

Another way to set up a matrix is to set its elements one by one

We first create mutable zero matrix and then set every. The function fullRange creates a range that runs over all the elements of I. When working with matrices, one has to be careful if they are in column major or row major ordering and accordingly iterate over i first and then over j. We will explain later how this is done in SciLean so for now it is safe to just iterate over both indices simultaneously and we get the optimal order

Of course the above implementation of has the drawback that it first initialized the whole matrix to zero and then go over the matrix again and set it up to the correct value. Sometimes it is much more natural to create the matrix element by element. We can create an array with dynamic size and push element one by one. Once we are done we can fix the dimensions of the matrix.

Recall that Float^[n,m] is just syntax for DataArrayN Float (Fin n × Fin m) and DataArrayN X I is just a structure holding data : DataArray X and a proof h_size : data.size = size I. In this case, we provide the matrix A and in the second element we should provide a proof that A.size = size (Fin n × Fin m) = n*m. Right now, we do not want to focus on proofs to we just omit it. Deciding when to provide proofs and when to omit them is a crucial skill when writing programs in Lean. Often it is very useful to just state what your program is supposed to do. It is a an amazing tool to clarify in your head what program are you actually writing. On the other hand, providing all the proofs can be really tedious and often a waste of time if you have to reorganize your program and all your proofs are suddently invalid.

def reshape1 (x : Float^[I]) (n : Nat)    (h : size I = n)     : Float^[n] := ...
def reshape2 (x : Float^[I]) (n m : Nat)  (h : size I = n*m)   : Float^[n,m] := ...
def reshape3 (x : Float^[I]) (n m k: Nat) (h : size I = n*m*k) : Float^[n,m,k] := ...
...