+++ /dev/null
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE InstanceSigs #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-module Symantic.Semantics.ToFer where
-
-import Control.Monad (Monad, (>=>))
-import Data.Function qualified as Fun
-import Data.Functor (Functor, (<$>))
-import GHC.Generics (Generic)
-
-import Symantic.Syntaxes.Classes
-import Symantic.Syntaxes.EithersOfTuples
-import Symantic.Syntaxes.TuplesOfFunctions
-
--- * Type 'TuplesOfFunctions'
-
--- | The 'ToFer' intermediate interpreter
--- return Tuples-of-Functions instead of Eithers-of-Tuples.
---
--- In other words, it transforms 'SumFunctor' into functions returning @(sem next)@
--- and 'ProductFunctor' into arguments of those functions.
---
--- This is like using an extension parameter introduced in
--- https://okmij.org/ftp/typed-formatting/index.html#DSL-FIn
--- but here only a single type parameter @(a)@ is exposed
--- instead of two.
---
--- Useful to avoid declaring and pattern-matching
--- an algebraic datatype of type @(a)@,
--- as the corresponding function will be called directly,
--- given as arguments the terms that would have been
--- pattern-matched from a constructor
--- of such algebraic datatype.
-data ToFer sem a = ToFer
- { tuplesOfFunctions :: forall next. ToF a next -> sem next
- , eithersOfTuples :: sem a
- }
-
-instance (ProductFunctor sem, Monad sem) => ProductFunctor (ToFer sem) where
- a <.> b =
- ToFer
- { tuplesOfFunctions = tuplesOfFunctions a >=> tuplesOfFunctions b
- , eithersOfTuples = eithersOfTuples a <.> eithersOfTuples b
- }
- a .> b =
- ToFer
- { tuplesOfFunctions = tuplesOfFunctions a >=> tuplesOfFunctions b
- , eithersOfTuples = eithersOfTuples a .> eithersOfTuples b
- }
- a <. b =
- ToFer
- { tuplesOfFunctions = tuplesOfFunctions a >=> tuplesOfFunctions b
- , eithersOfTuples = eithersOfTuples a <. eithersOfTuples b
- }
-instance (SumFunctor sem, AlternativeFunctor sem) => SumFunctor (ToFer sem) where
- a <+> b =
- ToFer
- { tuplesOfFunctions = \(l, r) -> tuplesOfFunctions a l <|> tuplesOfFunctions b r
- , eithersOfTuples = eithersOfTuples a <+> eithersOfTuples b
- }
-instance (Optionable sem, Functor sem) => Optionable (ToFer sem) where
- optional ma = ToFer{tuplesOfFunctions = (<$> sem), eithersOfTuples = sem}
- where
- sem = optional (eithersOfTuples ma)
-instance Functor sem => Dataable (ToFer sem) where
- data_ ::
- forall a.
- Generic a =>
- RepOfEoT a =>
- EoTOfRep a =>
- UnToF a =>
- ToFer sem (EoT (ADT a)) ->
- ToFer sem a
- data_ a =
- ToFer
- { tuplesOfFunctions = \f -> unToF @(IsToF a) @a f Fun.. adtOfeot <$> eithersOfTuples a
- , eithersOfTuples = adtOfeot <$> eithersOfTuples a
- }
import Data.Bool (Bool (..))
import Data.Either (Either (..))
import Data.Eq (Eq)
-import Data.Function qualified as Fun
+import Data.Function (const, id, ($), (.))
import Data.Kind (Type)
+import Data.Ord (Ord)
import Text.Show (Show)
-import Type.Reflection ((:~:) (..))
--- * Type 'ToF'
-type ToF a next = ToFIf (IsToF a) a next
+-- * Type family '(-->)'
--- ** Type 'ToFIf'
+-- | Convenient alias for a Tuples of Functions transformation.
+--
+-- Example of a covariant semantic producing a 'Text':
+--
+-- @
+-- data Texter a = { unTexter :: forall next. (a --> next) -> next }
+-- runTexter :: Texter a -> (a --> Text) -> Text
+-- runTexter = unTexter
+--
+-- @
+--
+-- Example of a contravariant semantic producing a 'Text':
+--
+-- @
+-- data Texter a = { unTexter :: forall next. (Text -> next) -> a --> next }
+-- runTexter :: Texter a -> a --> Text
+-- runTexter sem = unTexter sem id
+-- @
+type (-->) a next = ToFIf (IsToF a) a next
--- | Transform a type @(a)@ to Tuples-of-Functions returning @(next)@.
--- The @(t)@ parameter is to avoid overlapping instances of 'UnToFIf'.
-type family ToFIf t a next :: Type where
--- For '<.>': curry.
- ToFIf 'True (a, b) next = ToF a (ToF b next)
--- For '<+>', request both branches.
- ToFIf 'True (Either l r) next = (ToF l next, ToF r next)
--- Useless to ask '()' as argument.
+infixr 0 -->
+
+-- ** Type family 'ToFIf'
+
+-- | Return Tuples-of-Functions instead of Eithers-of-Tuples
+--
+-- Useful to avoid introducing a parameter dedicated for the return value,
+-- as in https://okmij.org/ftp/typed-formatting/index.html#DSL-FIn
+--
+-- Useful to avoid declaring and pattern-matching
+-- an algebraic datatype of type @(a)@,
+-- as the corresponding function will be called directly,
+-- given as arguments the terms that would have been
+-- pattern-matched from a constructor
+-- of such algebraic datatype.
+type family ToFIf (t :: Bool) a next :: Type where
+-- Curry on '<.>'.
+ ToFIf 'True (a, b) next = a --> b --> next
+-- Branch on '<+>'.
+ ToFIf 'True (Either a b) next = (a --> next, b --> next)
+-- Skip '()' as argument.
ToFIf 'True () next = next
-- Enable a different return value for each function.
- ToFIf 'True (Endpoint end a) next = (next :~: end, a)
+ ToFIf 'True (Endpoint sem a) next = ToFEndpoint sem a next
-- Everything else becomes a new argument.
ToFIf 'False a next = a -> next
--- ** Type 'IsToF'
+-- ** Type family 'IsToF'
--- | This 'Bool' is added to 'ToFIf' to avoid overlapping instances.
-type family IsToF a :: Bool where
- IsToF () = 'True
+-- | When @('IsToF' a ~ 'True')@, iif. the argument is changed by 'ToFIf'.
+-- This being a closed type family, it enables to avoid defining
+-- an instance of 'ToFIf' and 'ToFable' for all types.
+type family IsToF (a :: Type) :: Bool where
IsToF (a, b) = 'True
- IsToF (Either l r) = 'True
+ IsToF (Either a b) = 'True
+ IsToF () = 'True
IsToF (Endpoint end a) = 'True
IsToF a = 'False
-- ** Type 'Endpoint'
-newtype Endpoint end a = Endpoint {unEndpoint :: a}
- deriving (Eq, Show)
-endpoint :: a -> ToF (Endpoint end a) end
-endpoint = (Refl,)
+-- | @('Endpoint' sem a)@ enables the function equivalent to a datatype constructor,
+-- to return a value of type @a@.
+--
+-- Useful to enable functions to return different types.
+newtype Endpoint (sem :: Type -> Type) a = Endpoint {unEndpoint :: a}
+ deriving (Eq, Ord, Show)
+
+-- ** Type family 'ToFEndpoint'
+type family ToFEndpoint (sem :: Type -> Type) a next :: Type
--- * Type 'UnToF'
-type UnToF a = UnToFIf (IsToF a) a
+-- * Class 'ToFable'
+class ToFable a where
+ tofOffun :: (a -> next) -> a --> next
+ funOftof :: (a --> next) -> a -> next
+ default tofOffun :: (a --> next) ~ (a -> next) => (a -> next) -> a --> next
+ default funOftof :: (a --> next) ~ (a -> next) => (a --> next) -> a -> next
+ tofOffun = id
+ funOftof = id
+instance ToFable () where
+ tofOffun = ($ ())
+ funOftof = const
+instance (ToFable a, ToFable b) => ToFable (a, b) where
+ tofOffun ab2n = tofOffun (\a -> tofOffun (\b -> ab2n (a, b)))
+ funOftof k (a, b) = funOftof (funOftof k a) b
+instance (ToFable a, ToFable b) => ToFable (Either a b) where
+ tofOffun e2n = (tofOffun (e2n . Left), tofOffun (e2n . Right))
+ funOftof (ak, bk) = \case
+ Left a -> funOftof ak a
+ Right b -> funOftof bk b
--- * Class 'UnToFIf'
-class UnToFIf (t :: Bool) a where
- unToF :: ToFIf t a next -> a -> next
-instance UnToFIf 'True () where
- unToF = Fun.const
-instance (UnToF a, UnToF b) => UnToFIf 'True (a, b) where
- unToF hab (a, b) = (unToF @(IsToF b) (unToF @(IsToF a) hab a)) b
-instance (UnToF a, UnToF b) => UnToFIf 'True (Either a b) where
- unToF (ha, hb) = \case
- Left a -> unToF @(IsToF a) ha a
- Right b -> unToF @(IsToF b) hb b
-instance UnToFIf 'False a where
- unToF = Fun.id
+-- OVERLAPPABLE could be avoided by using 'ToFIf',
+-- but that would a be a bit more verbose and require more type annotations.
+instance {-# OVERLAPPABLE #-} IsToF a ~ 'False => ToFable a
sourcephile / git / haskell / symantic-base.git / commitdiff