在 Idris 中，如何编写一个 "vect generator" 函数，该函数在参数中采用索引函数

Question

我正在尝试在 Idris 中编写一个函数，该函数通过传递 Vect 的大小和一个在参数中采用索引的函数来创建 Vect。到目前为止，我有这个：

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

但我想确保传入参数的函数只采用小于 Vect 大小的索引。我试过了：

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

但它没有编译错误

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

我的问题是：我想做的事情是否可行以及如何实现？

Answer 1

关键思想是向量的第一个元素是f 0，对于尾部，如果你有k : Fin n，那么FS k : Fin (S n)就是一个"shift"同时增加其值和类型的有限数字。

利用这个观察结果，我们可以将 generate 重写为

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

另一种可能性是按照@dfeuer 的建议生成一个 Fin 的向量，然后将 f 映射到它上面：

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 _

证明 generate f = generate' f 留作 reader 的练习。

Answer 2

Cactus 的答案似乎是获得您所要求的最佳方式，但如果您想要可以在运行时使用的东西，那将是非常低效的。其本质原因是，将 Fin n 弱化为 Fin n+m 需要您完全解构它以更改其 FZ 的类型，然后重新构建它。因此，为每个向量元素生成的 Fin 值之间根本没有共享。另一种方法是将 Nat 与它低于给定界限的证明结合起来，这会导致擦除的可能性：

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)

与 Fin 方法一样，您传递给 generate 的函数不需要对所有自然数起作用；它只需要处理小于 n.

的

我使用 NFin 类型明确表示我希望在所有情况下都删除 LT m n 证明。如果我没有 want/need 那个，我可以用 (m ** LT m n) 代替。

在 Idris 中，如何编写一个 "vect generator" 函数，该函数在参数中采用索引函数

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

dependent-type

idris