Finger trees without polymorphic recursion

finger_tree_gadt.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
module FingerTree where

import Data.Kind (Type)

data Nat = Z | S Nat

data Digit n a
  = One (Tree n a)
  | Two (Tree n a) (Tree n a)
  | Three (Tree n a) (Tree n a) (Tree n a)
  | Four (Tree n a) (Tree n a) (Tree n a) (Tree n a)

data Node n a
  = Node2 (Tree n a) (Tree n a)
  | Node3 (Tree n a) (Tree n a) (Tree n a)

-- Two-three tree with values at leaves.
data Tree :: Nat -> Type -> Type where
  TreeZero :: a -> Tree 'Z a
  TreeSucc :: Node n a -> Tree ('S n) a

data FingerTreeN :: Nat -> Type -> Type where
  Empty :: FingerTreeN n a
  Single :: Tree n a -> FingerTreeN n a
  Deep :: Digit n a -> FingerTreeN ('S n) a -> Digit n a -> FingerTreeN n a

newtype FingerTree a = FingerTree (FingerTreeN 'Z a)

finger_tree_polymorphic_recursion.hs

module FingerTree where

data Digit a
  = One a
  | Two a a
  | Three a a a
  | Four a a a a

data Node a = Node2 a a | Node3 a a a

data FingerTree a
  = Empty
  | Single a
  | Deep (Digit a) (FingerTree (Node a)) (Digit a)