DFinger.lhs

This module is inspired by 

   Claessen, Finger Trees Explained Anew, and Slightly Simplified (Functional Pearl)
   Haskell Symposium 2020

It is a reinterpretation of the FingerTree data structure using GADTs in place of nested datatypes.
The original version of the code is available [here](Finger.lhs).

> {-# LANGUAGE UndecidableInstances #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE DeriveTraversable #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE InstanceSigs #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE ScopedTypeVariables #-}
> {-# LANGUAGE StandaloneDeriving #-}
> {-# LANGUAGE TypeApplications #-}
> {-# LANGUAGE TypeInType #-}
> {-# LANGUAGE TypeFamilies #-}

> {-# OPTIONS_GHC -Wno-name-shadowing -Wno-unticked-promoted-constructors #-}


> module DFinger where
>
> import Prelude hiding (tail,head)
> import Data.Kind (Type)
> import Nat hiding (Some)

Two-Three Trees
---------------

We start by implementing 2-3 trees that statically track their height.  This
index ensures that the tree is balanced. All subtrees must have the exactly the
same height.

> -- two or three values
> data Tuple a = Pair a a | Triple a a a
>   deriving (Eq, Show, Functor, Foldable, Traversable)

> -- A two-three tree of height n, with values of type a at the leaves
> -- Natural numbers are defined in the [Nat](Nat.lhs) module.
> data TwoThree n a where
>    Leaf :: a -> TwoThree Z a
>    Node :: Tuple (TwoThree n a) -> TwoThree (S n) a

> deriving instance Show a => Show (TwoThree n a)
> deriving instance Eq a => Eq (TwoThree n a)
> deriving instance Functor (TwoThree n)
> deriving instance Foldable (TwoThree n)
> deriving instance Traversable (TwoThree n)

NOTE: A height 0 tree is just a single value.

Sequences / FingerTrees
-----------------------

We will use these 2-3 trees as the building block of FingerTrees. Here the `n`
parameter works in reverse of the 2-3 trees above: in each recursive call it
increases, allowing each subsequent level to use larger 2-3 trees at the argument
to the `Unit` data constructor.

> data Some a = One a | Two a a | Three a a a
>    deriving (Eq,Show, Foldable, Traversable, Functor)

> data Seq (n :: Nat) (a :: Type) where
>    Nil  :: Seq n a
>    Unit :: TwoThree n a -> Seq n a
>    More :: Some (TwoThree n a) -> Seq (S n) a -> Some (TwoThree n a) -> Seq n a

Compared to the original nested datatype version, the `Unit` and `Some`
 constructors takes n a `TwoThree n a` instead of an `a` and the recursive
 call to `Seq` increments the natural number.

> deriving instance Show a => Show (Seq n a)
> deriving instance Eq a => Eq (Seq n a)
> deriving instance Functor (Seq n)
> deriving instance Foldable (Seq n)
> deriving instance Traversable (Seq n)

> head :: Seq n a -> TwoThree n a
> head Nil = error "no head"
> head (Unit x) = x
> head (More (One x) _ _ ) = x
> head (More (Two x _) _ _) = x
> head (More (Three x _ _) _ _) = x

> tail :: Seq n a -> Seq n a
> tail Nil = error "no tail"
> tail (Unit _) = Nil
> tail (More (Three _ x y) q u) = More (Two x y) q u
> tail (More (Two _ x) q u) = More (One x) q u
> tail (More (One _ ) q u) = more0 q u
>
> more0 :: Seq (S n) a -> Some (TwoThree n a) -> Seq n a
> more0 q u =
>   case uncons q of
>     Just (Node (Pair x y), tq) -> More (Two x y) tq u
>     Just (Node (Triple x _ _), _tq) -> More (One x) (map1 chop q) u
>        where
>          chop :: TwoThree n a -> TwoThree n a
>          chop (Node (Triple _ y z)) = Node (Pair y z)
>     Nothing -> case u of
>                  (One y) -> Unit y
>                  (Two y z) -> More (One y) Nil (One z)
>                  (Three y z w) -> More (One y) Nil (Two z w)
    

> map1 :: (TwoThree n a -> TwoThree n a) -> Seq n a  -> Seq n a
> map1 _f Nil = Nil
> map1 f (Unit x) = Unit (f x)
> map1 f (More (One x) q u) = More (One (f x)) q u
> map1 f (More (Two x y) q u) = More (Two (f x) y) q u
> map1 f (More (Three x y z) q u) = More (Three (f x) y z) q u

> -- | Safer combination of head/tail
> uncons :: Seq n a -> Maybe (TwoThree n a, Seq n a)
> uncons Nil = Nothing
> uncons (Unit y) = Just (y,Nil)
> uncons (More (Three w x y) q u) = Just (w, More (Two x y) q u)
> uncons (More (Two w x) q u) = Just (w, More (One x) q u)
> uncons (More (One w) q u) = Just (w, more0 q u)


> -- add to the front
> cons :: TwoThree n a -> Seq n a -> Seq n a
> cons x Nil = Unit x
> cons x (Unit y) = More (One x) Nil (One y)
> cons x (More (One y) q u) = More (Two x y) q u
> cons x (More (Two y z) q u) = More (Three x y z) q u
> cons x (More (Three y z w) q u) = More (Two x y) (cons (Node (Pair z w)) q) u

> -- add to the back
> snoc :: Seq n a -> TwoThree n a -> Seq n a
> snoc Nil x = Unit x
> snoc (Unit y) x = More (One y) Nil (One x)
> snoc (More u q (One y)) x = More u q (Two y x)
> snoc (More u q (Two y z)) x = More u q (Three y z x)
> snoc (More u q (Three y z w)) x = More u (snoc q (Node (Pair z w))) (Two y x)


> toTuples :: [a] -> [Tuple a]
> toTuples [ ] = [ ]
> toTuples [x, y] = [Pair x y ]
> toTuples [x, y, z, w] = [Pair x y, Pair z w]
> toTuples (x : y : z : xs) = Triple x y z : toTuples xs
>
> toList :: Some (TwoThree n a) -> [TwoThree n a]
> toList (One x) = [x]
> toList (Two x y) = [x, y]
> toList (Three x y z) = [x,y,z]

> glue :: Seq n a -> [ TwoThree n a ] -> Seq n a -> Seq n a
> glue Nil as q2 = foldr cons q2 as
> glue q1 as Nil = foldl snoc q1 as
> glue (Unit x) as q2 = foldr cons q2 (x : as)
> glue q1 as (Unit y) = foldl snoc q1 (as ++ [y])
> glue (More u1 q1 v1) as (More u2 q2 v2) =
>   More u1 (glue q1 (map Node (toTuples (toList v1 ++ as ++ toList u2))) q2) v2

> 
> instance Semigroup (Seq n a) where
>   q1 <> q2 = glue q1 [] q2