Concatenative Combinators

concatenative.lhs

> {-# LANGUAGE DataKinds, TypeOperators, GADTs #-}

> data Stack xs where
>   Empty :: Stack '[]
>   Push :: x -> Stack xs -> Stack (x ': xs)

> pop :: Stack (x ': xs) -> Stack xs
> pop (Push _ s) = s

> peek :: Stack (x ': xs) -> x
> peek (Push x _) = x

> dup :: Stack (x ': xs) -> Stack (x ': x ': xs)
> dup (Push x s) = Push x $ Push x s

> swap :: Stack (x ': y ': xs) -> Stack (y ': x ': xs)
> swap (Push x (Push y s)) = (Push y $ Push x s)

> unit :: Stack (x ': s) -> Stack (Stack '[x] ': s)
> unit (Push x s) = Push (Push x Empty) s

> isEmpty :: Stack xs -> Bool
> isEmpty Empty = True
> isEmpty _ = False

> data Uniform x xs where
>   Zero :: Uniform x '[]
>   Succ :: Uniform x xs -> Uniform x (x ': xs)

> _1 = Succ $ Zero
> _2 = Succ $ Succ $ Zero
> _3 = Succ $ Succ $ Succ $ Zero
> _4 = Succ $ Succ $ Succ $ Succ $ Zero
> _5 = Succ $ Succ $ Succ $ Succ $ Succ $ Zero

> toList :: Uniform x xs -> Stack xs -> [x]
> toList _ Empty = []
> toList (Succ w) (Push x s) = (x : toList w s)

> insertWith :: (x -> x -> Bool) -> Uniform x xs -> x -> Stack xs -> Stack (x ': xs)
> insertWith p _ x Empty = Push x Empty
> insertWith p (Succ w) x (Push y s) =
>   if p x y 
>     then Push x $ Push y s 
>     else Push y $ insertWith p w x s

> insert :: (Ord x) => Uniform x xs -> x -> Stack xs -> Stack (x ': xs)
> insert = insertWith (<)

> sort :: (Ord x) => Uniform x xs -> Stack xs -> Stack xs
> sort _ Empty = Empty
> sort (Succ w) (Push x s) = insert w x (sort w s)

> sorted = toList _5 $ sort _5 $ Push 1 $ Push 5 $ Push 2 $ Push 4 $ Push 3 $ Empty