5

我正在尝试在 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)

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

4

2 回答 2

4

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

使用这个观察，我们可以重写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 的建议进行操作并生成Fins 的向量，然后对其进行映射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留给读者作为练习。

于 2015-05-11T01:50:51.697 回答
4

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

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在所有情况下都删除证明。如果我不想/不需要那个，我可以(m ** LT m n)改用。

于 2015-05-11T20:37:28.460 回答