Quickysort en Idris

Un algoritmo que me gusta mucho es el quicksort, porque es un algoritmo por demás claro. Ya he escrito lo fácil que es implementarlo en Erlang, Rust, haskell y lisp

Ahora le toca a Idris. Básicamente, el algoritmo toma un pivote y agrupa los menores que el pivote al principio y los mayores al final y aplica quicksort a estos dos grupos. Y si la lista es vacía o tiene un elemento, ya está ordenada. 

Vamos al código: 

quicksort : Ord a => List a -> List a

quicksort [] = []

quicksort (pivot :: xs) =

    quicksort (filter (<= pivot) xs)

    ++ [pivot] ++

    quicksort (filter (> pivot) xs)

¿Cómo sabemos que el resultado está realmente ordenado? En Idris podemos intentar expresar esa propiedad en el tipo.

Definimos qué significa “estar ordenado”. Por ejemplo, podemos crear una relación inductiva:

data Sorted : List Nat -> Type where

    Empty : Sorted []

    Single : Sorted [x]

    ...

Y acá empieza lo interesante: Sorted no es un booleano.

No hacemos:

isSorted : List Nat -> Bool

Estamos creando un tipo cuyos valores representan una prueba de que una lista está ordenada.

Conceptualmente:

Sorted [1, 2, 3, 4]

puede tener un valor.

Pero:

Sorted [3, 1, 4]

no debería poder construirse.

Entonces el objetivo final sería algo parecido a:

quicksort :

    (xs : List Nat) ->

    (result : List Nat ** Sorted result)

Es decir: Dame una lista y te devuelvo una lista junto con una prueba de que esa lista está ordenada.

QuickSort es bastante fácil de escribir. Demostrarlo no.

Porque cuando hacemos:

menores ++ [pivot] ++ mayores

no alcanza con demostrar que:

menores está ordenado;

mayores está ordenado.

También necesitamos demostrar que:

todos los elementos de menores <= pivot

y:

pivot < todos los elementos de mayores

Es decir, Idris nos obliga a hacer explícito algo que normalmente dejamos implícito en nuestra cabeza.

Y entonces?

Primero definimos qué significa que una lista esté ordenada:

data Sorted : List Nat -> Type where

  Empty  : Sorted []

  Single : Sorted [x]

  Cons   : LTE x y ->

           Sorted (y :: xs) ->

           Sorted (x :: y :: xs)

La parte interesante viene con la firma de quicksort:

quicksort :

  (xs : List Nat) ->

  (result : List Nat ** Sorted result)

Veamos el código completo: 

quicksort :

    (xs : List Nat) ->

    (result : List Nat ** Sorted result)

quicksort [] =

    ([] ** Empty)

quicksort (pivot :: xs) =

    let (left ** leftSorted) =

            quicksort (filter (<= pivot) xs)

        (right ** rightSorted) =

            quicksort (filter (> pivot) xs)

        result =

            left ++ [pivot] ++ right

    in

        (result ** ?proof)