https://www.fpcomplete.com/user/edwardk/fibonacci/leonardo

leonardo.hs

{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, GADTs, StandaloneDeriving, ScopedTypeVariables, Rank2Types, PolyKinds, DeriveTraversable #-}
import Unsafe.Coerce
import GHC.TypeLits
import Data.Type.Equality
import Data.Proxy
import Prelude hiding (drop)
import Data.Foldable

data Tree :: Nat -> Nat -> * -> * where
  Bin :: a -> Tree i j a -> Tree j k a -> Tree k (1 + j + k) a
  Tip :: a -> Tree 1 1 a

deriving instance Show a => Show (Tree i j a)
deriving instance Functor (Tree i j)
deriving instance Foldable (Tree i j)
deriving instance Traversable (Tree i j)

data Leonardo a where
  Cons :: !(ANat i) -> !(ANat j) -> Tree i j a -> Leonardo a -> Leonardo a
  Nil :: Leonardo a

deriving instance Show a => Show (Leonardo a)
deriving instance Functor Leonardo
deriving instance Foldable Leonardo
deriving instance Traversable Leonardo

infixr 5 <|

(<|) :: a -> Leonardo a -> Leonardo a
a <| Cons _ j s (Cons j' k t z)
  | Just r@Refl <- eqANat j j' = Cons k l (Bin a s t) z
  where
    l = (aNat :: ANat 1) `plusANat` j `plusANat` k
a <| z = Cons aNat aNat (Tip a) z
{-# NOINLINE (<|) #-} -- for debugging

fromList :: [a] -> Leonardo a
fromList = foldr (<|) Nil

ix :: forall f a. Applicative f => Int -> (a -> f a) -> Leonardo a -> f (Leonardo a)
ix _ _ Nil = pure Nil
ix i f (Cons j k a as)
  | i < getANat k = fmap (\a' -> Cons j k a' as)
    (go i (prev (getANat j) (getANat k)) (getANat j) a)
  | otherwise = Cons j k a <$> ix (i - getANat k) f as
  where
    go :: Int -> Int -> Int -> Tree i j a -> f (Tree i j a)
    go 0 _ _ (Tip a) = Tip <$> f a
    go 0 _ _ (Bin a l r) = fmap (\a' -> Bin a' l r) (f a)
    go i j k (Bin a l r)
      | i <= j    = fmap (\l' -> Bin a l r) (go (i - 1) (prev2 j k) (prev j k) l)
      | otherwise = Bin a l <$> go (i - j - 1) (prev j k) j r

prev :: Int -> Int -> Int
prev i j = j - i - 1

prev2 :: Int -> Int -> Int
prev2 i j = 2 * i - j

-- | Alternative representation of @KnownNat n => Proxy n@
newtype ANat (i :: Nat) = UnsafeANat { getANat :: Int } deriving Show

eqANat :: ANat i -> ANat j -> Maybe (i :~: j)
eqANat (UnsafeANat i) (UnsafeANat j) | i == j = Just $ unsafeCoerce Refl
eqANat _ _ = Nothing
{-# INLINE eqANat #-}

aNat :: forall n. KnownNat n => ANat n
aNat = UnsafeANat $ fromIntegral $ natVal (Proxy :: Proxy n)
{-# INLINE aNat #-}

plusANat :: ANat m -> ANat n -> ANat (m + n)
plusANat = unsafeCoerce ((+) :: Int -> Int -> Int)
{-# INLINE plusANat #-}