Limits of dependent typing in Idris

Question

I have been writing Haskell for a while now but wanted to try some experiments with the Idris language, and dependent typing. I have played around a bit, and read the basic doc, however I want to express a certain style of function, and do not know how / if it is possible.

Here are a couple of examples of what I wish to know whether or not can be expressed:

first: a function that takes two natural numbers but only type checks if the first is smaller than the other. So f : Nat -> Nat -> whatever where nat1 is smaller than nat2. The idea is that if a called like f 5 10 it would work, but if I called it like f 10 5 it would fail to type check.

second: a function that takes a string and a list of strings that only type checks if the first string is in the list of strings.

Are functions like this possible in Idris? If so how would you implement one of the simple examples noted? Thanks!

EDIT:

With the help of several users the following solution functions have been written:

module Main

import Data.So

f : (n : Nat) -> (m : Nat) -> {auto isLT : So (n < m)} -> Int
f _ _ = 50

g : (x : String) -> (xs : List String) -> {auto inIt : So (elem x xs)} -> Int
g x xs = 52

main : IO ()
main = putStrLn $ show $ g "hai" ["test", "yo", "ban", "hai", "dog"]

These current solutions do not work for large cases. For example if you run f with numbers above a few thousand it takes forever (not literally). I think this is because the type checking is currently search based. One user commented that it is possible to provide a hint to auto by writing the proof yourself. Assuming this is what is needed how would one write such a proof for either of these simple cases?

Answer 1

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.

Answer 2

So is a very general thing, that allows you to "lift" any boolean condition to the type level. This generality has its price though, which is that such proofs are (at least in my experience) harder to construct and more expensive to compute.

Instead it's usually better to create yourself a specialised proof type, which allows you to express only a certain type of condition, but in a simpler manner, yielding proofs that are cleaner and easier to construct. Idris standard library is full of such specialized proof types (or rather type families). Sure enough, it already contains those that you're concerned about here.

||| Proofs that `n` is less than or equal to `m`
||| @ n the smaller number
||| @ m the larger number
data LTE  : (n, m : Nat) -> Type where
  ||| Zero is the smallest Nat
  LTEZero : LTE Z    right
  ||| If n <= m, then n + 1 <= m + 1
  LTESucc : LTE left right -> LTE (S left) (S right)

(from Prelude.Nat)

A term of type LTE x y represents a proof that x is not larger than y (note that it works only for Nats, because it relies on the very internal structure of that type). LTEZero does not require any arguments since Z is never larger than any Nat (including Z itself). You are free to construct such proofs at will. For other numbers you can prove the LTE relation by induction (given the rule that LTE x y implies LTE (S x) (S y)). By deconstructing your arguments, you'll finally arrive at a moment when one of them is Z. If it's the left one, then you're done by stating that Z is less than or equal anything, if it's the right one, sorry, your assumption was false and therefore you won't be able to construct your proof.

maybeLTE : (n, m : Nat) -> Maybe (LTE n m)
maybeLTE Z _ = Just LTEZero
maybeLTE _ Z = Nothing
maybeLTE (S n) (S m) = map LTESucc $ maybeLTE n m

Note how this construction does not rely on any external notion of ordering. Instead, this very type defines what does it mean for a Nat to be less than or equal to another Nat. The two constructors (along with the type Nat itself) can be thought of as axioms of a theory, from which you can derive your proofs. Let's look at the types of these constructors again:

LTEZero : LTE Z right states that Z is less than or equal to right for all rights.

LTESucc : LTE left right -> LTE (S left) (S right) represents an implication: if left is less than or equal to right then S left is less than or equal to S right.

This is Curry-Howard Isomorphism in full glory.