Strangest program I ever wrote #10001 (Nested datatypes)

I've been looking at nested datatypes to see if they would have some benefit for simplifying beam grouping, maybe they would but they are pretty complicated in themselves.

Here's a List nested datatype with just fmap and length operations, it took a lot of head scratching to get this far:

{-# LANGUAGE TypeSynonymInstances       #-}
{-# OPTIONS -Wall #-}

-- Hinze,   Manufacturing Datatypes      page 9
-- Okasaki, From Fast Exponentiation ... page 30 


module List where

import Data.Char ( chr )                -- for tests
import Prelude hiding ( length )

type Vector       = Vector' ()
data Vector' t a  = Zero t 
                  | Succ (Vector' (a,t) a)
  deriving (Eq,Show)

type List = Vector


list00 :: List Int
list00 = Zero ()

list01 :: List Int
list01 = Succ (Zero (1, ()))

list02 :: List Int
list02 = Succ (Succ (Zero (1, (2, ())))) 

list03 :: List Int
list03 = Succ (Succ (Succ (Zero (1, (2, (3, ()))))))



mapL :: (a -> b) -> List a -> List b
mapL = mapV ()


-- Perform the map by destructing the list, applying f to the 
-- /head/ and recurvisely working on the tail, then consing the 
-- structure back into shape.
--
-- The initial value for /Zero/ needs to be supplied as a 
-- parameter.
--

mapV :: t -> (a -> b) -> Vector' t a -> Vector' t b
mapV t0 f xs = let ans = desV xs in
               case ans of
                 Nothing -> Zero t0 
                 Just (a,rest) -> consV (f a) (mapV t0 f rest)


instance Functor List where
  fmap = mapV ()


length :: Vector a -> Int
length = lengthV

lengthV :: Vector' t a -> Int
lengthV (Zero _)  = 0
lengthV (Succ xs) = 1 + lengthV xs


cons :: a -> List a -> List a
cons a xs = consV a xs

consV :: a -> Vector' t a -> Vector' t a
consV a (Zero b)  = Succ (Zero (a, b))
consV a (Succ xs) = Succ (consV a xs)

list04 :: List Int
list04 = cons 0 list03

-- Helps to have a destructor...

des :: List a -> Maybe (a, List a)
des = desV

desV :: Vector' t a -> Maybe (a, Vector' t a)
desV (Zero _)             = Nothing
desV (Succ (Zero (a,bs))) = Just (a, Zero bs)
desV (Succ xs)            = case desV xs of
                              Nothing -> Nothing 
                              Just (a,xs') -> Just (a, Succ xs')

list05 :: List Char
list05 = fmap (chr . (+64)) list04