Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Typelevel quicksort (and integer arithmetic) in Julia
#!/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()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment