如何在Agda中实现列表随机打乱功能？

首先明确：只靠模式匹配不可能实现真正的随机打乱。模式匹配完全依赖输入的结构，输出是固定的——输入相同的列表，模式匹配写出的函数永远返回相同的结果，做不到随机的不确定性。

你的初始思路（从头部取n个元素移到尾部）如果n是固定值，那只是循环移位，不是随机；如果要n是随机值，就必须引入随机数生成逻辑。但Agda是纯函数式语言，纯函数的输出完全由输入决定，所以随机数生成必须依赖种子状态：把种子作为函数输入，每次生成随机数后返回新的种子，以此延续随机状态。

下面是基于Fisher-Yates洗牌算法的实现示例，这是纯函数环境下实现随机洗牌的标准方案：

首先定义简单的随机数生成器：

open import Data.Nat
open import Data.List
open import Data.Vec using (Vec; toList; fromList; lookup; updateAt)
open import Data.Product
open import Function

-- 随机数种子用自然数表示
Seed : Set
Seed = ℕ

-- 线性同余生成器（LCG）生成下一个种子
nextSeed : Seed → Seed
nextSeed s = (1103515245 * s + 12345) mod 2^31

-- 生成0到n-1之间的随机整数，返回新种子和结果
randInt : Seed → ℕ → Seed × ℕ
randInt s n = let s' = nextSeed s in (s', s' mod n)

然后实现针对Vec的洗牌（Vec支持随机访问，适合Fisher-Yates算法），再封装成List的洗牌函数：

-- 对Vec进行洗牌，返回新种子和洗牌后的Vec
shuffleVec : {A : Set} {n : ℕ} → Seed → Vec A n → Seed × Vec A n
shuffleVec {n = zero} s [] = (s , [])
shuffleVec {n = suc n} s (x ∷ xs) =
  let (s' , k) = randInt s (suc n)
      -- 交换第k个元素和第一个元素
      xs' = updateAt k (const x) xs
      (s'' , xs'') = shuffleVec s' xs'
  in (s'' , lookup k (x ∷ xs) ∷ xs'')

-- 针对List的洗牌函数，需要传入初始种子
shuffle : {A : Set} → Seed → List A → Seed × List A
shuffle s xs = let (s' , v) = shuffleVec s (fromList xs) in (s' , toList v)

关键说明 #

1. 纯函数的限制：必须传入种子，且每次洗牌会返回新的种子——这样后续的随机操作可以基于新的种子继续，保证随机性的延续。
2. Fisher-Yates算法：通过随机选取位置交换元素，递归处理剩余列表，是高效且无偏的洗牌算法，适合纯函数式实现。
3. 无种子的“伪随机”：如果不需要真随机，只是想生成任意排列，可以用非确定性的方式枚举所有可能排列，但这不是真正的随机，且实际使用中仍需要外部输入来选择具体排列。

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