So I told my (non-Haskeller) friends about Morte and how it promises that programs with identical semantics have identical performance. They immediately replied: “How is that possible, if we have different sorting algorithms with the same semantics but different asymptotic performance”. I replied: “Either it is impossible to write a sorting algorithm in Morte, or they all have the same performance”. Looking back I now understand that identical semantics here means identical semantics as provable by equational reasoning and that there might be other notions of identical semantics where programs with identical semantics can have different performance.
Anyway, I challenged myself to write a sorting algorithm in Morte to see what’s going on. As a first step I had to find a non-recursive Haskell sorting algorithm. This is what the rest of this post is about. I then plan to translate it to Morte.
Let’s first introduce the standard F-Algebra and F-Coalgebra machinery. Why? Because Gabriel suggest to implement recursion with an algebra and corecursion with a coalgebra. A little generalization doesn’t hurt.
data Fix f = In {out :: f (Fix f)}
fold :: (Functor f) => (f x -> x) -> Fix f -> x
fold alg = alg . fmap (fold alg) . out
wrap :: f (Fix f) -> Fix f
wrap = In
unfold :: (Functor g) => (s -> g s) -> s -> Fix g
unfold coalg = In . fmap (unfold coalg) . coalg
unwrap :: Fix g -> g (Fix g)
unwrap = out
But these standard definitions for Fix, fold and unfold are recursive. This will not do.
The non-recursive version encodes the least fix point Mu as the ability to fold and the greatest fix point Nu as the ability to unfold. Mu uses universal quantification and Nu uses existential quantification. wrap folds the inner data and then applies the given algebra one more time. unwrap applies the coalgebra once and then proceeds to unfold with the new seed.
data Mu f = Mu (forall x . (f x -> x) -> x)
fold :: (f x -> x) -> Mu f -> x
fold alg (Mu mu) = mu alg
wrap :: (Functor f) => f (Mu f) -> Mu f
wrap layer = Mu (\alg -> alg (fmap (fold alg) layer))
data Nu g = forall s . Nu (s -> g s) s
unfold :: (s -> g s) -> s -> Nu g
unfold coalg s = Nu coalg s
unwrap :: (Functor g) => Nu g -> g (Nu g)
unwrap (Nu coalg s) = fmap (unfold coalg) (coalg s)
We then have different types for lists and streams that both share the same underlying Functor called L.
data L a x = Empty | Cons a x deriving (Functor)
type List a = Mu (L a)
type Stream a = Nu (L a)
The actual sorting algorithm is from this paper about sorting with folds and unfolds. It does a better job at explaining it than I could do here so I’ll just give you the definitions for insertion sort and selection sort.
insertionSort :: (Ord a) => List a -> Stream a
insertionSort = fold insert
insert :: (Ord a) => L a (Stream a) -> Stream a
insert = unfold (swap . fmap unwrap)
selectionSort :: (Ord a) => List a -> Stream a
selectionSort = unfold select
select :: (Ord a) => List a -> L a (List a)
select = fold (fmap wrap . swap)
swap :: (Ord a) => L a (L a x) -> L a (L a x)
swap Empty = Empty
swap (Cons a Empty) = Cons a Empty
swap (Cons a1 (Cons a2 x)) = if a1 <= a2
then Cons a1 (Cons a2 x)
else Cons a2 (Cons a1 x)
If we translate the definitions for insertion sort and for selection sort to Morte, will they be identical?
