Idris 2中permute函数线性上下文类型检查异常原因咨询

问题背景 #

基于向量置换的需求编写了如下Idris 2代码，其中swap函数实现向量指定位置与首元素的交换，Swaps类型记录置换序列，permute函数应用置换序列到向量：

import Data.Vect
import Data.Fin

swap : (1 i : Fin (S n)) -> (1 xs : Vect (S n) a) -> Vect (S n) a
swap FZ     (x0 :: xs) = (x0 :: xs)
swap (FS i) (x0 :: xs) = go i xs
  where
    go : Fin k -> Vect k a -> Vect (S k) a
    go FZ     (x :: xs) = x :: x0 :: xs
    go (FS i) (x :: xs) =
      let (x' :: xs') = go i xs in
      x' :: x :: xs'

data Swaps : Nat -> Type where
  Nil  : Swaps 0
  Cons : Fin (S n) -> Swaps n -> Swaps (S n)

permute : (1 ss : Swaps n) -> (1 xs : Vect n a) -> Vect n a
permute [] xs = xs
permute (Cons i ss) xs =
  case swap i xs of
    x' :: xs' => x' :: permute ss xs'

报错信息 #

上述permute的写法无法通过类型检查，报错如下：

While processing right hand side of permute. Sorry, I can't find any elaboration which works. All errors:
     If Main.swap: Trying to use linear name xs in non-linear context.
     
     Shuffle:29:15--29:17
      25 | 
      26 | permute : (1 ss : Swaps n) -> (1 xs : Vect n a) -> Vect n a
      27 | permute [] xs = xs
      28 | permute (Cons i ss) xs =
      29 |   case swap i xs of

可行写法 #

若对permute第二个子句的xs先做模式匹配，再重构调用swap，则可通过类型检查：

permute : (1 ss : Swaps n) -> (1 xs : Vect n a) -> Vect n a
permute [] xs = xs
permute (Cons i ss) (x :: xs) =
  let (x' :: xs') = swap i (x :: xs) in x' :: permute ss xs'

问题解析 #

这是线性类型系统的固有约束，而非单纯的Idris 2实现限制，核心逻辑如下：

• 线性变量的核心规则：标注(1 xs : ...)的线性变量必须被恰好使用一次，既不能重复引用，也不能被丢弃。
• 未模式匹配的歧义：第一种写法中，xs作为未模式匹配的线性变量传入swap时，类型检查器无法明确验证xs被恰好消耗——它无法排除代码中存在其他隐式引用xs的可能，因此判定xs处于“非线性上下文”，违反线性约束。
• 模式匹配的明确性：对xs做(x :: xs)模式匹配后，相当于将线性变量的结构完全暴露给检查器。此时重构(x :: xs)并传递给swap，检查器可以清晰追踪到：原线性变量被完整拆解后重组，且仅被swap消耗一次，后续逻辑中没有额外引用，完全符合线性类型的使用规则，因此通过检查。

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