Hackle's blog
between the abstractions we want and the abstractions we get.
Hackle's blog
between the abstractions we want and the abstractions we get.
In Fin we've seen a version of type-safe indexFin (which is basically a copy of the index function defined in Data.Vect) which once compiles, guarantees to return a valid element from a vector.
import Data.Fin
import Data.Vect
indexFin : {n: Nat} -> Fin n -> Vect n a -> a
indexFin FZ (x :: xs) = x
indexFin (FS s) (x :: xs) = indexFin s xs
Which is simply called as such:
*fin> indexFin 3 [1,2,3,4]
4 : Integer
*fin> indexFin 0 [1,2,3,4]
1 : Integer
*fin> indexFin 3 [1,2,3]
(input):1:10:When checking argument prf to function Data.Fin.fromInteger:
When using 3 as a literal for a Fin 3
3 is not strictly less than 3
Out of sheer curiosity - can we have an alternative to this?
Suppose I can prove an index argument is less than the length of the vector, I should be able to get the same type-safety?
elementAtelementAt : (idx: Nat) -> Vect (S n) a -> { auto prf: n `GTE` idx } -> a
A few interesting things:
S n rather than simply n, which is an Idris way of saying this vect must not be emptyGTE idx which means idx must be within bound.(Read more about auto proof here)
I don't know about you but I feel pretty impressed (by Idris and myself) how expressive the types alone can be!
Let's now get to my favorite part - coding with Idris!
Naturally, Ctrl+Alt+A to add a definition (with Atom), so we have:
elementAt : (idx: Nat) -> Vect (S n) a -> { auto prf: n `GTE` idx } -> a
elementAt idx xs = ?elementAt_rhs
Well, don't think twice, just case split, and case split again.
elementAt : (idx: Nat) -> Vect (S n) a -> { auto prf: n `GTE` idx } -> a
elementAt Z (x :: xs) = ?elementAt_rhs_2
elementAt (S k) (x :: xs) = ?elementAt_rhs_3
Next we'll do a proof search on the hole elementAt_rhs_2, as expected, x is returned, which makes sense - if the idx is 0, then we should return the very first element in the list. So far so good!
elementAt : (idx: Nat) -> Vect (S n) a -> { auto prf: n `GTE` idx } -> a
elementAt Z (x :: xs) = x
elementAt (S k) (x :: xs) = ?elementAt_rhs_3
Now if we also do a proof search on elementAt_rhs_3, we get x as well - which is in the correct type, but won't make much sense for our function.
When in doubt, type search. Idris tells us:
a : Type
k : Nat
x : a
n : Nat
xs : Vect n a
prf : LTE (S k) n
--------------------------------------
elementAt_rhs_3 : a
There is a proof LTE (S k) n that tells us S k is less than or equal to n. Apparently this is just another form of n `GTE` idx (S k is one form of idx). Informative, but not very helpful.
To jump the gun here, the only way I see how - is just to return elementAt k xs. Seems reasonable right? Both the index and the size of the vector decrease by one, in another word, we are just using good-old recursion. So we get:
elementAt : (idx: Nat) -> Vect (S n) a -> { auto prf: n `GTE` idx } -> a
elementAt Z (x :: xs) = x
elementAt (S k) (x :: xs) = let x1 = elementAt k xs in ?elementAt_rhs_3
Try type check, no - the compiler does not like it...
When checking right hand side of elementAt with expected type
a
When checking argument prf to Main.elementAt:
Can't find a value of type
LTE k n
This is telling us we need to prove that k is less than or equal to n. But we already have GTE n (S k)?
While I think surely this makes perfect sense, Idris does not understand that if idx <= n + 1 then idx - 1 <= n . We have to prove it to Idris.
A bit lost, and honestly I don't know what to do except bringing the auto prf proof to scope. But the compiler still gives the same error.
elementAt : (idx: Nat) -> Vect (S n) a -> { auto prf: n `GTE` idx } -> a
elementAt Z (x :: xs) = x
elementAt (S k) (x :: xs) {prf} = let x1 = elementAt k xs in ?elementAt_rhs_3
Still lost, the only thing left to do, is to case split on prf, before that though, I have to revert the previous step, now I get:
elementAt : (idx: Nat) -> Vect (S n) a -> { auto prf: n `GTE` idx } -> a
elementAt Z (x :: xs) = x
elementAt (S k) (x :: xs) {prf = (LTESucc y)} = ?elementAt_rhs_1
Now a type search on the hole returns:
a : Type
k : Nat
x : a
right : Nat
xs : Vect (S right) a
y : LTE k right
--------------------------------------
elementAt_rhs_1 : a
A few things to note here
prf can be constructed, is LTESucc y, which by the name of it, means it's a successive definition over another proof yy is LTE k right, and S right is the length of xs. Previously we needed to prove LTE k n, and n is the length of xs too. That means we've found our proof now!?elementAt : (idx: Nat) -> Vect (S n) a -> { auto prf: n `GTE` idx } -> a
elementAt Z (x :: xs) = x
elementAt (S k) (x :: xs) {prf = (LTESucc y)} = elementAt k xs
Ah, now it compiles! Let's see if it really works?
*elementAt> elementAt 0 [1,2,3]
1 : Integer
*elementAt> elementAt 1 [1,2,3]
2 : Integer
*elementAt> elementAt 2 [1,2,3]
3 : Integer
*elementAt> elementAt 3 [1,2,3]
(input):1:1-19:When checking argument prf to function Main.elementAt:
Can't find a value of type
LTE 3 2
Yes, it does!
The Idris compiler is so powerful that if we express our problems well enough in types, it can guide us to a solution by giving us very useful information every step of the way.
For List, there is also an index function defined as such:
index : (n : Nat) ->
(xs : List a) ->
{auto ok : InBounds n xs} -> a
Note there is an auto proof ok? What's different is that a Vect has a length in its type, but a List does not, so how does List do it? And can the same proof be used for Vect? Why or why not?