{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
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 a next = ToFIf (IsToF a) a next
type family ToFIf t a next :: Type where
ToFIf 'True (a, b) next = ToF a (ToF b next)
ToFIf 'True (Either l r) next = (ToF l next, ToF r next)
ToFIf 'True () next = next
ToFIf 'True (Endpoint end a) next = (next :~: end, a)
ToFIf 'False a next = a -> next
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
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 a = UnToFIf (IsToF a) a
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