Barbies.Bare.Translate.hs

{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE StandaloneKindSignatures   #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE UndecidableInstances       #-}

module Barbies.Bare.Translate
  ( Implicit (..)
  , Explicit (..)
  , ImplicitT (..)
  , ExplicitT (..)
  , Reducible (..)
  ) where

import Barbies.Bare         (Covered)
import Data.Functor.Layered (FunctorB)
import Data.Ix              (Ix)
import Data.Kind            (Type)
import GHC.Exts             (IsList, IsString)
import GHC.Generics         (Generic)

-- | Fit a type @a@ that has @'Type' -> ('Type' -> 'Type') -> 'Type'@ kind to @('Type' -> 'Type') -> 'Type'@.
-- In other words remove a type parameter 'Covered' from the type @a@.
type Implicit :: (Type -> (k -> Type) -> Type) -> (k -> Type) -> Type
newtype Implicit a f = Implicit { unimplicit :: a Covered f } deriving Generic

deriving stock instance Show (a Covered f) => Show (Implicit a f)
deriving stock instance Read (a Covered f) => Read (Implicit a f)
deriving stock instance Eq (a Covered f) => Eq (Implicit a f)
deriving stock instance Ord (a Covered f) => Ord (Implicit a f)
deriving stock instance Bounded (a Covered f) => Bounded (Implicit a f)
deriving newtype instance Enum (a Covered f) => Enum (Implicit a f)
deriving newtype instance Num (a Covered f) => Num (Implicit a f)
deriving newtype instance Real (a Covered f) => Real (Implicit a f)
deriving newtype instance Integral (a Covered f) => Integral (Implicit a f)
deriving newtype instance Fractional (a Covered f) => Fractional (Implicit a f)
deriving newtype instance Floating (a Covered f) => Floating (Implicit a f)
deriving newtype instance RealFrac (a Covered f) => RealFrac (Implicit a f)
deriving newtype instance RealFloat (a Covered f) => RealFloat (Implicit a f)
deriving newtype instance Ix (a Covered f) => Ix (Implicit a f)
deriving newtype instance IsString (a Covered f) => IsString (Implicit a f)
deriving newtype instance IsList (a Covered f) => IsList (Implicit a f)
deriving newtype instance FunctorB (a Covered) => FunctorB (Implicit a)

-- | Fit a type @a@ that has @('Type' -> 'Type') -> 'Type'@ kind to @'Type' -> ('Type' -> 'Type') -> 'Type'@.
-- In other words add an additional type parameter 'Covered' to the type @a@.
type Explicit :: ((k -> Type) -> Type) -> Type -> (k -> Type) -> Type
data family Explicit a b f

newtype instance Explicit a Covered f = Explicit { unexplicit :: a f } deriving Generic

deriving stock instance Show (a f) => Show (Explicit a Covered f)
deriving stock instance Read (a f) => Read (Explicit a Covered f)
deriving stock instance Eq (a f) => Eq (Explicit a Covered f)
deriving stock instance Ord (a f) => Ord (Explicit a Covered f)
deriving stock instance Bounded (a f) => Bounded (Explicit a Covered f)
deriving newtype instance Enum (a f) => Enum (Explicit a Covered f)
deriving newtype instance Num (a f) => Num (Explicit a Covered f)
deriving newtype instance Real (a f) => Real (Explicit a Covered f)
deriving newtype instance Integral (a f) => Integral (Explicit a Covered f)
deriving newtype instance Fractional (a f) => Fractional (Explicit a Covered f)
deriving newtype instance Floating (a f) => Floating (Explicit a Covered f)
deriving newtype instance RealFrac (a f) => RealFrac (Explicit a Covered f)
deriving newtype instance RealFloat (a f) => RealFloat (Explicit a Covered f)
deriving newtype instance Ix (a f) => Ix (Explicit a Covered f)
deriving newtype instance IsString (a f) => IsString (Explicit a Covered f)
deriving newtype instance IsList (a f) => IsList (Explicit a Covered f)
deriving newtype instance FunctorB a => FunctorB (Explicit a Covered)

type ImplicitT :: (Type -> (Type -> (k -> Type) -> Type) -> (k -> Type) -> Type) -> (k -> Type) -> ((k -> Type) -> Type) -> Type
newtype ImplicitT t f a = ImplicitT { unimplicitT :: t Covered (Explicit a) f } deriving Generic

deriving stock instance Show (t Covered (Explicit a) f) => Show (ImplicitT t f a)
deriving stock instance Read (t Covered (Explicit a) f) => Read (ImplicitT t f a)
deriving stock instance Eq (t Covered (Explicit a) f) => Eq (ImplicitT t f a)
deriving stock instance Ord (t Covered (Explicit a) f) => Ord (ImplicitT t f a)
deriving stock instance Bounded (t Covered (Explicit a) f) => Bounded (ImplicitT t f a)
deriving newtype instance Enum (t Covered (Explicit a) f) => Enum (ImplicitT t f a)
deriving newtype instance Num (t Covered (Explicit a) f) => Num (ImplicitT t f a)
deriving newtype instance Real (t Covered (Explicit a) f) => Real (ImplicitT t f a)
deriving newtype instance Integral (t Covered (Explicit a) f) => Integral (ImplicitT t f a)
deriving newtype instance Fractional (t Covered (Explicit a) f) => Fractional (ImplicitT t f a)
deriving newtype instance Floating (t Covered (Explicit a) f) => Floating (ImplicitT t f a)
deriving newtype instance RealFrac (t Covered (Explicit a) f) => RealFrac (ImplicitT t f a)
deriving newtype instance RealFloat (t Covered (Explicit a) f) => RealFloat (ImplicitT t f a)
deriving newtype instance Ix (t Covered (Explicit a) f) => Ix (ImplicitT t f a)
deriving newtype instance IsString (t Covered (Explicit a) f) => IsString (ImplicitT t f a)
deriving newtype instance IsList (t Covered (Explicit a) f) => IsList (ImplicitT t f a)

type ExplicitT :: ((k -> Type) -> ((k -> Type) -> Type) -> Type) -> Type -> (k -> Type) -> (Type -> (k -> Type) -> Type) -> Type
data family ExplicitT t b f a

newtype instance ExplicitT t Covered f a = ExplicitT { unexplicitT :: t f (Implicit a) } deriving Generic

deriving stock instance Show (t f (Implicit a)) => Show (ExplicitT t Covered f a)
deriving stock instance Read (t f (Implicit a)) => Read (ExplicitT t Covered f a)
deriving stock instance Eq (t f (Implicit a)) => Eq (ExplicitT t Covered f a)
deriving stock instance Ord (t f (Implicit a)) => Ord (ExplicitT t Covered f a)
deriving stock instance Bounded (t f (Implicit a)) => Bounded (ExplicitT t Covered f a)
deriving newtype instance Enum (t f (Implicit a)) => Enum (ExplicitT t Covered f a)
deriving newtype instance Num (t f (Implicit a)) => Num (ExplicitT t Covered f a)
deriving newtype instance Real (t f (Implicit a)) => Real (ExplicitT t Covered f a)
deriving newtype instance Integral (t f (Implicit a)) => Integral (ExplicitT t Covered f a)
deriving newtype instance Fractional (t f (Implicit a)) => Fractional (ExplicitT t Covered f a)
deriving newtype instance Floating (t f (Implicit a)) => Floating (ExplicitT t Covered f a)
deriving newtype instance RealFrac (t f (Implicit a)) => RealFrac (ExplicitT t Covered f a)
deriving newtype instance RealFloat (t f (Implicit a)) => RealFloat (ExplicitT t Covered f a)
deriving newtype instance Ix (t f (Implicit a)) => Ix (ExplicitT t Covered f a)
deriving newtype instance IsString (t f (Implicit a)) => IsString (ExplicitT t Covered f a)
deriving newtype instance IsList (t f (Implicit a)) => IsList (ExplicitT t Covered f a)

class Reducible a where
  type Reduce a :: (k -> Type) -> Type
  reduce :: a f -> Reduce a f

instance Reducible (Explicit (Implicit a) Covered) where
  type Reduce (Explicit (Implicit a) Covered) = a Covered
  reduce = unimplicit . unexplicit

instance Reducible (Implicit (Explicit a)) where
  type Reduce (Implicit (Explicit a)) = a
  reduce = unexplicit . unimplicit