In Idris, how to write a "vect generator" function that take a function of index in parameter

5
votes

I'm trying to write in Idris a function that create a Vect by passing the size of the Vect and a function taking the index in parameter. So far, I've this :

import Data.Fin
import Data.Vect

generate: (n:Nat) -> (Nat -> a) ->Vect n a
generate n f = generate' 0 n f where
  generate': (idx:Nat) -> (n:Nat) -> (Nat -> a) -> Vect n a
  generate' idx Z f = []
  generate' idx (S k) f = (f idx) :: generate' (idx + 1) k f

But I would like to ensure that the function passed in parameter is only taking index lesser than the size of the Vect. I tried that :

generate: (n:Nat) -> (Fin n -> a) ->Vect n a
generate n f = generate' 0 n f where
  generate': (idx:Fin n) -> (n:Nat) -> (Fin n -> a) -> Vect n a
  generate' idx Z f = []
  generate' idx (S k) f = (f idx) :: generate' (idx + 1) k f

But it doesn't compile with the error 

    Can't convert
            Fin n
    with
            Fin (S k)

My question is : is what I want to do possible and how ?

2
dependent-typeidris
I don't (yet) have an answer, but note two things: 1. If you can implement a "count up" function that takes n:Nat and gives the vector [FZ,...,n-1], then you can build your function using map. 2. It's not too terribly hard to write a function to reverse vectors, so if you can figure out a way to write a "count down" function, you can reverse its result to count down. – dfeuer
Another thought (maybe better). You can always "weaken" a Fin n to a Fin (m + n). So one idea might be to work with one argument going up and one argument going down, and one argument proving their sum is right. – dfeuer

2 Answers

4
votes

The key idea is that the first element of the vector is f 0, and for the tail, if you have k : Fin n, then FS k : Fin (S n) is a "shift" of the finite number that increments its value and its type at the same time.

Using this observation, we can rewrite generate as

generate : {n : Nat} -> (f : Fin n -> a) -> Vect n a
generate {n = Z} f = []
generate {n = S _} f = f 0 :: generate (f . FS)

Another possibility is to do what @dfeuer suggested and generate a vector of Fins, then map f over it:

fins : (n : Nat) -> Vect n (Fin n)
fins Z = []
fins (S n) = FZ :: map FS (fins n)

generate' : {n : Nat} -> (f : Fin n -> a) -> Vect n a
generate' f = map f $ fins _

Proving generate f = generate' f is left as en exercise to the reader.

4
votes

Cactus's answer appears to be about the best way to get what you asked for, but if you want something that can be used at runtime, it will be quite inefficient. The essential reason for this is that to weaken a Fin n to a Fin n+m requires that you completely deconstruct it to change the type of its FZ, and then build it back up again. So there can be no sharing at all between the Fin values produced for each vector element. An alternative is to combine a Nat with a proof that it is below a given bound, which leads to the possibility of erasure:

data NFin : Nat -> Type where
  MkNFin : (m : Nat) -> .(LT m n) -> NFin n

lteSuccLeft : LTE (S n) m -> LTE n m
lteSuccLeft {n = Z} prf = LTEZero
lteSuccLeft {n = (S k)} {m = Z} prf = absurd (succNotLTEzero prf)
lteSuccLeft {n = (S k)} {m = (S j)} (LTESucc prf) = LTESucc (lteSuccLeft prf)

countDown' : (m : Nat) -> .(m `LTE` n) -> Vect m (NFin n)
countDown' Z mLTEn = []
countDown' (S k) mLTEn = MkNFin k mLTEn :: countDown' k (lteSuccLeft mLTEn)

countDown : (n : Nat) -> Vect n (NFin n)
countDown n = countDown' n lteRefl

countUp : (n : Nat) -> Vect n (NFin n)
countUp n = reverse $ countDown n

generate : (n : Nat) -> (NFin n -> a) -> Vect n a
generate n f = map f (countUp n)

As in the Fin approach, the function you pass to generate does not need to work on all naturals; it only needs to handle ones less than n.

I used the NFin type to explicitly indicate that I want the LT m n proof to be erased in all cases. If I didn't want/need that, I could just use (m ** LT m n) instead.