Limits of dependent typing in Idris

I'm not especially fond of So, or indeed of having avoidable proof-terms running around in programs at all. It's more satisfying to weave your expectations into the fabric of the data itself. I'm going to write down a type for "natural numbers smaller than n".

data Fin : Nat -> Set where
  FZ : Fin (S n)
  FS : Fin n -> Fin (S n)

Fin is a number-like data type - compare the shape of FS (FS FZ) with that of the natural number S (S Z) - but with some additional type-level structure. Why's it called Fin? There are precisely n unique members of the type Fin n; Fin is thus the family of finite sets.

I mean it: Fin really is a sort of number.

natToFin : (n : Nat) -> Fin (S n)
natToFin Z = FZ
natToFin (S k) = FS (natToFin k)

finToNat : Fin n -> Nat
finToNat FZ = Z
finToNat (FS i) = S (finToNat i)

Here's the point: a Fin n value must be smaller than its n.

two : Fin 3
two = FS (FS FZ)
two' : Fin 4
two' = FS (FS FZ)
badTwo : Fin 2
badTwo = FS (FS FZ)  -- Type mismatch between Fin (S n) (Type of FZ) and Fin 0 (Expected type)

While we're at it, there aren't any numbers less than zero. That is to say, Fin Z, a set with a cardinality of 0, is an empty set.

Uninhabited (Fin Z) where
  uninhabited FZ impossible
  uninhabited (FS _) impossible

If you have a number that's less than n, then it's certainly less than S n. We thus have a way of loosening the upper bound on a Fin:

weaken : Fin n -> Fin (S n)
weaken FZ = FZ
weaken (FS x) = FS (weaken x)

We can also go the other way, using the type checker to automatically find the tightest possible bound on a given Fin.

strengthen : (i : Fin n) -> Fin (S (finToNat i))
strengthen FZ = FZ
strengthen (FS x) = FS (strengthen x)

One can safely define subtraction of Fin numbers from Nat numbers that are larger. We can also express the fact that the result won't be any bigger than the input.

(-) : (n : Nat) -> Fin (S n) -> Fin (S n)
n - FZ = natToFin n
(S n) - (FS m) = weaken (n - m)

---

That all works, but there's a problem: weaken works by rebuilding its argument in O(n) time, and we're applying it at every recursive call of -, yielding an O(n^2) algorithm for subtraction. How embarrassing! weaken is only really there to help type-checking, but it has a drastic effect on the asymptotic time complexity of the code. Can we get away without weakening the result of the recursive call?

Well, we had to call weaken because every time we encounter an S, the difference between the result and the bound grows. Instead of forcefully yanking the value up to the correct type, we can close the gap by gently pulling the type down to meet it.

(-) : (n : Nat) -> (i : Fin (S n)) -> Fin (S (n `sub` finToNat i))
n - FZ = natToFin n
(S n) - (FS i) = n - i

This type is inspired by our success in tightening a Fin's bound with strengthen. The bound on the result of - is exactly as tight as it needs to be.

sub, which I used in the type, is subtraction of natural numbers. The fact that it truncates at zero needn't trouble us, because the type of - ensures that it'll never actually happen. (This function can be found in the Prelude under the name of minus.)

sub : Nat -> Nat -> Nat
sub n Z = n
sub Z m = Z
sub (S n) (S m) = sub n m

The lesson to be learned here is this. At first, building some correctness properties into our data caused an asymptotic slowdown. We could've given up on making promises about the return value and gone back to an untyped version, but in fact giving the type checker more information allowed us to get where we were going without making sacrifices.