{-# LANGUAGE ConstraintKinds #-} -- For type class synonyms
module Symantic.Dityped.Transformable where

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

-- * Class 'Transformable'
-- | Used with @DefaultSignatures@ and default methods,
-- in the symantics class definition,
-- it then avoids on an interpreter instance
-- to define unused methods.
class Transformable from to where
  trans :: from a k -> to a k

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

-- * Class 'Transformable1'
class Transformable1 from to where
  -- | Convenient helper lifing an unary operator,
  -- but also enables to identify unary operators.
  trans1 ::
    (from a b -> from c d) ->
    to a b -> to c d
  trans1 f = trans . f . trans
  default trans1 ::
    BiTransformable from to =>
    (from a b -> from c d) ->
    to a b -> to c d

-- * Class 'Transformable2'
class Transformable2 from to where
  -- | Convenient helper lifting a binary operator,
  -- but also enables to identify binary operators.
  trans2 ::
    (from a b -> from c d -> from e f) ->
    to a b -> to c d -> to e f
  trans2 f x y = trans (f (trans x) (trans y))
  default trans2 ::
    BiTransformable from to =>
    (from a b -> from c d -> from e f) ->
    to a b -> to c d -> to e f

-- * Class 'Transformable3'
class Transformable3 from to where
  trans3 ::
    (from a ak -> from b bk -> from c ck -> from d dk) ->
    to a ak -> to b bk -> to c ck -> to d dk
  trans3 f a b c = trans (f (trans a) (trans b) (trans c))
  default trans3 ::
    BiTransformable from to =>
    (from a ak -> from b bk -> from c ck -> from d dk) ->
    to a ak -> to b bk -> to c ck -> to d dk
  {-# INLINE trans3 #-}

-- * Type family 'Unlifted'
-- | The underlying representation that @(repr)@ transforms to.
type family Unlifted (repr :: Type -> Type -> Type) :: Type -> Type -> Type

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

unlift :: forall repr a k.
  Transformable repr (Unlifted repr) =>
  repr a k -> Unlifted repr a k
unlift = trans @repr
{-# INLINE unlift #-}

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

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

-- ** Class 'Liftable3'
-- | Convenient type class synonym for using 'Unlifted'
type Liftable3 repr = Transformable3 (Unlifted repr) repr
lift3 :: forall repr a ak b bk c ck d dk.
  Liftable3 repr =>
  (Unlifted repr a ak -> Unlifted repr b bk -> Unlifted repr c ck -> Unlifted repr d dk) ->
  repr a ak -> repr b bk -> repr c ck -> repr d dk
lift3 = trans3 @(Unlifted repr)
{-# INLINE lift3 #-}