Typelevel quicksort (and integer arithmetic) in Julia

typesort.jl

#!/usr/bin/env julia

# Peano arithmetic (https://en.wikipedia.org/wiki/Peano_axioms)
abstract Natural <: Integer
immutable Zero <: Natural end
immutable Successor{P<:Natural} <: Natural end

# Define a total order relation
<(::Type{Zero}, ::Type{Zero}) = false
<{P<:Natural}(::Type{Zero}, ::Type{Successor{P}}) = true
<{P<:Natural}(::Type{Successor{P}}, ::Type{Zero}) = false
<{P1<:Natural, P2<:Natural}(::Type{Successor{P1}}, ::Type{Successor{P2}}) = P1 < P2

# A linked list
abstract Node
immutable Nil <: Node end
immutable Cell{N<:Natural, Next<:Node} <: Node end

# Note: ^ is cons, because it's right-associative
(^){N<:Natural, C<:Node}(::Type{N}, ::Type{C}) = Cell{N, C}
(^){N<:Natural}(::Type{Nil}, ::Type{N}) = Cell{N2, Nil}
(^){N1<:Natural, N2<:Natural, C<:Node}(::Type{Cell{N1, C}}, ::Type{N2}) = Cell{N1, C ^ N2}

# List concat
(^)(::Type{Nil}, ::Type{Nil}) = Nil
(^){C<:Node}(::Type{Nil}, ::Type{C}) = C
(^){C<:Node}(::Type{C}, ::Type{Nil}) = C
(^){N1<:Natural, N2<:Natural, C1<:Node, C2<:Node}(::Type{Cell{N1, C1}}, ::Type{Cell{N2, C2}}) = Cell{N1, C1^N2^C2}

partition{Pivot<:Natural}(::Type{Nil}, ::Type{Pivot}) = (Nil, Nil)
partition{N<:Natural, Pivot<:Natural, Next<:Node}(::Type{Cell{N, Next}}, ::Type{Pivot}) = begin
    LT, GT = partition(Next, Pivot)
    N < Pivot ? (N ^ LT, GT) : (LT, N ^ GT)
end

sort(::Type{Nil}) = Nil
sort{N<:Natural, C<:Node}(::Type{Cell{N, C}}) = begin
    LT, GT = partition(C, N)
    sort(LT) ^ N ^ sort(GT)
end


# Bonus: Arithmetic on the type system
+(::Type{Zero}, ::Type{Zero}) = Zero
+{P<:Natural}(::Type{Zero}, ::Type{Successor{P}}) = Successor{P}
+{P<:Natural}(::Type{Successor{P}}, ::Type{Zero}) = Successor{P}
+{P1<:Natural, P2<:Natural}(::Type{Successor{P1}}, ::Type{P2}) = P1 + Successor{P2}

*(::Type{Zero}, ::Type{Zero}) = Zero
*{P<:Natural}(::Type{Zero}, ::Type{Successor{P}}) = Zero
*{P<:Natural}(::Type{Successor{P}}, ::Type{Zero}) = Zero
*{P1<:Natural, P2<:Natural}(::Type{Successor{P1}}, ::Type{Successor{P2}}) = Successor{P2} + P1 * Successor{P2}

^(::Type{Zero}, ::Type{Zero}) = error("Cannot into 0^0 :(")
^{N<:Natural}(::Type{Zero}, ::Type{N}) = Zero
^{N<:Natural}(::Type{N}, ::Type{Zero}) = Successor{Zero}
^{P1<:Natural, P2<:Natural}(::Type{Successor{P1}}, ::Type{Successor{P2}}) = Successor{P1} * Successor{P1} ^ P2

# conversion and construction
Base.int(::Type{Zero}) = 0
Base.int{N<:Natural}(::Type{Successor{N}}) = 1 + int(N)
natural(n::Integer) = n == 0 ? Zero : Successor{natural(n - 1)}

# making the list iterable
Base.start{C<:Node}(::Type{C}) = C
Base.done{Cs<:Node, N<:Natural, C<:Node}(::Type{Cs}, ::Type{Cell{N, C}}) = false
Base.done{Cs<:Node}(::Type{Cs}, ::Type{Nil}) = true
Base.next{N<:Natural, Cs<:Node, C<:Node}(::Type{Cs}, ::Type{Cell{N, C}}) = (N, C)

_0 = Zero
_1 = Successor{_0}
_2 = Successor{_1}
_3 = Successor{_2}
_4 = Successor{_3}
_5 = Successor{_4}
list = _4 ^ _5 ^ _3 ^ _1 ^ _2 ^ _0 ^ Nil

function main()
    println("List:")
    for n in list
        println(n)
    end
    println("Sorted:")
    for n in sort(list)
        println(n)
    end
end
main()