1 {-# LANGUAGE AllowAmbiguousTypes #-}
2 {-# LANGUAGE ConstraintKinds #-}
3 {-# LANGUAGE DataKinds #-}
4 {-# LANGUAGE UndecidableInstances #-}
6 -- | This module enables the use of Tuples-of-Functions
7 -- instead of Eithers-of-Tuples.
8 module Symantic.Syntaxes.TuplesOfFunctions where
10 import Data.Bool (Bool (..))
11 import Data.Either (Either (..))
13 import Data.Function (const, id, ($), (.))
14 import Data.Kind (Type)
16 import Text.Show (Show)
18 -- * Type family '(-->)'
20 -- | Convenient alias for a Tuples of Functions transformation.
22 -- Example of a covariant semantic producing a 'Text':
25 -- data Texter a = { unTexter :: forall next. (a --> next) -> next }
26 -- runTexter :: Texter a -> (a --> Text) -> Text
27 -- runTexter = unTexter
31 -- Example of a contravariant semantic producing a 'Text':
34 -- data Texter a = { unTexter :: forall next. (Text -> next) -> a --> next }
35 -- runTexter :: Texter a -> a --> Text
36 -- runTexter sem = unTexter sem id
38 type (-->) a next = ToFIf (IsToF a) a next
42 -- ** Type family 'ToFIf'
44 -- | Return Tuples-of-Functions instead of Eithers-of-Tuples
46 -- Useful to avoid introducing a parameter dedicated for the return value,
47 -- as in https://okmij.org/ftp/typed-formatting/index.html#DSL-FIn
49 -- Useful to avoid declaring and pattern-matching
50 -- an algebraic datatype of type @(a)@,
51 -- as the corresponding function will be called directly,
52 -- given as arguments the terms that would have been
53 -- pattern-matched from a constructor
54 -- of such algebraic datatype.
55 type family ToFIf (t :: Bool) a next :: Type where
57 ToFIf 'True (a, b) next = a --> b --> next
59 ToFIf 'True (Either a b) next = (a --> next, b --> next)
60 -- Skip '()' as argument.
61 ToFIf 'True () next = next
62 -- Enable a different return value for each function.
63 ToFIf 'True (Endpoint sem a) next = ToFEndpoint sem a next
64 -- Everything else becomes a new argument.
65 ToFIf 'False a next = a -> next
67 -- ** Type family 'IsToF'
69 -- | When @('IsToF' a ~ 'True')@, iif. the argument is changed by 'ToFIf'.
70 -- This being a closed type family, it enables to avoid defining
71 -- an instance of 'ToFIf' and 'ToFable' for all types.
72 type family IsToF (a :: Type) :: Bool where
74 IsToF (Either a b) = 'True
76 IsToF (Endpoint end a) = 'True
81 -- | @('Endpoint' sem a)@ enables the function equivalent to a datatype constructor,
82 -- to return a value of type @a@.
84 -- Useful to enable functions to return different types.
85 newtype Endpoint (sem :: Type -> Type) a = Endpoint {unEndpoint :: a}
86 deriving (Eq, Ord, Show)
88 -- ** Type family 'ToFEndpoint'
89 type family ToFEndpoint (sem :: Type -> Type) a next :: Type
93 tofOffun :: (a -> next) -> a --> next
94 funOftof :: (a --> next) -> a -> next
95 default tofOffun :: (a --> next) ~ (a -> next) => (a -> next) -> a --> next
96 default funOftof :: (a --> next) ~ (a -> next) => (a --> next) -> a -> next
99 instance ToFable () where
102 instance (ToFable a, ToFable b) => ToFable (a, b) where
103 tofOffun ab2n = tofOffun (\a -> tofOffun (\b -> ab2n (a, b)))
104 funOftof k (a, b) = funOftof (funOftof k a) b
105 instance (ToFable a, ToFable b) => ToFable (Either a b) where
106 tofOffun e2n = (tofOffun (e2n . Left), tofOffun (e2n . Right))
107 funOftof (ak, bk) = \case
108 Left a -> funOftof ak a
109 Right b -> funOftof bk b
111 -- OVERLAPPABLE could be avoided by using 'ToFIf',
112 -- but that would a be a bit more verbose and require more type annotations.
113 instance {-# OVERLAPPABLE #-} IsToF a ~ 'False => ToFable a