{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DeriveGeneric #-}

-- Output algebra notation of algebraic data types.
-- E.g., "data T = A | B Int T"
-- then alg (Proxy :: Proxy T) = "T = 1 + Int * T"

module AlgebraOfType where

import Data.Proxy
import Data.Typeable
import GHC.Generics

class GAlg (f :: k -> *) where
    galg :: p f -> String

instance Typeable t => GAlg (K1 i t) where
    galg _ = show (typeRep (Proxy :: Proxy t))

instance GAlg U1 where
    galg _ = "1"

instance GAlg V1 where
    galg _ = "0"

instance (GAlg f, GAlg g) => GAlg ((:*:) f g) where
    galg _ = galg (Proxy :: Proxy f) ++ " * " ++ galg (Proxy :: Proxy g)

instance (GAlg f, GAlg g) => GAlg ((:+:) f g) where
    galg _ = galg (Proxy :: Proxy f) ++ " + " ++ galg (Proxy :: Proxy g)

instance GAlg f => GAlg (M1 i c f) where
    galg _ = galg (Proxy :: Proxy f)

class Alg a where
    alg :: p a -> String
    default alg :: (Generic a, Typeable a, GAlg (Rep a)) => p a -> String
    alg p = show (typeRep (Proxy :: Proxy a))
            ++ " = "
            ++ galg (Proxy :: Proxy (Rep a))

data T = A | B Int T
    deriving (Generic, Show)

instance Alg T

instance Typeable a => Alg [a]