Skip to content

Instantly share code, notes, and snippets.

@kakkun61
Created February 22, 2022 06:32
Show Gist options
  • Save kakkun61/3b4269e184b90d2d6abb5ae6566dac94 to your computer and use it in GitHub Desktop.
Save kakkun61/3b4269e184b90d2d6abb5ae6566dac94 to your computer and use it in GitHub Desktop.
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment