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
  14 -- * Type 'ToF'
  15 type ToF a next = ToFIf (IsToF a) a next
  16
  17 -- ** Type 'ToFIf'
  18
  19 -- | Transform a type @(a)@ to Tuples-of-Functions returning @(next)@.
  20 -- The @(t)@ parameter is to avoid overlapping instances of 'UnToFIf'.
  21 type family ToFIf t a next :: Type where
  22 -- For '<.>': curry.
  23   ToFIf 'True (a, b) next = ToF a (ToF b next)
  24 -- For '<+>', request both branches.
  25   ToFIf 'True (Either l r) next = (ToF l next, ToF r next)
  26 -- Useless to ask '()' as argument.
  27   ToFIf 'True () next = next
  28 -- Everything else becomes a new argument.
  29   ToFIf 'False a next = a -> next
  30
  31 -- ** Type 'IsToF'
  32
  33 -- | This 'Bool' is added to 'ToFIf' to avoid overlapping instances.
  34 type family IsToF a :: Bool where
  35   IsToF () = 'True
  36   IsToF (a, b) = 'True
  37   IsToF (Either l r) = 'True
  38   IsToF a = 'False
  39
  40 -- * Type 'UnToF'
  41 type UnToF a = UnToFIf (IsToF a) a
  42
  43 -- * Class 'UnToFIf'
  44 class UnToFIf (t :: Bool) a where
  45   unToF :: ToFIf t a next -> a -> next
  46 instance UnToFIf 'True () where
  47   unToF = Fun.const
  48 instance (UnToF a, UnToF b) => UnToFIf 'True (a, b) where
  49   unToF hab (a, b) = (unToF @(IsToF b) (unToF @(IsToF a) hab a)) b
  50 instance (UnToF a, UnToF b) => UnToFIf 'True (Either a b) where
  51   unToF (ha, hb) = \case
  52     Left a -> unToF @(IsToF a) ha a
  53     Right b -> unToF @(IsToF b) hb b
  54 instance UnToFIf 'False a where
  55   unToF = Fun.id