{-# LANGUAGE ConstraintKinds #-} -- For type class synonyms
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DefaultSignatures #-} -- For adding LiftDerived* constraints
module Symantic.Dityped.Derive where

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

-- * Type family 'Derived'
-- | The representation that @(repr)@ derives to.
type family Derived (repr :: Type -> Type -> Type) :: Type -> Type -> Type

-- * Class 'Derivable'
-- | Derivable an interpreter to a another interpreter
-- determined by the 'Derived' open type family.
-- This is mostly useful when running the interpreter stack,
-- but also when going back from an initial encoding to a final one.
--
-- Note that 'derive' and 'liftDerived' are not necessarily reciprocical functions.
class Derivable repr where
  derive :: repr a ka -> Derived repr a ka

-- * Class 'LiftDerived'
-- | Lift the 'Derived' interpreter of an interpreter, to that interpreter.
-- This is mostly useful to give default values to class methods
-- in order to skip their definition for interpreters
-- where 'liftDerived' can already apply the right semantic.
--
-- Note that 'derive' and 'liftDerived' are not necessarily reciprocical functions.
class LiftDerived repr where
  liftDerived :: Derived repr a ka -> repr a ka

-- * Class 'LiftDerived1'
-- | Convenient wrapper of 'derive' and 'liftDerived' for functions with a single argument.
class LiftDerived1 repr where
  liftDerived1 ::
    (Derived repr a ka -> Derived repr b kb) ->
    repr a ka -> repr b kb
  liftDerived1 Derived repr a ka -> Derived repr b kb
f = Derived repr b kb -> repr b kb
forall (repr :: * -> * -> *) a ka.
LiftDerived repr =>
Derived repr a ka -> repr a ka
liftDerived (Derived repr b kb -> repr b kb)
-> (repr a ka -> Derived repr b kb) -> repr a ka -> repr b kb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derived repr a ka -> Derived repr b kb
f (Derived repr a ka -> Derived repr b kb)
-> (repr a ka -> Derived repr a ka)
-> repr a ka
-> Derived repr b kb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. repr a ka -> Derived repr a ka
forall (repr :: * -> * -> *) a ka.
Derivable repr =>
repr a ka -> Derived repr a ka
derive
  default liftDerived1 ::
    LiftDerived repr => Derivable repr =>
    (Derived repr a ka -> Derived repr b kb) ->
    repr a ka -> repr b kb

-- * Class 'LiftDerived2'
-- | Convenient wrapper of 'derive' and 'liftDerived' for functions with two arguments.
class LiftDerived2 repr where
  liftDerived2 ::
    (Derived repr a ka -> Derived repr b kb -> Derived repr c kc) ->
    repr a ka -> repr b kb -> repr c kc
  liftDerived2 Derived repr a ka -> Derived repr b kb -> Derived repr c kc
f repr a ka
a repr b kb
b = Derived repr c kc -> repr c kc
forall (repr :: * -> * -> *) a ka.
LiftDerived repr =>
Derived repr a ka -> repr a ka
liftDerived (Derived repr a ka -> Derived repr b kb -> Derived repr c kc
f (repr a ka -> Derived repr a ka
forall (repr :: * -> * -> *) a ka.
Derivable repr =>
repr a ka -> Derived repr a ka
derive repr a ka
a) (repr b kb -> Derived repr b kb
forall (repr :: * -> * -> *) a ka.
Derivable repr =>
repr a ka -> Derived repr a ka
derive repr b kb
b))
  default liftDerived2 ::
    LiftDerived repr => Derivable repr =>
    (Derived repr a ka -> Derived repr b kb -> Derived repr c kc) ->
    repr a ka -> repr b kb -> repr c kc

-- * Class 'LiftDerived3'
-- | Convenient wrapper of 'derive' and 'liftDerived' for functions with three arguments.
class LiftDerived3 repr where
  liftDerived3 ::
    (Derived repr a ka -> Derived repr b kb -> Derived repr c kc -> Derived repr d kd) ->
    repr a ka -> repr b kb -> repr c kc -> repr d kd
  liftDerived3 Derived repr a ka
-> Derived repr b kb -> Derived repr c kc -> Derived repr d kd
f repr a ka
a repr b kb
b repr c kc
c = Derived repr d kd -> repr d kd
forall (repr :: * -> * -> *) a ka.
LiftDerived repr =>
Derived repr a ka -> repr a ka
liftDerived (Derived repr a ka
-> Derived repr b kb -> Derived repr c kc -> Derived repr d kd
f (repr a ka -> Derived repr a ka
forall (repr :: * -> * -> *) a ka.
Derivable repr =>
repr a ka -> Derived repr a ka
derive repr a ka
a) (repr b kb -> Derived repr b kb
forall (repr :: * -> * -> *) a ka.
Derivable repr =>
repr a ka -> Derived repr a ka
derive repr b kb
b) (repr c kc -> Derived repr c kc
forall (repr :: * -> * -> *) a ka.
Derivable repr =>
repr a ka -> Derived repr a ka
derive repr c kc
c))
  default liftDerived3 ::
    LiftDerived repr => Derivable repr =>
    (Derived repr a ka -> Derived repr b kb -> Derived repr c kc -> Derived repr d kd) ->
    repr a ka -> repr b kb -> repr c kc -> repr d kd

-- * Class 'LiftDerived4'
-- | Convenient wrapper of 'derive' and 'liftDerived' for functions with three arguments.
class LiftDerived4 repr where
  liftDerived4 ::
    (Derived repr a ka -> Derived repr b kb -> Derived repr c kc -> Derived repr d kd -> Derived repr e ke) ->
    repr a ka -> repr b kb -> repr c kc -> repr d kd -> repr e ke
  liftDerived4 Derived repr a ka
-> Derived repr b kb
-> Derived repr c kc
-> Derived repr d kd
-> Derived repr e ke
f repr a ka
a repr b kb
b repr c kc
c repr d kd
d = Derived repr e ke -> repr e ke
forall (repr :: * -> * -> *) a ka.
LiftDerived repr =>
Derived repr a ka -> repr a ka
liftDerived (Derived repr a ka
-> Derived repr b kb
-> Derived repr c kc
-> Derived repr d kd
-> Derived repr e ke
f (repr a ka -> Derived repr a ka
forall (repr :: * -> * -> *) a ka.
Derivable repr =>
repr a ka -> Derived repr a ka
derive repr a ka
a) (repr b kb -> Derived repr b kb
forall (repr :: * -> * -> *) a ka.
Derivable repr =>
repr a ka -> Derived repr a ka
derive repr b kb
b) (repr c kc -> Derived repr c kc
forall (repr :: * -> * -> *) a ka.
Derivable repr =>
repr a ka -> Derived repr a ka
derive repr c kc
c) (repr d kd -> Derived repr d kd
forall (repr :: * -> * -> *) a ka.
Derivable repr =>
repr a ka -> Derived repr a ka
derive repr d kd
d))
  default liftDerived4 ::
    LiftDerived repr => Derivable repr =>
    (Derived repr a ka -> Derived repr b kb -> Derived repr c kc -> Derived repr d kd -> Derived repr e ke) ->
    repr a ka -> repr b kb -> repr c kc -> repr d kd -> repr e ke

-- * Type synonyms @FromDerived*@
-- | Convenient type synonym for using 'liftDerived' on symantic class @(sym)@.
type FromDerived  sym repr = ( LiftDerived  repr, sym (Derived repr) )
type FromDerived1 sym repr = ( LiftDerived1 repr, sym (Derived repr) )
type FromDerived2 sym repr = ( LiftDerived2 repr, sym (Derived repr) )
type FromDerived3 sym repr = ( LiftDerived3 repr, sym (Derived repr) )
type FromDerived4 sym repr = ( LiftDerived4 repr, sym (Derived repr) )