How to shuffle a list i agda?

I would like to randomly shuffle a list in agda.

I thought about taking random n elements from the beginning and adding them to the end, but I couldn't get the random part to work from this approach.

Is this possible with pattern matching or do I really have to figure out random number generation?

Current state:

shuffle : {A : Set} -> List A -> List A
shuffle [] = []
shuffle (x ∷ []) = x ∷ []
shuffle (x ∷ x₁ ∷ xs) = ?

I think the straightforward way to implement Fisher-Yates shuffle is to use a monadic effect for generating random numbers:

open import Data.Nat
open import Data.Fin
open import Data.Vec
variable
A : Set _
open import Data.Product hiding (swap)
swap : ∀ {n} → Fin (suc n) → Vec A (suc n) → (A × Vec A n)
swap         zero    (x₀ ∷ xs) = x₀ , xs
swap {A = A} (suc i) (x₀ ∷ xs) = go i xs
where
go : ∀ {n} → Fin n → Vec A n → A × Vec A n
go zero    (x ∷ xs) = x , x₀ ∷ xs
go (suc i) (x ∷ xs) with go i xs
... | (x′ , xs′) = x′ , x ∷ xs′
open import Category.Monad
module Shuffle {M} (Mon : RawMonad M) (randomFin : ∀ {n} → M (Fin (suc n))) where
open RawMonad Mon
shuffle : ∀ {n} → Vec A n → M (Vec A n)
shuffle [] = pure []
shuffle {n = suc n} xs@(_ ∷ _) = do
k ← randomFin
let (x′ , xs′) = swap k xs
xs″ ← shuffle xs′
pure (x′ ∷ xs″)

So how do we produce random Fin ns? @mudri's comment points us to Data.Nat.PseudoRandom.LCG which suggests using step with a state of type ℕ, and using simple remainder by n to produce a Fin n:

module ShuffleState (step : ℕ → ℕ) where
open import Category.Monad.State
open RawMonadState (StateMonadState ℕ)
randomℕ : State ℕ ℕ
randomℕ = modify step ⊛> get
open import Data.Nat.DivMod
randomFin : ∀ {n} → State ℕ (Fin (suc n))
randomFin = (_mod _) <$> randomℕ
open Shuffle monad randomFin public

Example usage:

module _ where
open import Data.Nat.PseudoRandom.LCG
open ShuffleState (step glibc)
test : Vec (Fin 10) 10
test = proj₁ (shuffle (allFin 10) 0)

Note that this doesn't prove that the output is indeed a permutation of the input. If you need that, I think it's easier to change shuffle and swap to produce a permutation witness (e.g. like this) instead of operating on the input vector directly and proving it externally.

Edited to add:
In Idris 2 at least, we can prove that shuffle is linear in the shuffled vector by just using linear types where they matter:

import Data.Vect
import Data.Fin
swap : 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'
shuffle: Monad m => (randomFin : {k : _} -> m (Fin (S k))) => {n : _} -> (1 xs : Vect n a) -> m (Vect n a)
shuffle [] = pure []
shuffle (x::xs) = do
k <- randomFin
let (x' :: xs') = swap k (x :: xs)
xs'' <- shuffle xs'
pure (x' :: xs'')

Note the type of xs in the signature of shuffle. I think parametricity + linearity together here should be sufficiently convincing that shuffle indeed shuffles its input.