How to shuffle a list i agda?

Question

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) = ?

Answer 1

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.