{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DefaultSignatures          #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE FlexibleContexts           #-}

module Main where

--------------------------------------------------------------------------------
-- Simple generic programming (instant-generics-like library)
--------------------------------------------------------------------------------
data U a = UNIT | SUM (U a) (U a) | PRODUCT (U a) (U a) | REC a

-- GADT interpretation
data I :: U * -> * where
  Unit          :: I UNIT
  Inl           :: I a -> I (SUM a b)
  Inr           :: I b -> I (SUM a b)
  Product       :: I a -> I b -> I (PRODUCT a b)
  Rec           :: a -> I (REC a)

-- Class embedding types and their generic representation
class Generic (a :: *) where
  type Rep a :: U *
  from :: a -> I (Rep a)
  to   :: I (Rep a) -> a

-- Generic size on representations
class GSize (a :: U *) where
  gsize :: I a -> Int

instance GSize UNIT where
  gsize Unit = 0

instance (GSize a, GSize b) => GSize (SUM a b) where
  gsize (Inl x) = gsize x
  gsize (Inr x) = gsize x

instance (GSize a, GSize b) => GSize (PRODUCT a b) where
  gsize (Product a b) = gsize a + gsize b

instance (Size a) => GSize (REC a) where
  gsize (Rec x) = 1 + size x

-- Size on datatypes
class Size (a :: *) where
  size :: a -> Int
  default size :: (Generic a, GSize (Rep a)) => a -> Int
  size = gsize . from

instance (Size a) => Size [a] -- default
instance Size Char where size _ = 1 -- adhoc

-- Example encoding: lists
instance Generic [a] where
  type Rep [a] = SUM UNIT (PRODUCT (REC a) (REC [a]))
  from []    = Inl Unit
  from (h:t) = Inr (Product (Rec h) (Rec t))
  to (Inl Unit)                      = []
  to (Inr (Product (Rec h) (Rec t))) = h:t

-- Testing size
test1 = size "abc"

main = print test1