{-# 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.Function qualified as Fun
import Data.Kind (Type)
import Type.Reflection ((:~:) (..))

-- * Type 'ToF'
type ToF a next = ToFIf (IsToF a) a next

-- ** Type 'ToFIf'

-- | Transform a type @(a)@ to Tuples-of-Functions returning @(next)@.
-- The @(t)@ parameter is to avoid overlapping instances of 'UnToFIf'.
type family ToFIf t a next :: Type where
-- For '<.>': curry.
  ToFIf 'True (a, b) next = ToF a (ToF b next)
-- For '<+>', request both branches.
  ToFIf 'True (Either l r) next = (ToF l next, ToF r next)
-- Useless to ask '()' as argument.
  ToFIf 'True () next = next
-- Enable a different return value for each function.
  ToFIf 'True (Endpoint end a) next = (next :~: end, a)
-- Everything else becomes a new argument.
  ToFIf 'False a next = a -> next

-- ** Type 'IsToF'

-- | This 'Bool' is added to 'ToFIf' to avoid overlapping instances.
type family IsToF a :: Bool where
  IsToF () = 'True
  IsToF (a, b) = 'True
  IsToF (Either l r) = 'True
  IsToF (Endpoint end a) = 'True
  IsToF a = 'False

-- ** Type 'Endpoint'
newtype Endpoint end a = Endpoint {unEndpoint :: a}

endpoint :: a -> ToF (Endpoint end a) end
endpoint = (Refl,)

-- * Type 'UnToF'
type UnToF a = UnToFIf (IsToF a) a

-- * Class 'UnToFIf'
class UnToFIf (t :: Bool) a where
  unToF :: ToFIf t a next -> a -> next
instance UnToFIf 'True () where
  unToF = Fun.const
instance (UnToF a, UnToF b) => UnToFIf 'True (a, b) where
  unToF hab (a, b) = (unToF @(IsToF b) (unToF @(IsToF a) hab a)) b
instance (UnToF a, UnToF b) => UnToFIf 'True (Either a b) where
  unToF (ha, hb) = \case
    Left a -> unToF @(IsToF a) ha a
    Right b -> unToF @(IsToF b) hb b
instance UnToFIf 'False a where
  unToF = Fun.id