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 (const, id, ($), (.))
  13 import Data.Kind (Type)
  14 import Data.Ord (Ord)
  15 import Text.Show (Show)
  16
  17 -- * Type family '(-->)'
  18
  19 -- | Convenient alias for a Tuples of Functions transformation.
  20 --
  21 -- Example of a covariant semantic producing a 'Text':
  22 --
  23 -- @
  24 -- data Texter a = { unTexter :: forall next. (a --> next) -> next }
  25 -- runTexter :: Texter a -> (a --> Text) -> Text
  26 -- runTexter = unTexter
  27 --
  28 -- @
  29 --
  30 -- Example of a contravariant semantic producing a 'Text':
  31 --
  32 -- @
  33 -- data Texter a = { unTexter :: forall next. (Text -> next) -> a --> next }
  34 -- runTexter :: Texter a -> a --> Text
  35 -- runTexter sem = unTexter sem id
  36 -- @
  37 type (-->) a next = ToFIf (IsToF a) a next
  38
  39 infixr 0 -->
  40
  41 -- ** Type family 'ToFIf'
  42
  43 -- | Return Tuples-of-Functions instead of Eithers-of-Tuples
  44 --
  45 -- Useful to avoid introducing a parameter dedicated for the return value,
  46 -- as in https://okmij.org/ftp/typed-formatting/index.html#DSL-FIn
  47 --
  48 -- Useful to avoid declaring and pattern-matching
  49 -- an algebraic datatype of type @(a)@,
  50 -- as the corresponding function will be called directly,
  51 -- given as arguments the terms that would have been
  52 -- pattern-matched from a constructor
  53 -- of such algebraic datatype.
  54 type family ToFIf (t :: Bool) a next :: Type where
  55 -- Curry on '<.>'.
  56   ToFIf 'True (a, b) next = a --> b --> next
  57 -- Branch on '<+>'.
  58   ToFIf 'True (Either a b) next = (a --> next, b --> next)
  59 -- Skip '()' as argument.
  60   ToFIf 'True () next = next
  61 -- Enable a different return value for each function.
  62   ToFIf 'True (Endpoint sem a) next = ToFEndpoint sem a next
  63 -- Everything else becomes a new argument.
  64   ToFIf 'False a next = a -> next
  65
  66 -- ** Type family 'IsToF'
  67
  68 -- | When @('IsToF' a ~ 'True')@, iif. the argument is changed by 'ToFIf'.
  69 -- This being a closed type family, it enables to avoid defining
  70 -- an instance of 'ToFIf' and 'ToFable' for all types.
  71 type family IsToF (a :: Type) :: Bool where
  72   IsToF (a, b) = 'True
  73   IsToF (Either a b) = 'True
  74   IsToF () = 'True
  75   IsToF (Endpoint end a) = 'True
  76   IsToF a = 'False
  77
  78 -- ** Type 'Endpoint'
  79
  80 -- | @('Endpoint' sem a)@ enables the function equivalent to a datatype constructor,
  81 -- to return a value of type @a@.
  82 --
  83 -- Useful to enable functions to return different types.
  84 newtype Endpoint (sem :: Type -> Type) a = Endpoint {unEndpoint :: a}
  85   deriving (Eq, Ord, Show)
  86
  87 -- ** Type family 'ToFEndpoint'
  88 type family ToFEndpoint (sem :: Type -> Type) a next :: Type
  89
  90 -- * Class 'ToFable'
  91 class ToFable a where
  92   tofOffun :: (a -> next) -> a --> next
  93   funOftof :: (a --> next) -> a -> next
  94   default tofOffun :: (a --> next) ~ (a -> next) => (a -> next) -> a --> next
  95   default funOftof :: (a --> next) ~ (a -> next) => (a --> next) -> a -> next
  96   tofOffun = id
  97   funOftof = id
  98 instance ToFable () where
  99   tofOffun = ($ ())
 100   funOftof = const
 101 instance (ToFable a, ToFable b) => ToFable (a, b) where
 102   tofOffun ab2n = tofOffun (\a -> tofOffun (\b -> ab2n (a, b)))
 103   funOftof k (a, b) = funOftof (funOftof k a) b
 104 instance (ToFable a, ToFable b) => ToFable (Either a b) where
 105   tofOffun e2n = (tofOffun (e2n . Left), tofOffun (e2n . Right))
 106   funOftof (ak, bk) = \case
 107     Left a -> funOftof ak a
 108     Right b -> funOftof bk b
 109
 110 -- OVERLAPPABLE could be avoided by using 'ToFIf',
 111 -- but that would a be a bit more verbose and require more type annotations.
 112 instance {-# OVERLAPPABLE #-} IsToF a ~ 'False => ToFable a