Arrays

Arrays are implemented using tuples and dependent types.

What on earth is the type of this function?

Array(T: Type, n: Nat): Type
Array(T, 0) = ()
Array(T, n) = (T, Array(T, n - 1))

How it would expand into a tuple-array?

Array(Int, 3)
= (Int, Array(Int, 2))
= (Int, Int, Array(Int, 1))
= (Int, Int, Int, Array(Int, 0))
= (Int, Int, Int, ())
= (Int, (Int, (Int, ())))

Vectors

Implemented with Arrays and (dynamic typing?)

The type of data changes based on previous values, making it a dependent type

Big deal: the type of data is dependent on the value of capacity

Vec(T) = {
	length: Nat,
	capacity: Nat,
	data: Box(Array(T, capacity))
}

Invariants on structures

You might want to encode length <= capacity on the type (or other arbitrary things), because that way just by the fact you have a value v : Vec, you know v.length <= v.capacity.

Q: How do you do this?

A: Store a proof that length <= capacity on the vector.

This is the syntax for it.

a *<= b means “proof that a is less than b”.

Vec(T) = {
	length: Nat,
	capacity: Nat,
	data: Box(Array(T, capacity)),

	// Meat and potatoes
	proof_a: length < capacity, 
}

Q: What the hell? Why is statement being expressed as a type.

A: Types are analogous to statements, and values are analogous to proofs. The statement a value proves is it’s type. proofOfStmt: Stmt

A: Good 18 minute explanation ****https://youtu.be/SknxggwRPzU

A: Amazing ****42 minute explanation https://www.youtube.com/watch?v=IOiZatlZtGU

Vector Implementation

Vec(T) = {
	/* Data */
	length: Nat,
	capacity: Nat,
	data: Box(Array(T, capacity)),

	/* Proofs */
	no_overflow: (length <= capacity = True)
};

impl Vec (
	/* Pushes a new element to the end of the vector,
	allocating more memory if neccesary. */
	push[T](vec: &mut Vec(T))(elem: T) = (
		/* Extend if vector is out of space. */
		if vec.length == vec.capacity (
			vec.expand();
		)

		/* Note the new length of the vector. */
		vec.length += 1;

		/* Write element to heap. */
		vec.data[vec.length - 1] = elem;
	)

	/* Doubles the amount of space allocated for this vector. */
	expand[T](vec: &mut Vec(T)) = (
			/* The data pointer is about to be overwritten, so we must save the
			old value. */
			let old_data = vec.data;
			/* Because the Box has just been moved from vec.data to old_data,
			vec.data is uninitialised now. */

			/* Double the capacity of the vector. */
			vec.capacity *= 2;
			/* Because  */

			/* Allocate a new data pointer. */
			vec.data = Box::new();
	)

	/* Halves the amount of space allocated for this vector. */
);