{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Tuples-of-Functions
module Symantic.Syntaxes.TuplesOfFunctions where

import Data.Bool (Bool (..))
import Data.Either (Either (..))
import Data.Eq (Eq)
import Data.Function (const, id, ($), (.))
import Data.Kind (Type)
import Data.Ord (Ord)
import Text.Show (Show)

-- * Type family '(-->)'

-- | Convenient alias for a Tuples of Functions transformation.
--
-- Example of a covariant semantic producing a 'Text':
--
-- @
-- data Texter a = { unTexter :: forall next. (a --> next) -> next }
-- runTexter :: Texter a -> (a --> Text) -> Text
-- runTexter = unTexter
--
-- @
--
-- Example of a contravariant semantic producing a 'Text':
--
-- @
-- data Texter a = { unTexter :: forall next. (Text -> next) -> a --> next }
-- runTexter :: Texter a -> a --> Text
-- runTexter sem = unTexter sem id
-- @
type (-->) a next = ToFIf (IsToF a) a next

infixr 0 -->

-- ** Type family 'ToFIf'

-- | Return Tuples-of-Functions instead of Eithers-of-Tuples
--
-- Useful to avoid introducing a parameter dedicated for the return value,
-- as in https://okmij.org/ftp/typed-formatting/index.html#DSL-FIn
--
-- Useful to avoid declaring and pattern-matching
-- an algebraic datatype of type @(a)@,
-- as the corresponding function will be called directly,
-- given as arguments the terms that would have been
-- pattern-matched from a constructor
-- of such algebraic datatype.
type family ToFIf (t :: Bool) a next :: Type where
-- Curry on '<.>'.
  ToFIf 'True (a, b) next = a --> b --> next
-- Branch on '<+>'.
  ToFIf 'True (Either a b) next = (a --> next, b --> next)
-- Skip '()' as argument.
  ToFIf 'True () next = next
-- Enable a different return value for each function.
  ToFIf 'True (Endpoint sem a) next = ToFEndpoint sem a next
-- Everything else becomes a new argument.
  ToFIf 'False a next = a -> next

-- ** Type family 'IsToF'

-- | When @('IsToF' a ~ 'True')@, iif. the argument is changed by 'ToFIf'.
-- This being a closed type family, it enables to avoid defining
-- an instance of 'ToFIf' and 'ToFable' for all types.
type family IsToF (a :: Type) :: Bool where
  IsToF (a, b) = 'True
  IsToF (Either a b) = 'True
  IsToF () = 'True
  IsToF (Endpoint end a) = 'True
  IsToF a = 'False

-- ** Type 'Endpoint'

-- | @('Endpoint' sem a)@ enables the function equivalent to a datatype constructor,
-- to return a value of type @a@.
--
-- Useful to enable functions to return different types.
newtype Endpoint (sem :: Type -> Type) a = Endpoint {unEndpoint :: a}
  deriving (Eq, Ord, Show)

-- ** Type family 'ToFEndpoint'
type family ToFEndpoint (sem :: Type -> Type) a next :: Type

-- * Class 'ToFable'
class ToFable a where
  tofOffun :: (a -> next) -> a --> next
  funOftof :: (a --> next) -> a -> next
  default tofOffun :: (a --> next) ~ (a -> next) => (a -> next) -> a --> next
  default funOftof :: (a --> next) ~ (a -> next) => (a --> next) -> a -> next
  tofOffun = id
  funOftof = id
instance ToFable () where
  tofOffun = ($ ())
  funOftof = const
instance (ToFable a, ToFable b) => ToFable (a, b) where
  tofOffun ab2n = tofOffun (\a -> tofOffun (\b -> ab2n (a, b)))
  funOftof k (a, b) = funOftof (funOftof k a) b
instance (ToFable a, ToFable b) => ToFable (Either a b) where
  tofOffun e2n = (tofOffun (e2n . Left), tofOffun (e2n . Right))
  funOftof (ak, bk) = \case
    Left a -> funOftof ak a
    Right b -> funOftof bk b

-- OVERLAPPABLE could be avoided by using 'ToFIf',
-- but that would a be a bit more verbose and require more type annotations.
instance {-# OVERLAPPABLE #-} IsToF a ~ 'False => ToFable a