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