Limits of dependent typing in Idris

Question

I wrote Haskell for a while, but wanted to try some experiments with the Idris language and dependent typing. I played a little and read the basic document, but I want to express a certain style of the function and do not know how to do it.

Here are some examples of what I want to know if it can be expressed:

first: a function that takes two natural numbers, but only checks the type if the first is less than the other. So f : Nat -> Nat -> whatever , where nat1 is less than nat2. The idea is that if the called f 5 10 style would work, but if I named it as f 10 5 , it would not be able to enter a check.

second: a function that takes a line and a list of lines that only enter a check if the first line is in the list of lines.

Are such functions the same as in Idris? If so, how would you implement one of the simple examples? Thanks!

EDIT:

With the help of several users, the following solution functions were 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 gx 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 will take forever (not literally). I think this is because type checking is currently search based. One user commented that you can give a hint to a car by writing a proof yourself. Assuming this is necessary, how can I write such proof for any of these simple cases?

Answer 1

I don’t particularly like So or generally avoid justified verification conditions running in programs in general. This is more satisfactory to weave your expectations into the fabric of the data itself. I am going to write a type for "natural numbers less than n ".

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

Fin is a numerical data type - compare the form of FS (FS FZ) with the form of the natural number S (SZ) , but with some additional level structure. Why is it called Fin ? There are exactly n unique members of type Fin n ; Fin , therefore, is a family of finite sets.

I mean: Fin really is a kind 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 less than 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 are in it, there are no numbers less than zero. That is, Fin Z , a set with a capacity of 0, is an empty set.

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

If you have a number less than n , then it, of course, is less than S n . So we have a way to loosen 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 maximum possible binding to the given Fin .

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

It is safe to determine the subtraction of Fin numbers from the number Nat , which are larger. We can also express the fact that the result will not be more than the input.

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

---

Everything works, but there is a problem: weaken works by rebuilding its argument in O (n) time, and we apply it with every recursive call - which gives O (n ^ 2) a subtraction algorithm. How awkward! weaken does exist to help type checking, but has a significant effect on the asymptotic complexity of the code. Can we leave without weakening the result of the recursive call?

Well, we had to call weaken , because every time we come across S , the difference between the result and the score increases. Instead of vigorously pulling the value to the correct type, we can close the gap by carefully pulling it 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 the compression of Fin associated with strengthen . Evaluation of the result - exactly the same as necessary.

sub that I used in the type is the subtraction of natural numbers. The fact that it is truncated by zero does not bother us, because type - ensures that it never happens. (This function can be found in Prelude as minus .)

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

The lesson to be learned here is this. At first, the construction of some correctness properties in our data caused an asymptotic slowdown. We could refuse to create promises about the return value and return to the untyped version, but actually giving the type checking function more information allowed us to get to where we were going without sacrificing.

Answer 2

So that this is a very common thing, which allows you to "raise" any logical condition to the type level. This commonality comes at a price, which is that such evidence (at least in my experience) is harder to build and more expensive to compute.

Instead, it is usually best to create a specialized type of evidence for yourself that allows you to express only a certain type of condition, but in a simpler way, obtaining evidence that is cleaner and easier to build. The Idris Standard Library is full of such specialized types of evidence (or rather, type families). Of course, it already contains the ones that bother you 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 xy provides evidence that x not greater than y (note that it only works for Nat s, since it relies on the internal structure of this type). LTEZero does not require any arguments, since Z never bigger than any Nat (including Z itself). You can build such evidence as you wish. For other numbers, you can prove the LTE relation by induction (given the rule that LTE xy implies LTE (S x) (S y) ). By deconstructing your arguments, you will finally get the moment when one of them is Z If it is left, you did it by stating that Z less than or equal to anything, if it is correct, sorry, your assumption was false, and therefore you you cannot build evidence.

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

Note that this construction does not depend on any external concepts of ordering. Instead, this type defines what it means for Nat be less than or equal to another Nat . Two constructors (along with the type Nat ) can be considered as axioms of the theory from which you can get your proofs. Let's look at the types of these constructors again:

LTEZero: LTE Z right indicates that Z less than or equal to right for all right s.

LTESucc: LTE left right → LTE (S left) (S right) is a consequence: if left less than or equal to right then S left less than or equal to S right .

This is Curry-Howard isomorphism in full glory.