IEnum.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wall #-}
module IEnum where

import Data.Type.Equality
import Data.Kind (Type, Constraint)

import Data.GADT.Compare
import Data.GADT.Show
import Data.Dependent.Sum
import Data.Functor.Classes
import Data.Some

-------------------------------------------------------------------------------
-- Class
-------------------------------------------------------------------------------

class Cata (ICode f) => IEnum f where
    type ICode f :: [Type]

    ifrom :: f a -> IRep (ICode f) a
    ito   :: IRep (ICode f) a -> f a

-------------------------------------------------------------------------------
-- Representation
-------------------------------------------------------------------------------

data family IRep (code :: [Type]) x :: Type
data instance IRep '[] x
data instance IRep (y ': xs) x where
    IHere  :: IRep (x ':  xs) x
    IThere :: IRep xs x -> IRep (y ': xs) x


-- N-ary Product as Family
data family NPF (f :: k -> Type) (code :: [k])
data instance NPF f '[]       = Nil
data instance NPF f (x ': xs) = f x ::* NPF f xs

infixr 4 ::*

-------------------------------------------------------------------------------
-- Cata
-------------------------------------------------------------------------------

class Cata (xs :: [Type]) where
    cata :: f '[] -> (forall z zs. Cata zs => f zs -> f (z ': zs)) -> f xs

instance Cata '[] where
    cata n _ = n

instance Cata xs => Cata (x ': xs) where
    cata n c = c (cata n c)

-------------------------------------------------------------------------------
-- Examples: Example type
-------------------------------------------------------------------------------

data Domain a where
    DomainInt  :: Domain Int
    DomainChar :: Domain Char

instance IEnum Domain where
    type ICode Domain = '[ Int, Char ]

    ifrom DomainInt = IHere
    ifrom DomainChar = IThere IHere

    ito IHere               = DomainInt
    ito (IThere IHere)      = DomainChar
    ito (IThere (IThere v)) = case v of {}

-------------------------------------------------------------------------------
-- Examples: GEq
-------------------------------------------------------------------------------

genericGeq :: forall a b f. IEnum f => f a ->  f b -> Maybe (a :~: b) 
genericGeq = \x y -> getIGEq (cata nil_ cons_) (ifrom x) (ifrom y) where
    nil_ :: IGEq a b '[]
    nil_ = IGEq $ \a -> case a of {}

    cons_ :: IGEq a b zs -> IGEq a b (z ': zs)
    cons_ (IGEq rec) = IGEq $ \xs ys -> case (xs, ys) of
        (IHere,      IHere)      -> Just Refl
        (IHere,      IThere  _)  -> Nothing
        (IThere _,   IHere )     -> Nothing
        (IThere xs', IThere ys') -> rec xs' ys'

newtype IGEq a b xs = IGEq
    { getIGEq :: IRep xs a -> IRep xs b -> Maybe (a :~: b) }

{-
-- RHS size: {terms: 20, types: 68, coercions: 18, joins: 0/0}
igeq_$sigeq
igeq_$sigeq
  = \ @ a_X1aw @ b_X1ay eta_B2 eta1_B1 ->
      case eta_B2 of {
        DomainInt co_a1cI ->
          case eta1_B1 of {
            DomainInt co1_X1eW -> igeq1 `cast` <Co:9>;
            DomainChar co1_a1cN -> Nothing
          };
        DomainChar co_a1cN ->
          case eta1_B1 of {
            DomainInt co1_a1cI -> Nothing;
            DomainChar co1_X1f1 -> igeq1 `cast` <Co:9>
          }
      }
-}
instance GEq Domain where
    geq = genericGeq

-- This actually simplifies to Nothing
{-

-- RHS size: {terms: 1, types: 5, coercions: 0, joins: 0/0}
ex01
ex01 = Nothing

-}
ex01 :: Maybe (Int :~: Char)
ex01 = geq DomainInt DomainChar

-------------------------------------------------------------------------------
-- Examples: GCompare
-------------------------------------------------------------------------------

genericGCompare :: forall a b f. IEnum f => f a ->  f b -> GOrdering a b
genericGCompare = \x y -> getIGCompare (cata nil_ cons_) (ifrom x) (ifrom y) where
    nil_ :: IGCompare a b '[]
    nil_ = IGCompare $ \a -> case a of {}

    cons_ :: IGCompare a b zs -> IGCompare a b (z ': zs)
    cons_ (IGCompare rec) = IGCompare $ \xs ys -> case (xs, ys) of
        (IHere,      IHere)      -> GEQ
        (IHere,      IThere  _)  -> GLT
        (IThere _,   IHere )     -> GGT
        (IThere xs', IThere ys') -> rec xs' ys'

newtype IGCompare a b xs = IGCompare
    { getIGCompare :: IRep xs a -> IRep xs b -> GOrdering a b }

{-

-- RHS size: {terms: 20, types: 70, coercions: 16, joins: 0/0}
$fGCompareTYPEDomain_$sgenericGCompare
$fGCompareTYPEDomain_$sgenericGCompare
  = \ @ a_X3je @ b_X3jg eta_B2 eta1_B1 ->
      case eta_B2 of {
        DomainInt co_a3pG ->
          case eta1_B1 of {
            DomainInt co1_X3ts -> $WGEQ `cast` <Co:8>;
            DomainChar co1_a3pL -> GLT
          };
        DomainChar co_a3pL ->
          case eta1_B1 of {
            DomainInt co1_a3pG -> GGT;
            DomainChar co1_X3tx -> $WGEQ `cast` <Co:8>
          }
      }

-}
instance GCompare Domain where
    gcompare = genericGCompare

{-

-- RHS size: {terms: 1, types: 4, coercions: 0, joins: 0/0}
ex03
ex03 = GLT

-}
ex03 :: GOrdering Int Char
ex03 = gcompare DomainInt DomainChar

-------------------------------------------------------------------------------
-- Examples: ArgDict
-------------------------------------------------------------------------------

-- | @constraints@
data Dict c where
    Dict :: c => Dict c

class ArgDict f where
    type ArgDictC (c :: Type -> Constraint) f :: Constraint
    type ArgDictC c f = All c (ICode f)

    argDict :: ArgDictC c f => f a -> Dict (c a)
    default argDict :: (All c (ICode f), IEnum f, GArgDict a (ICode f)) => f a -> Dict (c a)
    argDict = giargDict . ifrom

type family All (c :: Type -> Constraint) (xs :: [Type]) :: Constraint where
    All c '[]       = ()
    All c (x ': xs) = (c x, All c xs)

class GArgDict a xs where
    giargDict :: All c xs => IRep xs a -> Dict (c a)

instance GArgDict a '[] where
    giargDict x = case x of {}

instance GArgDict a xs => GArgDict a (x ': xs) where
    giargDict IHere      = Dict
    giargDict (IThere x) = giargDict x

{-

-- RHS size: {terms: 15, types: 55, coercions: 51, joins: 0/0}
$fArgDictDomain_$cargDict
$fArgDictDomain_$cargDict
  = \ @ c_s36s @ a_s36t w_s36u w1_s36v ->
      case w1_s36v of {
        DomainInt co_a2yO ->
          Dict (($p1(%,%) (w_s36u `cast` <Co:19>)) `cast` <Co:3>);
        DomainChar co_a2yT ->
          Dict
            (($p1(%,%) (($p2(%,%) (w_s36u `cast` <Co:19>)) `cast` <Co:7>))
             `cast` <Co:3>)
      }

-}
instance ArgDict Domain

{-

ex02
ex02
  = \ @ a_a2uM dom_X16Q x_X16S ->
      case dom_X16Q of {
        DomainInt co_a2yO -> $fShowInt_$cshow (x_X16S `cast` <Co:2>);
        DomainChar co_a2yT -> $fShowChar_$cshow (x_X16S `cast` <Co:2>)
      }

-}
ex02 :: forall a. Domain a -> a -> String
ex02 dom x = case argDict dom :: Dict (Show a) of
    Dict -> show x

-------------------------------------------------------------------------------
-- GShow & ShowTag
-------------------------------------------------------------------------------

genericShowTaggedPrec
    :: forall tag f (a :: Type). (ArgDict tag, ArgDictC Show tag, Show1 f)
    => tag a -> Int -> f a -> ShowS
genericShowTaggedPrec ta d fa = case argDict ta :: Dict (Show a) of
    Dict -> showsPrec1 d fa

deriving instance Show (Domain a)

instance GShow Domain where gshowsPrec = showsPrec
instance Show1 f => ShowTag Domain f where
    showTaggedPrec = genericShowTaggedPrec

-------------------------------------------------------------------------------
-- Universe
-------------------------------------------------------------------------------

genericUniverse :: IEnum f => [Some f]
genericUniverse = map (mapSome ito) $ getIUniverseSome (cata nil_ cons_) where
    nil_ :: IUniverseSome '[]
    nil_ = IUniverseSome []

    cons_ :: IUniverseSome zs -> IUniverseSome (z : zs)
    cons_ (IUniverseSome rec) = IUniverseSome $
        Some IHere : map (mapSome IThere) rec

newtype IUniverseSome xs = IUniverseSome
    { getIUniverseSome :: [Some (IRep xs)] }

mapSome :: (forall x. f x -> g x) -> Some f -> Some g
mapSome nt (Some x) = Some (nt x)

-- some maps and coercions :(
ex04 :: [Some Domain]
ex04 = genericUniverse


genericUniverse2 :: IEnum f => [Some f]
genericUniverse2 = collapse_NPF ito $ getIUniverseSome2 (cata nil_ cons_) where
    nil_ :: IUniverseSome2 '[]
    nil_ = IUniverseSome2 Nil

    cons_ :: Cata zs => IUniverseSome2 zs -> IUniverseSome2 (z : zs)
    cons_ (IUniverseSome2 rec) = IUniverseSome2 $
        IHere ::* map_NPF IThere rec

newtype IUniverseSome2 xs = IUniverseSome2
    { getIUniverseSome2 :: NPF (IRep xs) xs }

collapse_NPF
    :: forall f g xs. Cata xs
    => (forall x. f x -> g x) -> NPF f xs -> [Some g]
collapse_NPF nt = getCollapseNPF (cata nil_ cons_) where
    nil_ :: CollapseNPF f g '[]
    nil_ = CollapseNPF $ \_ -> []

    cons_ :: CollapseNPF f g zs -> CollapseNPF f g (z : zs)
    cons_ (CollapseNPF rec) = CollapseNPF $ \(z ::* zs) -> Some (nt z) : rec zs

newtype CollapseNPF f g xs = CollapseNPF { getCollapseNPF :: NPF f xs -> [Some g] }

map_NPF
    :: forall (f :: Type -> Type) g xs. Cata xs
    => (forall x. f x -> g x) -> NPF f xs -> NPF g xs
map_NPF nt = getMapNPF (cata nil_ cons_) where
    nil_ :: MapNPF f g '[]
    nil_ = MapNPF $ \_ -> Nil

    cons_ :: MapNPF f g zs -> MapNPF f g (z : zs)
    cons_ (MapNPF rec) = MapNPF $ \(z ::* zs) -> nt z ::* rec zs

newtype MapNPF f g xs = MapNPF { getMapNPF :: NPF f xs -> NPF g xs }

{-

-- RHS size: {terms: 3, types: 6, coercions: 11, joins: 0/0}
ex4
ex4 = : ($WDomainChar `cast` <Co:11>) []

-- RHS size: {terms: 3, types: 3, coercions: 11, joins: 0/0}
ex05
ex05 = : ($WDomainInt `cast` <Co:11>) ex4

-}
ex05 :: [Some Domain]
ex05 = genericUniverse2