{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}



module Serialization where

data Nat = Zero | Suc Nat



data family Frame (s :: [*]) (s' :: [*])

infixr :.

data Stack (s :: [*]) where
  Done :: Stack '[]
  (:.) :: Frame s s' -> Stack s' -> Stack s

data instance Frame (Bool ': s) s' where
  TrueS :: Frame (Bool ': s) s
  FalseS :: Frame (Bool ': s) s

data instance Frame (Nat ': s) s' where
  ZeroS :: Frame (Nat ': s) s
  SucS :: Frame (Nat ': s) (Nat ': s)

data instance Frame ((a,b) ': s) s' where
  PairS :: Frame ((a,b) ': s) (a ': b ': s)

data instance Frame ([a] ': s) s' where
  NilS :: Frame ([a] ': s) s
  ConsS :: Frame ([a] ': s) (a ': [a] ': s)


s :: Stack '[[(Nat,Bool)]]
s =
  ConsS :.
  PairS :.
  SucS :.
  ZeroS :.
  TrueS :.
  ConsS :.
  PairS :.
  ZeroS :.
  FalseS :.
  NilS :.
  Done