src/Symantic/Syntaxes/TuplesOfFunctions.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE ConstraintKinds #-}
   3 {-# LANGUAGE DataKinds #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5
   6 -- | Tuples-of-Functions
   7 module Symantic.Syntaxes.TuplesOfFunctions where
   8
   9 import Data.Bool (Bool (..))
  10 import Data.Either (Either (..))
  11 import Data.Eq (Eq)
  12 import Data.Function qualified as Fun
  13 import Data.Kind (Type)
  14 import Text.Show (Show)
  15 import Type.Reflection ((:~:) (..))
  16
  17 -- * Type 'ToF'
  18 type ToF a next = ToFIf (IsToF a) a next
  19
  20 -- ** Type 'ToFIf'
  21
  22 -- | Transform a type @(a)@ to Tuples-of-Functions returning @(next)@.
  23 -- The @(t)@ parameter is to avoid overlapping instances of 'UnToFIf'.
  24 type family ToFIf t a next :: Type where
  25 -- For '<.>': curry.
  26   ToFIf 'True (a, b) next = ToF a (ToF b next)
  27 -- For '<+>', request both branches.
  28   ToFIf 'True (Either l r) next = (ToF l next, ToF r next)
  29 -- Useless to ask '()' as argument.
  30   ToFIf 'True () next = next
  31 -- Enable a different return value for each function.
  32   ToFIf 'True (Endpoint end a) next = (next :~: end, a)
  33 -- Everything else becomes a new argument.
  34   ToFIf 'False a next = a -> next
  35
  36 -- ** Type 'IsToF'
  37
  38 -- | This 'Bool' is added to 'ToFIf' to avoid overlapping instances.
  39 type family IsToF a :: Bool where
  40   IsToF () = 'True
  41   IsToF (a, b) = 'True
  42   IsToF (Either l r) = 'True
  43   IsToF (Endpoint end a) = 'True
  44   IsToF a = 'False
  45
  46 -- ** Type 'Endpoint'
  47 newtype Endpoint end a = Endpoint {unEndpoint :: a}
  48   deriving (Eq, Show)
  49
  50 endpoint :: a -> ToF (Endpoint end a) end
  51 endpoint = (Refl,)
  52
  53 -- * Type 'UnToF'
  54 type UnToF a = UnToFIf (IsToF a) a
  55
  56 -- * Class 'UnToFIf'
  57 class UnToFIf (t :: Bool) a where
  58   unToF :: ToFIf t a next -> a -> next
  59 instance UnToFIf 'True () where
  60   unToF = Fun.const
  61 instance (UnToF a, UnToF b) => UnToFIf 'True (a, b) where
  62   unToF hab (a, b) = (unToF @(IsToF b) (unToF @(IsToF a) hab a)) b
  63 instance (UnToF a, UnToF b) => UnToFIf 'True (Either a b) where
  64   unToF (ha, hb) = \case
  65     Left a -> unToF @(IsToF a) ha a
  66     Right b -> unToF @(IsToF b) hb b
  67 instance UnToFIf 'False a where
  68   unToF = Fun.id