{-# 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 {forall end a. Endpoint end a -> a
unEndpoint :: a}

endpoint :: a -> ToF (Endpoint end a) end
endpoint :: forall a end. a -> ToF (Endpoint end a) end
endpoint = (end :~: end
forall {k} (a :: k). a :~: a
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 :: forall next. ToFIf 'True () next -> () -> next
unToF = ToFIf 'True () next -> () -> next
forall a b. a -> b -> a
Fun.const
instance (UnToF a, UnToF b) => UnToFIf 'True (a, b) where
  unToF :: forall next. ToFIf 'True (a, b) next -> (a, b) -> next
unToF ToFIf 'True (a, b) next
hab (a
a, b
b) = (forall (t :: Bool) a next.
UnToFIf t a =>
ToFIf t a next -> a -> next
unToF @(IsToF b) (forall (t :: Bool) a next.
UnToFIf t a =>
ToFIf t a next -> a -> next
unToF @(IsToF a) ToFIf 'True (a, b) next
ToFIf (IsToF a) a (ToFIf (IsToF b) b next)
hab a
a)) b
b
instance (UnToF a, UnToF b) => UnToFIf 'True (Either a b) where
  unToF :: forall next. ToFIf 'True (Either a b) next -> Either a b -> next
unToF (ToFIf (IsToF a) a next
ha, ToFIf (IsToF b) b next
hb) = \case
    Left a
a -> forall (t :: Bool) a next.
UnToFIf t a =>
ToFIf t a next -> a -> next
unToF @(IsToF a) ToFIf (IsToF a) a next
ha a
a
    Right b
b -> forall (t :: Bool) a next.
UnToFIf t a =>
ToFIf t a next -> a -> next
unToF @(IsToF b) ToFIf (IsToF b) b next
hb b
b
instance UnToFIf 'False a where
  unToF :: forall next. ToFIf 'False a next -> a -> next
unToF = ToFIf 'False a next -> a -> next
forall a. a -> a
Fun.id