A simple translation of the format combinators used in The Power of Pi (http://www.staff.science.uu.nl/~swier004/Publications/ThePowerOfPi.pdf)

Format.hs

{-# LANGUAGE EmptyDataDecls, ExistentialQuantification, RankNTypes, GADTs, ImplicitParams, TypeFamilies, DataKinds, TypeOperators, DeriveGeneric, PolyKinds #-}
module Format where

import Prelude hiding (read)
import Data.Either
import Data.Binary.Get
import Data.Binary.Builder
import Data.Monoid
import Data.Foldable
import Control.Applicative
import Control.Monad
import Data.Word
import Data.Int

data Void

newtype K a b = K { unK :: a }
data Exists f = forall a. Exists { getValue :: f a }
data Sigma f = forall a. Sigma { tag :: f a, value :: a}

data Pickler a = Pickler { get :: Get a, put :: a -> Builder }

bad :: Pickler Void
bad = Pickler (fail "bad") (const $ error "unpossible")

end :: Pickler ()
end = Pickler (pure ()) (const mempty)

plus :: Pickler a -> Pickler b -> Pickler (Either a b)
plus (Pickler ga pa) (Pickler gb pb) = Pickler ((Left <$> ga) <|> (Right <$> gb)) (either pa pb)

skip :: Pickler a -> a -> Pickler b -> Pickler b
skip (Pickler ga pa) a (Pickler gb pb) = Pickler (ga *> gb) (\b -> pa a <> pb b)

read :: Pickler (Exists f) -> (forall a. f a -> Pickler a) -> Pickler (Sigma f)
read (Pickler gf pf) f = Pickler (getter gf f) (\(Sigma tag value) -> pf (Exists tag) <> put (f tag) value)
  where
  getter :: Get (Exists f) -> (forall a. f a -> Pickler a) -> Get (Sigma f)
  getter gf f = do
    Exists t <- gf
    v <- get (f t)
    return $ Sigma t v

-- I could do this safely with Vec...
rep :: Int -> Pickler a -> Pickler [a]
rep n (Pickler ga pa) = Pickler (replicateM n ga) (\xs -> if length xs == n then foldMap pa xs else error "argh")





word8 :: Pickler Word8
word8 = Pickler getWord8 singleton

bool :: Pickler Bool
bool = Pickler (toEnum . fromIntegral <$> getWord8) (singleton . fromIntegral . fromEnum)

char :: Pickler Char
char = Pickler (toEnum . fromIntegral <$> getWord32be) (putWord32be . fromIntegral . fromEnum)

wrap :: Pickler a -> Pickler (Exists (K a))
wrap (Pickler ga pa) = Pickler (Exists . K <$> ga) (\(Exists (K x)) -> pa x)


-- len || a random bool || char * len
--test = read (wrap word8) (\(K len) -> undefined $ read (wrap bool) (\(K b) -> ?q len b))