{-# LANGUAGE ConstraintKinds #-} -- For type class synonyms
{-# LANGUAGE DefaultSignatures #-} -- For adding Trans* constraints
module Symantic.Univariant.Trans where

-- TODO: move to symantic-univariant

import Data.Function ((.))
import Data.Kind (Type)

-- * Type family 'Output'
type family Output (repr :: Type -> Type) :: Type -> Type

-- * Class 'Trans'
-- | A 'trans'lation from an interpreter @(from)@ to an interpreter @(to)@.
class Trans from to where
  trans :: from a -> to a

-- * Class 'BiTrans'
-- | Convenient type class synonym.
-- Note that this is not necessarily a bijective 'trans'lation, a 'trans' being not necessarily injective nor surjective.
type BiTrans from to = (Trans from to, Trans to from)

-- ** Class 'Liftable'
-- | Convenient type class synonym for using 'Output'
type Liftable repr = Trans (Output repr) repr
lift :: forall repr a.
  Liftable repr =>
  Output repr a -> repr a
lift = trans @(Output repr)
{-# INLINE lift #-}

unlift :: forall repr a.
  Trans repr (Output repr) =>
  repr a -> Output repr a
unlift = trans @repr
{-# INLINE unlift #-}

-- ** Class 'Unliftable'
-- | Convenient type class synonym for using 'Output'
type Unliftable repr = Trans repr (Output repr)

-- * Class 'Trans1'
class Trans1 from to where
  trans1 ::
    (from a -> from b) ->
    to a -> to b
  default trans1 ::
    BiTrans from to =>
    (from a -> from b) ->
    to a -> to b
  trans1 f = trans . f . trans
  {-# INLINE trans1 #-}

-- ** Class 'Liftable1'
-- | Convenient type class synonym for using 'Output'
type Liftable1 repr = Trans1 (Output repr) repr
lift1 :: forall repr a b.
  Liftable1 repr =>
  (Output repr a -> Output repr b) ->
  repr a -> repr b
lift1 = trans1 @(Output repr)
{-# INLINE lift1 #-}

-- * Class 'Trans2'
class Trans2 from to where
  trans2 ::
    (from a -> from b -> from c) ->
    to a -> to b -> to c
  default trans2 ::
    BiTrans from to =>
    (from a -> from b -> from c) ->
    to a -> to b -> to c
  trans2 f a b = trans (f (trans a) (trans b))
  {-# INLINE trans2 #-}

-- ** Class 'Liftable2'
-- | Convenient type class synonym for using 'Output'
type Liftable2 repr = Trans2 (Output repr) repr
lift2 :: forall repr a b c.
  Liftable2 repr =>
  (Output repr a -> Output repr b -> Output repr c) ->
  repr a -> repr b -> repr c
lift2 = trans2 @(Output repr)
{-# INLINE lift2 #-}

-- * Class 'Trans3'
class Trans3 from to where
  trans3 ::
    (from a -> from b -> from c -> from d) ->
    to a -> to b -> to c -> to d
  default trans3 ::
    BiTrans from to =>
    (from a -> from b -> from c -> from d) ->
    to a -> to b -> to c -> to d
  trans3 f a b c = trans (f (trans a) (trans b) (trans c))
  {-# INLINE trans3 #-}

-- ** Class 'Liftable3'
-- | Convenient type class synonym for using 'Output'
type Liftable3 repr = Trans3 (Output repr) repr
lift3 :: forall repr a b c d.
  Liftable3 repr =>
  (Output repr a -> Output repr b -> Output repr c -> Output repr d) ->
  repr a -> repr b -> repr c -> repr d
lift3 = trans3 @(Output repr)
{-# INLINE lift3 #-}

-- * Type 'Any'
-- | A newtype to disambiguate the 'Trans' instance to any other interpreter when there is also one or more 'Trans's to other interpreters with a different interpretation than the generic one.
newtype Any repr a = Any { unAny :: repr a }
type instance Output (Any repr) = repr
instance Trans (Any repr) repr where
  trans = unAny
instance Trans1 (Any repr) repr
instance Trans2 (Any repr) repr
instance Trans3 (Any repr) repr
instance Trans repr (Any repr) where
  trans = Any
instance Trans1 repr (Any repr)
instance Trans2 repr (Any repr)
instance Trans3 repr (Any repr)