Idris中基于Fin而非Nat实现向量初始段函数的类型错误问题

Let's break down what's going wrong with your code and how to fix it step by step.

The Root Cause of the Type Error #

Your original return type Vect n (p ** Vect (finToNat p) t) has a critical mismatch:

• p is typed as Fin n, which means finToNat p can only produce values from 0 to n-1 (since Fin n represents natural numbers less than n).
• But your function is trying to return initial segments of lengths 1 through n—including the full vector of length n. To get a segment length of n, you need finToNat p = n, which is impossible with p : Fin n. This is why the type checker rejects your code.

The Corrected Code #

We need to adjust the return type to use Fin (S n) for p—this type allows p to take values from 0 to n, so finToNat p can cover all required segment lengths from 1 to n. Here's the fixed version:

vectorsInits : Vect n t -> Vect n (p : Fin (S n) ** Vect (finToNat p) t)
vectorsInits Nil = Nil
vectorsInits (x::xs) = 
  ((FS FZ) ** (x::Nil)) :: map (\(p ** ys) => ((FS p) ** x::ys)) (vectorsInits xs)

Why This Works #

Let's verify the type consistency for the recursive case:

1. When processing x::xs (a vector of length S len), vectorsInits xs returns a Vect len (p : Fin (S len) ** Vect (finToNat p) t).
2. The map function transforms each element (p ** ys) to (FS p ** x::ys):
   • FS p converts a Fin (S len) to Fin (S (S len)), which is exactly Fin (S n) (since n = S len).
   • x::ys has length S (finToNat p), which equals finToNat (FS p)—perfectly matching the vector length required by the dependent pair.
3. The first element ((FS FZ) ** (x::Nil)) has p : Fin (S n) (since FS FZ is Fin (S (S len))) and a vector length of 1, which is finToNat (FS FZ).

All types now align correctly, satisfying the type checker.

Example Usage #

For a vector [1,2,3] : Vect 3 Int, the function will return:

[ (FS FZ ** [1]), 
  (FS (FS FZ) ** [1,2]), 
  (FS (FS (FS FZ)) ** [1,2,3]) ]

Each element's p is a Fin 4 (since S n = 4), and finToNat p gives the exact length of the corresponding initial segment.

内容的提问来源于stack exchange，提问作者Robert Kirk