A short gist showing how we can encode the correctness of a sorting algorithm through Idris2's type system. We define a structure to track the correct ordering of the output, and use lienarity to ensure that the output is a permutation of the input.

isort.idr

module ISort

import Data.Linear.Interface
import Data.Linear.Notation
import Data.Linear.LNat
import Data.Linear.LEither
import Data.Linear.LMaybe
import Data.Linear.LVect

-- Some useful things defined for LNats

-- Comparisons between linear nats
infix 5 <@

public export
(<@) : LNat -@ LNat -@ Bool
(<@) Zero Zero = False
(<@) Zero (Succ y) = y `seq` True
(<@) (Succ x) Zero = x `seq` False
(<@) (Succ x) (Succ y) = x <@ y

public export
fromNat : Nat -> LNat
fromNat 0 = Zero
fromNat (S k) = Succ (fromNat k)

public export
Num LNat where
    (+) Zero y = y
    (+) (Succ x) y = Succ (x + y)

    (*) Zero y = y
    (*) (Succ x) y = y + (x * y)

    fromInteger i = fromNat $ integerToNat i

public export
lnatToInteger : LNat -> Integer
lnatToInteger Zero = 0
lnatToInteger (Succ x) = 1 + lnatToInteger x

prim__integerToLNat : Integer -> LNat
prim__integerToLNat i
  = if intToBool (prim__lte_Integer 0 i)
      then believe_me i
      else Zero

public export
integerToLNat : Integer -> LNat
integerToLNat 0 = Zero -- Force evaluation and hence caching of x at compile time
integerToLNat x
  = if intToBool (prim__lte_Integer x 0)
       then Zero
       else Succ (assert_total (integerToLNat (prim__sub_Integer x 1)))


public export
Show LNat where
    show n = show (the Integer (lnatToInteger n))

-- Proofs about LNats
-- LTE etc copied from the Nat implementation
public export
data LTE  : (1 n : LNat) -> (1 m : LNat) -> Type where
  LTEZero : LTE Zero    right
  LTESucc : LTE left right -> LTE (Succ left) (Succ right)

public export
GTE : LNat -@ LNat -@ Type
GTE left right = LTE right left

public export
LT : LNat -@ LNat -@ Type
LT left right = LTE (Succ left) right

namespace LT
  ||| LT is defined in terms of LTE which makes it annoying to use.
  ||| This convenient view of allows us to avoid having to constantly
  ||| perform nested matches to obtain another LT subproof instead of
  ||| an LTE one.
  public export
  data View : LT m n -> Type where
    LTZero : View (LTESucc LTEZero)
    LTSucc : (lt : m `LT` n) -> View (LTESucc lt)

  ||| Deconstruct an LT proof into either a base case or a further *LT*
  export
  view : (lt : LT m n) -> View lt
  view (LTESucc LTEZero) = LTZero
  view (LTESucc lt@(LTESucc _)) = LTSucc lt

  ||| A convenient alias for trivial LT proofs
  export
  ltZero : Zero `LT` Succ m
  ltZero = LTESucc LTEZero

public export
GT : LNat -@ LNat -@ Type
GT left right = LT right left

export
succNotLTEzero : Not (LTE (Succ m) Zero)
succNotLTEzero LTEZero impossible

export
fromLteSucc : LTE (Succ m) (Succ n) -> LTE m n
fromLteSucc (LTESucc x) = x

export
succNotLTEpred : {x : LNat} -> Not $ LTE (Succ x) x
succNotLTEpred {x =   Zero} prf = succNotLTEzero prf
succNotLTEpred {x = Succ _} prf = succNotLTEpred $ fromLteSucc prf

public export
isLTE : (1 m : LNat) -> (1 n : LNat) -> Dec (LTE m n)
isLTE Zero n = consume n `seq` Yes LTEZero
isLTE (Succ k) Zero = consume k `seq` No succNotLTEzero
isLTE (Succ k) (Succ j)
    = case isLTE k j of
           No contra => No (contra . fromLteSucc)
           Yes prf => Yes (LTESucc prf)

public export
isLTEBool : (1 m : LNat) -> (1 n : LNat) -> Bool
isLTEBool m n = case isLTE m n of
                     (Yes prf) => True
                     (No contra) => False

public export
isLT : (1 m : LNat) -> (1 n : LNat) -> Dec (LT m n)
isLT m n = isLTE (Succ m) n

public export
isGT :  (1 m : LNat) -> (1 n : LNat) -> Dec (GT m n)
isGT m n = isLT n m


export
lteSuccRight : LTE n m -> LTE n (Succ m)
lteSuccRight LTEZero     = LTEZero
lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)

export
lteSuccLeft : LTE (Succ n) m -> LTE n m
lteSuccLeft (LTESucc x) = lteSuccRight x

export
lteAddRight : (n : LNat) -> LTE n (n + m)
lteAddRight Zero = LTEZero
lteAddRight (Succ k) {m} = LTESucc (lteAddRight {m} k)

export
notLTEImpliesGT : {a, b : LNat} -> Not (a `LTE` b) -> a `GT` b
notLTEImpliesGT {a = Zero  }           not_z_lte_b    = absurd $ not_z_lte_b LTEZero
notLTEImpliesGT {a = Succ a} {b = Zero  } notLTE = LTESucc LTEZero
notLTEImpliesGT {a = Succ a} {b = Succ k} notLTE = LTESucc (notLTEImpliesGT (notLTE . LTESucc))

infix 1 ##

-- Dependent pair of linear and linear
public export
record DPairLL (t : Type) (f : t -> Type) where
  constructor (##)
  1 fst : t
  1 snd : f fst

public export
isLinLTE : (1 m : LNat) -> (1 n : LNat) -> DPairLL LNat (\x => DPairLL LNat (\y => (Dec $ LTE x y, x === m, y === n)))
isLinLTE Zero n = Zero ## (n ## (Yes LTEZero, Refl, Refl))
isLinLTE (Succ x) Zero = (Succ x) ## (Zero ## (No succNotLTEzero, Refl, Refl))
isLinLTE (Succ x) (Succ z) = case isLinLTE x z of
                                  (x ## (y ## (Yes prf, Refl, Refl))) => (Succ x ## (Succ y ## (Yes (LTESucc prf), Refl, Refl)))
                                  (x ## (y ## (No contra, Refl, Refl))) => (Succ x ## (Succ y ## (No (contra . fromLteSucc), Refl, Refl)))

-- Stuff with sorted vectors.
data LSortedVect : Nat -> LNat -> Type where
    Nil : (1 e : LNat) -> LSortedVect 1 e
    Cons : (1 e : LNat) -> (1 es : LSortedVect n o) -> (0 prf : LTE e o) -> LSortedVect (S n) e

-- Hints for interactive editing
%name LSortedVect xs, ys, zs, ws, es, ms

Show (LSortedVect l m) where
    show sv = "[" ++ printSortedVect sv where
        printSortedVect : LSortedVect n e -> String
        printSortedVect ([] e) = (show e) ++ "]"
        printSortedVect (Cons e es prf) = (show e) ++ "," ++ printSortedVect es

Show (DPairLL LNat (\m => LSortedVect l m)) where
    show (_ ## snd) = show snd


-- Given a proof of Not (n <= m), produce a proof of m <= n
flipOrdContra : {n, m : LNat} -> Not (LTE n m) -> LTE m n
flipOrdContra f = lteSuccLeft $ notLTEImpliesGT f

-- Insert a new element into a sorted Vector.
-- Returns back a vector one element longer, with either the smallest element being `x`, or remaining unchanged.
insert : (1 x : LNat) -> (1 xs : LSortedVect l m) -> LEither (LSortedVect (S l) x) (LSortedVect (S l) m)
insert x ([] m) = case isLinLTE x m of
                       (x ## (m ## (Yes prf, Refl, Refl))) => Left $ Cons x (Nil m) prf
                       (x ## (m ## (No contra, Refl, Refl))) => Right $ Cons m (Nil x) (flipOrdContra contra)
insert x (Cons m ms p) = case isLinLTE x m of
                                (x ## (m ## ((Yes prf), (Refl, Refl)))) => Left $ Cons x (Cons m ms p) prf
                                (x ## (m ## ((No contra), (Refl, Refl)))) => case insert x ms of
                                                                                  (Left ms') => Right (Cons m ms' (flipOrdContra contra))
                                                                                  (Right ms') => Right (Cons m ms' p)

isort : (xs : LVect (S n) LNat) -> DPairLL LNat (\m =>LSortedVect (S n) m)
isort (x :: []) = (x ## Nil x)
isort (x :: (y :: xs)) = let (m' ## sv) = isort (y :: xs) in
    case insert x sv of
        (Left z) => x ## z
        (Right z) => m' ## z

sortedVector = isort [41, 2, 6, 3, 7, 3, 9, 11, 13, 29]