From cce4b8df9cac6dc85d7cb0c129134a3436508394 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Mon, 17 Jul 2023 22:06:54 +0200
Subject: [PATCH 01/16] iface: remove `ToFer` semantic in favor of `(-->)`

`ToFer` only supported covariant semantics,
and required it to be a `Monad`.
This is no longer the case when using `(-->)`
directly in a semantic's definition.
---
 src/Symantic/Semantics.hs                  |   2 -
 src/Symantic/Semantics/ToFer.hs            |  82 --------------
 src/Symantic/Syntaxes/Classes.hs           |   2 -
 src/Symantic/Syntaxes/TuplesOfFunctions.hs | 120 ++++++++++++++-------
 symantic-base.cabal                        |   4 -
 5 files changed, 82 insertions(+), 128 deletions(-)
 delete mode 100644 src/Symantic/Semantics/ToFer.hs

diff --git a/src/Symantic/Semantics.hs b/src/Symantic/Semantics.hs
index 6d40d6a..a151e18 100644
--- a/src/Symantic/Semantics.hs
+++ b/src/Symantic/Semantics.hs
@@ -1,11 +1,9 @@
 module Symantic.Semantics (
   module Symantic.Semantics.Reader,
   module Symantic.Semantics.SharingObserver,
-  module Symantic.Semantics.ToFer,
   module Symantic.Semantics.Viewer,
 ) where
 
 import Symantic.Semantics.Reader
 import Symantic.Semantics.SharingObserver
-import Symantic.Semantics.ToFer
 import Symantic.Semantics.Viewer
diff --git a/src/Symantic/Semantics/ToFer.hs b/src/Symantic/Semantics/ToFer.hs
deleted file mode 100644
index bb74486..0000000
--- a/src/Symantic/Semantics/ToFer.hs
+++ /dev/null
@@ -1,82 +0,0 @@
-{-# 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
-      }
diff --git a/src/Symantic/Syntaxes/Classes.hs b/src/Symantic/Syntaxes/Classes.hs
index 2f9f566..68a3a83 100644
--- a/src/Symantic/Syntaxes/Classes.hs
+++ b/src/Symantic/Syntaxes/Classes.hs
@@ -34,7 +34,6 @@ import Numeric.Natural (Natural)
 import Symantic.Syntaxes.CurryN
 import Symantic.Syntaxes.Derive
 import Symantic.Syntaxes.EithersOfTuples
-import Symantic.Syntaxes.TuplesOfFunctions
 
 -- * Type 'Syntax'
 type Syntax = Semantic -> Constraint
@@ -353,7 +352,6 @@ class Dataable sem where
     Generic a =>
     RepOfEoT a =>
     EoTOfRep a =>
-    UnToF a =>
     IsoFunctor sem =>
     sem (EoT (ADT a)) ->
     sem a
diff --git a/src/Symantic/Syntaxes/TuplesOfFunctions.hs b/src/Symantic/Syntaxes/TuplesOfFunctions.hs
index 672af56..e2723d2 100644
--- a/src/Symantic/Syntaxes/TuplesOfFunctions.hs
+++ b/src/Symantic/Syntaxes/TuplesOfFunctions.hs
@@ -9,60 +9,104 @@ module Symantic.Syntaxes.TuplesOfFunctions where
 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
diff --git a/symantic-base.cabal b/symantic-base.cabal
index 96eea13..f5c0508 100644
--- a/symantic-base.cabal
+++ b/symantic-base.cabal
@@ -45,9 +45,6 @@ description:
   and optimize recursive grammars.
   Inspired by Andy Gill's [Type-safe observable sharing in Haskell](https://doi.org/10.1145/1596638.1596653).
   For an example, see [symantic-parser](https://hackage.haskell.org/package/symantic-parser).
-  * @Symantic.Semantics.ToFer@
-  interprets combinators to return Tuples-of-Functions
-  instead of Eithers-of-Tuples.
   * @Symantic.Semantics.Viewer@
   interprets combinators as human-readable text.
   * @Symantic.Semantics.Viewer.Fixity@
@@ -86,7 +83,6 @@ library
     Symantic.Semantics
     Symantic.Semantics.Reader
     Symantic.Semantics.SharingObserver
-    Symantic.Semantics.ToFer
     Symantic.Semantics.Viewer
     Symantic.Semantics.Viewer.Fixity
     Symantic.Syntaxes
-- 
2.44.1


From 365aafb004afcb2a2e179b3aceb5634d94f809db Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Mon, 17 Jul 2023 22:43:48 +0200
Subject: [PATCH 02/16] iface: add the `a` parameter to the `Dataable` class

---
 src/Symantic/Syntaxes/Classes.hs | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

diff --git a/src/Symantic/Syntaxes/Classes.hs b/src/Symantic/Syntaxes/Classes.hs
index 68a3a83..3600386 100644
--- a/src/Symantic/Syntaxes/Classes.hs
+++ b/src/Symantic/Syntaxes/Classes.hs
@@ -344,23 +344,18 @@ construct f = dicurry (Proxy :: Proxy args) f eotOfadt
 -- * Class 'Dataable'
 
 -- | Enable the contruction or deconstruction
--- of a any algebraic data type.
-class Dataable sem where
+-- of an 'ADT' (algebraic data type).
+class Dataable a sem where
   -- | Unfortunately, 'UnToF' is needed for the 'ToFer' instance.
-  data_ :: Generic a => RepOfEoT a => EoTOfRep a => UnToF a => sem (EoT (ADT a)) -> sem a
-  default data_ ::
+  dataType :: sem (EoT (ADT a)) -> sem a
+  default dataType ::
     Generic a =>
     RepOfEoT a =>
     EoTOfRep a =>
     IsoFunctor sem =>
     sem (EoT (ADT a)) ->
     sem a
-  data_ = (<%>) (Iso adtOfeot eotOfadt)
-
--- | Like 'data_' but with the @(a)@ type parameter first
--- for convenience when specifying it.
-dataType :: forall a sem. Dataable sem => Generic a => RepOfEoT a => EoTOfRep a => UnToF a => sem (EoT (ADT a)) -> sem a
-dataType = data_
+  dataType = (<%>) (Iso adtOfeot eotOfadt)
 
 -- * Class 'IfSemantic'
 
-- 
2.44.1


From ed964802f99f59353e6130ddc0f3385cf28dc614 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Mon, 17 Jul 2023 22:44:34 +0200
Subject: [PATCH 03/16] impl: fix `(:!:)` completeness warning

---
 src/Symantic/Syntaxes/Classes.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Symantic/Syntaxes/Classes.hs b/src/Symantic/Syntaxes/Classes.hs
index 3600386..e79eb0e 100644
--- a/src/Symantic/Syntaxes/Classes.hs
+++ b/src/Symantic/Syntaxes/Classes.hs
@@ -293,6 +293,7 @@ pattern a :!: b <-
     a :!: b = (a, b)
 
 infixr 4 :!:
+{-# COMPLETE (:!:) #-}
 
 -- * Class 'AlternativeFunctor'
 
-- 
2.44.1


From 7bf5c11b812c21bf51c3d54e07ba905607f7532f Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Mon, 17 Jul 2023 22:45:04 +0200
Subject: [PATCH 04/16] doc: fix comment about `CurryN`

---
 src/Symantic/Syntaxes/CurryN.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Symantic/Syntaxes/CurryN.hs b/src/Symantic/Syntaxes/CurryN.hs
index 844fda4..93602c5 100644
--- a/src/Symantic/Syntaxes/CurryN.hs
+++ b/src/Symantic/Syntaxes/CurryN.hs
@@ -11,7 +11,7 @@ import Symantic.Syntaxes.EithersOfTuples (Tuples)
 -- * Class 'CurryN'
 
 -- | Produce and consume 'Tuples'.
--- Not actually useful for the Generic side of this module,
+-- Not actually useful for 'Symantic.Syntaxes.EithersOfTuples',
 -- but related through the use of 'Tuples'.
 class CurryN args where
   -- Like 'curry' but for an arbitrary number of nested 2-tuples.
-- 
2.44.1


From 57508e6cf583e0bcbe0aab04b7c20027f86033b6 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Thu, 10 Aug 2023 12:22:51 +0200
Subject: [PATCH 05/16] doc: remove old comments

---
 flake.lock                       | 6 +++---
 src/Symantic/Syntaxes/Classes.hs | 1 -
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/flake.lock b/flake.lock
index 1df8ddb..e64f0b2 100644
--- a/flake.lock
+++ b/flake.lock
@@ -17,11 +17,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1683207485,
-        "narHash": "sha256-gs+PHt/y/XQB7S8+YyBLAM8LjgYpPZUVFQBwpFSmJro=",
+        "lastModified": 1691328192,
+        "narHash": "sha256-w59N1zyDQ7SupfMJLFvtms/SIVbdryqlw5AS4+DiH+Y=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "cc45a3f8c98e1c33ca996e3504adefbf660a72d1",
+        "rev": "61676e4dcfeeb058f255294bcb08ea7f3bc3ce56",
         "type": "github"
       },
       "original": {
diff --git a/src/Symantic/Syntaxes/Classes.hs b/src/Symantic/Syntaxes/Classes.hs
index e79eb0e..9d7bb42 100644
--- a/src/Symantic/Syntaxes/Classes.hs
+++ b/src/Symantic/Syntaxes/Classes.hs
@@ -347,7 +347,6 @@ construct f = dicurry (Proxy :: Proxy args) f eotOfadt
 -- | Enable the contruction or deconstruction
 -- of an 'ADT' (algebraic data type).
 class Dataable a sem where
-  -- | Unfortunately, 'UnToF' is needed for the 'ToFer' instance.
   dataType :: sem (EoT (ADT a)) -> sem a
   default dataType ::
     Generic a =>
-- 
2.44.1


From d10fc143f5732d73361833f107444c59f209b9d5 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Sat, 26 Aug 2023 23:04:33 +0200
Subject: [PATCH 06/16] doc: rename type variable `able` to `syn`

---
 src/Symantic/Syntaxes/Data.hs | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/src/Symantic/Syntaxes/Data.hs b/src/Symantic/Syntaxes/Data.hs
index e7d6d31..7bee687 100644
--- a/src/Symantic/Syntaxes/Data.hs
+++ b/src/Symantic/Syntaxes/Data.hs
@@ -22,11 +22,11 @@ import Symantic.Syntaxes.Derive
 
 -- * Type 'SomeData'
 data SomeData sem a
-  = forall able.
-    ( Derivable (Data able sem)
-    , Typeable able
+  = forall syn.
+    ( Derivable (Data syn sem)
+    , Typeable syn
     ) =>
-    SomeData (Data able sem a)
+    SomeData (Data syn sem a)
 
 type instance Derived (SomeData sem) = sem
 instance Derivable (SomeData sem) where
@@ -39,24 +39,24 @@ instance Derivable (SomeData sem) where
 -- hence 'Data.Coerce.coerce' cannot be used on them for now.
 -- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
 -- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
-data family Data (able :: Syntax) :: Semantic -> Semantic
-type instance Derived (Data able sem) = sem
+data family Data (syn :: Syntax) :: Semantic -> Semantic
+type instance Derived (Data syn sem) = sem
 
 -- | Convenient utility to pattern-match a 'SomeData'.
-pattern Data :: Typeable able => Data able sem a -> SomeData sem a
+pattern Data :: Typeable syn => Data syn sem a -> SomeData sem a
 pattern Data x <- (unSomeData -> Maybe.Just x)
 
--- | @(unSomeData c :: 'Maybe' ('Data' able sem a))@
--- extract the data-constructor from the given 'SomeData'
--- iif. it belongs to the @('Data' able sem a)@ data-instance.
+-- | @(unSomeData sd :: 'Maybe' ('Data' syn sem a))@
+-- extract the data-constructor from the given 'SomeData' @(sd)@
+-- iif. it belongs to the @('Data' syn sem a)@ data-instance.
 unSomeData ::
-  forall able sem a.
-  Typeable able =>
+  forall syn sem a.
+  Typeable syn =>
   SomeData sem a ->
-  Maybe (Data able sem a)
-unSomeData (SomeData (c :: Data c sem a)) =
-  case typeRep @able `eqTypeRep` typeRep @c of
-    Maybe.Just HRefl -> Maybe.Just c
+  Maybe (Data syn sem a)
+unSomeData (SomeData (constr :: Data actualSyn sem a)) =
+  case typeRep @syn `eqTypeRep` typeRep @actualSyn of
+    Maybe.Just HRefl -> Maybe.Just constr
     Maybe.Nothing -> Maybe.Nothing
 
 -- Abstractable
-- 
2.44.1


From e45543f3c08af3e8f0a34c38318d8c1ad9aa1f23 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Sun, 27 Aug 2023 00:32:39 +0200
Subject: [PATCH 07/16] doc: improve comment about `Derivable`

---
 src/Symantic/Syntaxes/Derive.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Symantic/Syntaxes/Derive.hs b/src/Symantic/Syntaxes/Derive.hs
index a001533..12f4b5a 100644
--- a/src/Symantic/Syntaxes/Derive.hs
+++ b/src/Symantic/Syntaxes/Derive.hs
@@ -23,9 +23,9 @@ type family Derived (sem :: Semantic) :: Semantic
 
 -- * Class 'Derivable'
 
--- | Derive an interpreter to another interpreter
--- determined by the 'Derived' open type family.
--- This is mostly useful when running the interpreter stack,
+-- | Derive from a semantic @(sem)@
+-- another semantic determined by the 'Derived' open type family.
+-- This is mostly useful when running a semantic stack,
 -- but also when going back from an initial encoding to a final one.
 --
 -- Note that 'derive' and 'liftDerived' are not necessarily reciprocical functions.
-- 
2.44.1


From df1d797499b7a25f9c7e949645c1129686c72a99 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Wed, 30 Aug 2023 01:11:07 +0200
Subject: [PATCH 08/16] iface: add semantic `Forall`

---
 src/Symantic/Semantics.hs        |  2 +
 src/Symantic/Semantics/Forall.hs | 93 ++++++++++++++++++++++++++++++++
 src/Symantic/Syntaxes/Classes.hs |  6 +--
 symantic-base.cabal              |  1 +
 4 files changed, 99 insertions(+), 3 deletions(-)
 create mode 100644 src/Symantic/Semantics/Forall.hs

diff --git a/src/Symantic/Semantics.hs b/src/Symantic/Semantics.hs
index a151e18..13ccce5 100644
--- a/src/Symantic/Semantics.hs
+++ b/src/Symantic/Semantics.hs
@@ -1,9 +1,11 @@
 module Symantic.Semantics (
+  module Symantic.Semantics.Forall,
   module Symantic.Semantics.Reader,
   module Symantic.Semantics.SharingObserver,
   module Symantic.Semantics.Viewer,
 ) where
 
+import Symantic.Semantics.Forall
 import Symantic.Semantics.Reader
 import Symantic.Semantics.SharingObserver
 import Symantic.Semantics.Viewer
diff --git a/src/Symantic/Semantics/Forall.hs b/src/Symantic/Semantics/Forall.hs
new file mode 100644
index 0000000..e834857
--- /dev/null
+++ b/src/Symantic/Semantics/Forall.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Symantic.Semantics.Forall where
+
+import Control.Applicative (Applicative (..))
+import Control.Monad (Monad (..))
+import Data.Bool (Bool (..))
+import Data.Eq (Eq (..))
+import Data.Function ((.))
+import Data.Functor (Functor (..))
+import Data.Kind (Type)
+import Text.Show (Show (..))
+
+import Symantic.Syntaxes.Classes (Syntax, Syntaxes, Unabstractable (..))
+
+-- * Type 'Forall'
+newtype Forall (syns :: [Syntax]) (a :: Type)
+  = Forall (forall sem. Syntaxes syns sem => sem a)
+
+instance
+  ( forall sem. Syntaxes syns sem => Functor sem
+  ) =>
+  Functor (Forall syns)
+  where
+  fmap f (Forall sem) = Forall (fmap f sem)
+  a <$ (Forall sem) = Forall (a <$ sem)
+instance
+  ( forall sem. Syntaxes syns sem => Applicative sem
+  , Functor (Forall syns)
+  ) =>
+  Applicative (Forall syns)
+  where
+  pure a = Forall (pure a)
+  liftA2 f (Forall a) (Forall b) = Forall (liftA2 f a b)
+  (<*>) (Forall f) (Forall a) = Forall ((<*>) f a)
+  (<*) (Forall f) (Forall a) = Forall ((<*) f a)
+  (*>) (Forall f) (Forall a) = Forall ((*>) f a)
+instance
+  ( forall sem. Syntaxes syns sem => Monad sem
+  , Applicative (Forall syns)
+  ) =>
+  Monad (Forall syns)
+  where
+  (>>=) (Forall sa) f = Forall (sa >>= \a -> case f a of Forall sb -> sb)
+  return = pure
+  (>>) = (*>)
+instance
+  (forall sem. Syntaxes syns sem => Unabstractable sem) =>
+  Unabstractable (Forall syns)
+  where
+  Forall a2b .@ Forall a = Forall (a2b .@ a)
+
+-- * Type 'PerSyntax'
+data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
+  PerSyntaxZ :: a syn -> PerSyntax (syn ': syns) a
+  PerSyntaxS :: PerSyntax syns a -> PerSyntax (skipSyn ': syns) a
+
+instance Eq (PerSyntax '[] a) where
+  (==) = \case {}
+instance
+  ( Eq (a syn)
+  , Eq (PerSyntax syns a)
+  ) =>
+  Eq (PerSyntax (syn ': syns) a)
+  where
+  PerSyntaxZ x == PerSyntaxZ y = x == y
+  PerSyntaxS x == PerSyntaxS y = x == y
+  _ == _ = False
+
+instance Show (PerSyntax '[] a) where
+  showsPrec _p = \case {}
+instance
+  ( Show (a syn)
+  , Show (PerSyntax syns a)
+  ) =>
+  Show (PerSyntax (syn ': syns) a)
+  where
+  showsPrec p = \case
+    PerSyntaxZ a -> showsPrec p a
+    PerSyntaxS s -> showsPrec p s
+
+-- ** Class 'PerSyntaxable'
+class PerSyntaxable (syns :: [Syntax]) (syn :: Syntax) where
+  perSyntax :: a syn -> PerSyntax syns a
+instance {-# OVERLAPS #-} PerSyntaxable (syn ': syns) syn where
+  perSyntax = PerSyntaxZ
+instance PerSyntaxable syns syn => PerSyntaxable (skipSyn ': syns) syn where
+  perSyntax = PerSyntaxS . perSyntax
diff --git a/src/Symantic/Syntaxes/Classes.hs b/src/Symantic/Syntaxes/Classes.hs
index 9d7bb42..2a5252e 100644
--- a/src/Symantic/Syntaxes/Classes.hs
+++ b/src/Symantic/Syntaxes/Classes.hs
@@ -42,10 +42,10 @@ type Syntax = Semantic -> Constraint
 
 -- | Merge several 'Syntax'es into a single one.
 --
--- Useful in 'IfSemantic'.
+-- Useful in 'IfSemantic' or 'All'.
 type family Syntaxes (syns :: [Syntax]) (sem :: Semantic) :: Constraint where
-  Syntaxes '[] sem = ()
-  Syntaxes (syn ': syns) sem = (syn sem, Syntaxes syns sem)
+  Syntaxes '[] sem = (() :: Constraint)
+  Syntaxes (syn ': syns) sem = ((syn sem, Syntaxes syns sem) :: Constraint)
 
 -- * Class 'Abstractable'
 class Unabstractable sem => Abstractable sem where
diff --git a/symantic-base.cabal b/symantic-base.cabal
index f5c0508..0cd2dcc 100644
--- a/symantic-base.cabal
+++ b/symantic-base.cabal
@@ -81,6 +81,7 @@ library
   exposed-modules:
     Symantic
     Symantic.Semantics
+    Symantic.Semantics.Forall
     Symantic.Semantics.Reader
     Symantic.Semantics.SharingObserver
     Symantic.Semantics.Viewer
-- 
2.44.1


From 8228beb80b11327567e3593c11af1c07d124b004 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Wed, 30 Aug 2023 22:14:21 +0200
Subject: [PATCH 09/16] iface: split syntax `Abstractable` into `Abstractable1`
 and `Varable`

---
 src/Symantic/Semantics/Reader.hs |  4 +++-
 src/Symantic/Semantics/Viewer.hs | 37 +++++++++++++-----------------
 src/Symantic/Syntaxes/Classes.hs | 32 ++++++++++++++------------
 src/Symantic/Syntaxes/Data.hs    | 39 +++++++++++++++++++++++---------
 src/Symantic/Syntaxes/Reify.hs   |  1 +
 5 files changed, 66 insertions(+), 47 deletions(-)

diff --git a/src/Symantic/Semantics/Reader.hs b/src/Symantic/Semantics/Reader.hs
index f6b16ff..7ec7494 100644
--- a/src/Symantic/Semantics/Reader.hs
+++ b/src/Symantic/Semantics/Reader.hs
@@ -23,8 +23,10 @@ instance LiftDerived4 (Reader r sem) where
   liftDerived4 f a b c d = Reader (\r -> f (unReader a r) (unReader b r) (unReader c r) (unReader d r))
 
 instance Unabstractable sem => Unabstractable (Reader r sem)
+instance Varable sem => Varable (Reader r sem)
 instance Abstractable sem => Abstractable (Reader r sem) where
   lam f = Reader (\r -> lam ((`unReader` r) . f . liftDerived))
+instance Abstractable1 sem => Abstractable1 (Reader r sem) where
   lam1 f = Reader (\r -> lam1 ((`unReader` r) . f . liftDerived))
 instance Functionable sem => Functionable (Reader r sem)
 instance Anythingable sem => Anythingable (Reader r sem)
@@ -35,7 +37,7 @@ instance IfThenElseable sem => IfThenElseable (Reader r sem)
 
 -- Using 'Inferable' with a specific @a@ and keeping @sem@ polymorphic
 -- is more usual; hence commenting this instance that would overlap.
---instance Inferable a sem => Inferable a (Reader r sem)
+-- instance Inferable a sem => Inferable a (Reader r sem)
 instance Listable sem => Listable (Reader r sem)
 instance Maybeable sem => Maybeable (Reader r sem)
 instance IsoFunctor sem => IsoFunctor (Reader r sem)
diff --git a/src/Symantic/Semantics/Viewer.hs b/src/Symantic/Semantics/Viewer.hs
index 03d7a3b..40744b3 100644
--- a/src/Symantic/Semantics/Viewer.hs
+++ b/src/Symantic/Semantics/Viewer.hs
@@ -71,27 +71,20 @@ pairViewer env op s =
     (o, c) = viewEnv_pair env
 
 instance Abstractable Viewer where
-  var = Fun.id
-  lam = viewLam "x"
-  lam1 = viewLam "u"
-viewLam :: String -> (Viewer a -> Viewer b) -> Viewer (a -> b)
-viewLam varPrefix f = Viewer Fun.$ \env ->
-  pairViewer env op Fun.$
-    let x =
-          showString varPrefix
-            Fun.. showsPrec 0 (viewEnv_lamDepth env)
-     in -- showString "Lam1 (" .
-        showString "\\" Fun.. x Fun.. showString " -> "
-          Fun.. runViewer
-            (f (Viewer (\_env -> x)))
-            env
-              { viewEnv_op = (op, SideL)
-              , viewEnv_lamDepth = Prelude.succ (viewEnv_lamDepth env)
-              }
-  where
-    -- . showString ")"
-
-    op = infixN 0
+  lam f = Viewer Fun.$ \env ->
+    pairViewer env op Fun.$
+      let x = showString "x" Fun.. shows (viewEnv_lamDepth env)
+       in showString "\\"
+            Fun.. x
+            Fun.. showString " -> "
+            Fun.. runViewer
+              (f (Viewer (\_env -> x)))
+              env
+                { viewEnv_op = (op, SideL)
+                , viewEnv_lamDepth = Prelude.succ (viewEnv_lamDepth env)
+                }
+    where
+      op = infixN 0
 instance Unabstractable Viewer where
   ViewerInfix op _name infixName .@ ViewerApp x y = Viewer Fun.$ \env ->
     pairViewer env op Fun.$
@@ -106,6 +99,8 @@ instance Unabstractable Viewer where
         Fun.. showString " "
         Fun.. showString name
   f .@ x = ViewerApp f x
+instance Varable Viewer where
+  var = Fun.id
 instance Anythingable Viewer
 instance Bottomable Viewer where
   bottom = "<hidden>"
diff --git a/src/Symantic/Syntaxes/Classes.hs b/src/Symantic/Syntaxes/Classes.hs
index 2a5252e..f084289 100644
--- a/src/Symantic/Syntaxes/Classes.hs
+++ b/src/Symantic/Syntaxes/Classes.hs
@@ -48,32 +48,34 @@ type family Syntaxes (syns :: [Syntax]) (sem :: Semantic) :: Constraint where
   Syntaxes (syn ': syns) sem = ((syn sem, Syntaxes syns sem) :: Constraint)
 
 -- * Class 'Abstractable'
-class Unabstractable sem => Abstractable sem where
+class Abstractable sem where
   -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
   lam :: (sem a -> sem b) -> sem (a -> b)
-
-  -- | Like 'lam' but whose argument must be used only once,
-  -- hence safe to beta-reduce (inline) without duplicating work.
-  lam1 :: (sem a -> sem b) -> sem (a -> b)
-
-  var :: sem a -> sem a
   lam f = liftDerived (lam (derive Fun.. f Fun.. liftDerived))
-  lam1 f = liftDerived (lam1 (derive Fun.. f Fun.. liftDerived))
-  var = liftDerived1 var
   default lam ::
     FromDerived Abstractable sem =>
     Derivable sem =>
     (sem a -> sem b) ->
     sem (a -> b)
+
+-- ** Class 'Abstractable1'
+class Abstractable1 sem where
+  -- | Like 'lam' but whose argument must be used only once,
+  -- hence safe to beta-reduce (inline) without duplicating work.
+  lam1 :: (sem a -> sem b) -> sem (a -> b)
+  lam1 f = liftDerived (lam1 (derive Fun.. f Fun.. liftDerived))
   default lam1 ::
-    FromDerived Abstractable sem =>
+    FromDerived Abstractable1 sem =>
     Derivable sem =>
     (sem a -> sem b) ->
     sem (a -> b)
-  default var ::
-    FromDerived1 Abstractable sem =>
-    sem a ->
-    sem a
+
+-- ** Class 'Varable'
+class Varable sem where
+  -- | Mark the use of a variable.
+  var :: sem a -> sem a
+  var = liftDerived1 var
+  default var :: FromDerived1 Varable sem => sem a -> sem a
 
 -- ** Class 'Unabstractable'
 class Unabstractable sem where
@@ -166,6 +168,7 @@ class Equalable sem where
 infix 4 `equal`, ==
 (==) ::
   Abstractable sem =>
+  Unabstractable sem =>
   Equalable sem =>
   Eq a =>
   sem a ->
@@ -418,6 +421,7 @@ class Semigroupable sem where
 infixr 6 `concat`, <>
 (<>) ::
   Abstractable sem =>
+  Unabstractable sem =>
   Semigroupable sem =>
   Semigroup a =>
   sem a ->
diff --git a/src/Symantic/Syntaxes/Data.hs b/src/Symantic/Syntaxes/Data.hs
index 7bee687..2b68d40 100644
--- a/src/Symantic/Syntaxes/Data.hs
+++ b/src/Symantic/Syntaxes/Data.hs
@@ -62,16 +62,28 @@ unSomeData (SomeData (constr :: Data actualSyn sem a)) =
 -- Abstractable
 data instance Data Abstractable sem a where
   Lam :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a -> b)
-  Lam1 :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a -> b)
-  Var :: sem a -> Data Abstractable sem a
-instance Abstractable sem => Derivable (Data Abstractable sem) where
+instance (Abstractable sem, Varable sem) => Derivable (Data Abstractable sem) where
   derive = \case
     Lam f -> lam (\x -> derive (f (SomeData (Var x))))
-    Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x))))
-    Var x -> var x
-instance Abstractable sem => Abstractable (SomeData sem) where
+instance (Abstractable sem, Varable sem) => Abstractable (SomeData sem) where
   lam f = SomeData (Lam f)
+
+-- Abstractable1
+data instance Data Abstractable1 sem a where
+  Lam1 :: (SomeData sem a -> SomeData sem b) -> Data Abstractable1 sem (a -> b)
+instance (Abstractable1 sem, Varable sem) => Derivable (Data Abstractable1 sem) where
+  derive = \case
+    Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x))))
+instance (Abstractable1 sem, Varable sem) => Abstractable1 (SomeData sem) where
   lam1 f = SomeData (Lam1 f)
+
+-- Varable
+data instance Data Varable sem a where
+  Var :: sem a -> Data Varable sem a
+instance Varable sem => Derivable (Data Varable sem) where
+  derive = \case
+    Var x -> var x
+instance Varable sem => Varable (SomeData sem) where
   var = Fun.id
 
 -- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
@@ -83,6 +95,9 @@ instance Abstractable sem => Abstractable (SomeData sem) where
 normalOrderReduction ::
   forall sem a.
   Abstractable sem =>
+  Abstractable1 sem =>
+  Unabstractable sem =>
+  Varable sem =>
   IfThenElseable sem =>
   SomeData sem a ->
   SomeData sem a
@@ -121,14 +136,16 @@ instance Unabstractable sem => Unabstractable (SomeData sem) where
 -- Functionable
 instance
   ( Abstractable sem
+  , Unabstractable sem
+  , Varable sem
   ) =>
   Functionable (SomeData sem)
   where
-  ($) = lam1 (\f -> lam1 (\x -> f .@ x))
-  (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
-  const = lam1 (\x -> lam1 (\_y -> x))
-  flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
-  id = lam1 (\x -> x)
+  ($) = lam (\f -> lam (\x -> f .@ x))
+  (.) = lam (\f -> lam (\g -> lam (\x -> f .@ (g .@ x))))
+  const = lam (\x -> lam (\_y -> x))
+  flip = lam (\f -> lam (\x -> lam (\y -> f .@ y .@ x)))
+  id = lam (\x -> x)
 
 -- Anythingable
 data instance Data Anythingable sem a where
diff --git a/src/Symantic/Syntaxes/Reify.hs b/src/Symantic/Syntaxes/Reify.hs
index 91d6db8..b3824f5 100644
--- a/src/Symantic/Syntaxes/Reify.hs
+++ b/src/Symantic/Syntaxes/Reify.hs
@@ -49,6 +49,7 @@ infixr 8 -->
 
 (-->) ::
   Abstractable repr =>
+  Unabstractable repr =>
   ReifyReflect repr m1 o1 ->
   ReifyReflect repr m2 o2 ->
   ReifyReflect repr (m1 -> m2) (o1 -> o2)
-- 
2.44.1


From f409f0538d6f1bdc1f1f4c1461f5e00943e30750 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Wed, 30 Aug 2023 22:15:21 +0200
Subject: [PATCH 10/16] iface: add syntax `Abstractable` to semantic `Forall`

---
 src/Symantic/Semantics/Forall.hs | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/src/Symantic/Semantics/Forall.hs b/src/Symantic/Semantics/Forall.hs
index e834857..9c75c60 100644
--- a/src/Symantic/Semantics/Forall.hs
+++ b/src/Symantic/Semantics/Forall.hs
@@ -5,6 +5,11 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE UndecidableInstances #-}
 
+-- | This module provides the 'Forall' semantic
+-- which preserves the polymorphism of the semantic.
+-- Useful when parsing the syntax from a text
+-- (ie. when the domain-specific language
+-- is not embedded into a Haskell file).
 module Symantic.Semantics.Forall where
 
 import Control.Applicative (Applicative (..))
@@ -15,8 +20,9 @@ import Data.Function ((.))
 import Data.Functor (Functor (..))
 import Data.Kind (Type)
 import Text.Show (Show (..))
+import Unsafe.Coerce (unsafeCoerce)
 
-import Symantic.Syntaxes.Classes (Syntax, Syntaxes, Unabstractable (..))
+import Symantic.Syntaxes.Classes (Syntax, Syntaxes, Unabstractable (..), Abstractable(..))
 
 -- * Type 'Forall'
 newtype Forall (syns :: [Syntax]) (a :: Type)
@@ -54,6 +60,17 @@ instance
   Unabstractable (Forall syns)
   where
   Forall a2b .@ Forall a = Forall (a2b .@ a)
+instance
+  ( forall sem. Syntaxes syns sem => Abstractable sem
+  , forall sem. Syntaxes syns sem => Unabstractable sem
+  ) =>
+  Abstractable (Forall syns)
+  where
+  lam f = Forall (lam (\a -> let Forall b = f (forallSem a) in b))
+    where
+      -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
+      forallSem :: sem a -> Forall syns a
+      forallSem a = Forall (unsafeCoerce a)
 
 -- * Type 'PerSyntax'
 data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
-- 
2.44.1


From 69ee3bd81a7cb2bd069065edbe1ac99dc6edc165 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Wed, 30 Aug 2023 22:15:48 +0200
Subject: [PATCH 11/16] doc: reformat comments

---
 src/Symantic/Syntaxes/Reify.hs | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Symantic/Syntaxes/Reify.hs b/src/Symantic/Syntaxes/Reify.hs
index b3824f5..915ad47 100644
--- a/src/Symantic/Syntaxes/Reify.hs
+++ b/src/Symantic/Syntaxes/Reify.hs
@@ -32,12 +32,12 @@ import Symantic.Syntaxes.Classes (Abstractable (..), Unabstractable (..))
 -- DOC: http://okmij.org/ftp/tagless-final/NBE.html
 -- DOC: https://www.dicosmo.org/Articles/2004-BalatDiCosmoFiore-Popl.pdf
 data ReifyReflect repr meta a = ReifyReflect
-  { -- | 'reflect' converts from a *represented* Haskell term of type @a@
-    -- to an object *representing* that value of type @a@.
-    reify :: meta -> repr a
-  , -- | 'reflect' converts back an object *representing* a value of type @a@,
-    -- to the *represented* Haskell term of type @a@.
-    reflect :: repr a -> meta
+  { reify :: meta -> repr a
+  -- ^ 'reflect' converts from a *represented* Haskell term of type @a@
+  -- to an object *representing* that value of type @a@.
+  , reflect :: repr a -> meta
+  -- ^ 'reflect' converts back an object *representing* a value of type @a@,
+  -- to the *represented* Haskell term of type @a@.
   }
 
 -- | The base of induction : placeholder for a type which is not the arrow type.
-- 
2.44.1


From 5be2aa310b3c593a6b8fd0471ade3122581ec40c Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Wed, 30 Aug 2023 23:25:10 +0200
Subject: [PATCH 12/16] doc: move description to modules' header

---
 src/Symantic/Semantics/Reader.hs           |  4 ++-
 src/Symantic/Semantics/SharingObserver.hs  | 30 ++++++++++++----
 src/Symantic/Semantics/Viewer.hs           |  3 ++
 src/Symantic/Semantics/Viewer/Fixity.hs    |  4 ++-
 src/Symantic/Syntaxes/Classes.hs           |  5 ++-
 src/Symantic/Syntaxes/CurryN.hs            |  2 ++
 src/Symantic/Syntaxes/Data.hs              |  4 +++
 src/Symantic/Syntaxes/Derive.hs            |  3 ++
 src/Symantic/Syntaxes/EithersOfTuples.hs   | 16 +++++----
 src/Symantic/Syntaxes/Reify.hs             |  7 +++-
 src/Symantic/Syntaxes/TuplesOfFunctions.hs | 13 +++----
 symantic-base.cabal                        | 41 +---------------------
 12 files changed, 68 insertions(+), 64 deletions(-)

diff --git a/src/Symantic/Semantics/Reader.hs b/src/Symantic/Semantics/Reader.hs
index 7ec7494..e44ec72 100644
--- a/src/Symantic/Semantics/Reader.hs
+++ b/src/Symantic/Semantics/Reader.hs
@@ -1,3 +1,5 @@
+-- | This module provides the 'Reader' semantic
+-- which enables to change the syntax combinators using an environment.
 module Symantic.Semantics.Reader where
 
 import Data.Function (const, (.))
@@ -7,7 +9,7 @@ import Symantic.Syntaxes.Derive
 
 -- * Type 'Reader'
 
--- | An intermediate interpreter exposing an environment.
+-- | An intermediate semantic exposing an environment.
 newtype Reader r sem a = Reader {unReader :: r -> sem a}
 
 type instance Derived (Reader r sem) = sem
diff --git a/src/Symantic/Semantics/SharingObserver.hs b/src/Symantic/Semantics/SharingObserver.hs
index 33a8860..ccda22b 100644
--- a/src/Symantic/Semantics/SharingObserver.hs
+++ b/src/Symantic/Semantics/SharingObserver.hs
@@ -8,6 +8,16 @@
 {-# LANGUAGE ExistentialQuantification #-}
 
 -- {-# LANGUAGE MagicHash #-} -- For unsafeCoerce#
+
+-- | This module provides the 'SharingObserver' semantic
+-- which interprets combinators to observe @let@ definitions
+-- at the host language level (Haskell),
+-- effectively turning infinite values into finite ones,
+-- which is useful for example to inspect
+-- and optimize recursive grammars.
+--
+-- Inspired by Andy Gill's [Type-safe observable sharing in Haskell](https://doi.org/10.1145/1596638.1596653).
+-- For an example, see [symantic-parser](https://hackage.haskell.org/package/symantic-parser).
 module Symantic.Semantics.SharingObserver where
 
 import Control.Applicative (Applicative (..))
@@ -152,7 +162,7 @@ observeSharing (SharingObserver m) =
               | (letName, refCount) <- HM.elems (oss_refs st)
               , refCount > 0
               ]
-       in --trace (show refs) $
+       in -- trace (show refs) $
           MT.runWriter $
             (`MT.runReaderT` refs) $
               unFinalizeSharing fs
@@ -270,7 +280,8 @@ instance
   liftDerived2 f a b =
     observeSharingNode $
       SharingObserver $
-        f <$> unSharingObserver a
+        f
+          <$> unSharingObserver a
           <*> unSharingObserver b
 instance
   ( Referenceable letName sem
@@ -284,7 +295,8 @@ instance
   liftDerived3 f a b c =
     observeSharingNode $
       SharingObserver $
-        f <$> unSharingObserver a
+        f
+          <$> unSharingObserver a
           <*> unSharingObserver b
           <*> unSharingObserver c
 instance
@@ -299,7 +311,8 @@ instance
   liftDerived4 f a b c d =
     observeSharingNode $
       SharingObserver $
-        f <$> unSharingObserver a
+        f
+          <$> unSharingObserver a
           <*> unSharingObserver b
           <*> unSharingObserver c
           <*> unSharingObserver d
@@ -339,7 +352,8 @@ instance
   where
   liftDerived2 f a b =
     SharingFinalizer $
-      f <$> unFinalizeSharing a
+      f
+        <$> unFinalizeSharing a
         <*> unFinalizeSharing b
 instance
   (Eq letName, Hashable letName) =>
@@ -347,7 +361,8 @@ instance
   where
   liftDerived3 f a b c =
     SharingFinalizer $
-      f <$> unFinalizeSharing a
+      f
+        <$> unFinalizeSharing a
         <*> unFinalizeSharing b
         <*> unFinalizeSharing c
 instance
@@ -356,7 +371,8 @@ instance
   where
   liftDerived4 f a b c d =
     SharingFinalizer $
-      f <$> unFinalizeSharing a
+      f
+        <$> unFinalizeSharing a
         <*> unFinalizeSharing b
         <*> unFinalizeSharing c
         <*> unFinalizeSharing d
diff --git a/src/Symantic/Semantics/Viewer.hs b/src/Symantic/Semantics/Viewer.hs
index 40744b3..e65ebbe 100644
--- a/src/Symantic/Semantics/Viewer.hs
+++ b/src/Symantic/Semantics/Viewer.hs
@@ -5,6 +5,8 @@
 -- For Show (SomeData a)
 {-# LANGUAGE UndecidableInstances #-}
 
+-- | This module provides the 'Viewer' semantic
+-- which interprets combinators as human-readable text.
 module Symantic.Semantics.Viewer where
 
 import Data.Function qualified as Fun
@@ -18,6 +20,7 @@ import Symantic.Syntaxes.Classes
 import Symantic.Syntaxes.Data
 import Symantic.Syntaxes.Derive
 
+-- * Type 'Viewer'
 data Viewer a where
   Viewer :: (ViewerEnv -> ShowS) -> Viewer a
   ViewerUnifix :: Unifix -> String -> String -> Viewer (a -> b)
diff --git a/src/Symantic/Semantics/Viewer/Fixity.hs b/src/Symantic/Semantics/Viewer/Fixity.hs
index 3cee08f..71a1742 100644
--- a/src/Symantic/Semantics/Viewer/Fixity.hs
+++ b/src/Symantic/Semantics/Viewer/Fixity.hs
@@ -1,3 +1,5 @@
+-- | This module gathers utilities for parsing or viewing
+-- infix, prefix and postfix combinators.
 module Symantic.Semantics.Viewer.Fixity where
 
 import Data.Bool
@@ -55,7 +57,7 @@ isPairNeeded :: (Infix, Side) -> Infix -> Bool
 isPairNeeded (po, lr) op =
   infix_precedence op < infix_precedence po
     || infix_precedence op == infix_precedence po
-    && not associate
+      && not associate
   where
     associate =
       case (lr, infix_associativity po) of
diff --git a/src/Symantic/Syntaxes/Classes.hs b/src/Symantic/Syntaxes/Classes.hs
index f084289..4c612f7 100644
--- a/src/Symantic/Syntaxes/Classes.hs
+++ b/src/Symantic/Syntaxes/Classes.hs
@@ -11,7 +11,10 @@
 -- For Permutation
 {-# LANGUAGE UndecidableInstances #-}
 
--- | Combinators in this module conflict with usual ones from the @Prelude@
+-- | This module gathers commonly used tagless-final combinators
+-- (the syntax part of symantics).
+--
+-- Note: combinators in this module conflict with usual ones from the @Prelude@
 -- hence they are meant to be imported either explicitely or qualified.
 module Symantic.Syntaxes.Classes where
 
diff --git a/src/Symantic/Syntaxes/CurryN.hs b/src/Symantic/Syntaxes/CurryN.hs
index 93602c5..deb94a3 100644
--- a/src/Symantic/Syntaxes/CurryN.hs
+++ b/src/Symantic/Syntaxes/CurryN.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE DataKinds #-}
 
+-- | This module gathers utilities for currying or uncurrying tuples
+-- of size greater or equal to two.
 module Symantic.Syntaxes.CurryN where
 
 import Data.Function (($), (.))
diff --git a/src/Symantic/Syntaxes/Data.hs b/src/Symantic/Syntaxes/Data.hs
index 2b68d40..6678e49 100644
--- a/src/Symantic/Syntaxes/Data.hs
+++ b/src/Symantic/Syntaxes/Data.hs
@@ -6,6 +6,10 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ViewPatterns #-}
 
+-- | This module provides the intermediate semantic 'SomeData'
+-- which interprets combinators as data constructors.
+-- This enables to pattern-match on combinators
+-- while keeping their extensibility.
 module Symantic.Syntaxes.Data where
 
 import Data.Bool (Bool)
diff --git a/src/Symantic/Syntaxes/Derive.hs b/src/Symantic/Syntaxes/Derive.hs
index 12f4b5a..7535af8 100644
--- a/src/Symantic/Syntaxes/Derive.hs
+++ b/src/Symantic/Syntaxes/Derive.hs
@@ -6,6 +6,9 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE PolyKinds #-}
 
+-- | This modules enables to give a default value to combinators
+-- when it is possible to factorize the implementation of some combinators
+-- for a given semantic.
 module Symantic.Syntaxes.Derive where
 
 import Data.Function ((.))
diff --git a/src/Symantic/Syntaxes/EithersOfTuples.hs b/src/Symantic/Syntaxes/EithersOfTuples.hs
index cb87319..915de98 100644
--- a/src/Symantic/Syntaxes/EithersOfTuples.hs
+++ b/src/Symantic/Syntaxes/EithersOfTuples.hs
@@ -5,13 +5,15 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE UndecidableInstances #-}
 
--- | EOT (Either of Tuples) to/from ADT (Algebraic Data Type).
--- to produce or consume custom ADT with @('<.>')@ and @('<+>')@.
+-- | This modules leverages @GHC.Generics@ to generate reciprocal functions
+-- between algebraic data type (aka. ADT) constructors
+-- and Eithers-of-Tuples (aka. EOT).
 --
 -- This is like what is done in @generic-sop@:
 -- https://hackage.haskell.org/package/generics-sop-0.5.1.0/docs/src/Generics.SOP.GGP.html#gSumFrom
 -- but using directly 'Either' and 'Tuples'
--- instead of passing by the intermediary GADTs @NP@ and @NS@.
+-- instead of passing by the intermediary GADTs @NP@ and @NS@,
+-- enabling to produce or consume custom ADT with @('<.>')@ and @('<+>')@.
 module Symantic.Syntaxes.EithersOfTuples where
 
 import Data.Either (Either (..))
@@ -27,12 +29,12 @@ import GHC.Generics as Generics
 -- and their associativity and precedence,
 -- with no parenthesis messing around.
 type family EoT (adt :: [[Type]]) :: Type where
--- This is 'absurd'
+  -- This is 'absurd'
   EoT '[] = Void
--- There Is No Alternative
+  -- There Is No Alternative
   EoT '[ps] = Tuples ps
--- The right associativity of @('<+>')@
--- puts leaves on 'Left' and nodes on 'Right'
+  -- The right associativity of @('<+>')@
+  -- puts leaves on 'Left' and nodes on 'Right'
   EoT (ps ': ss) = Either (Tuples ps) (EoT ss)
 
 -- * Type family 'Tuples'
diff --git a/src/Symantic/Syntaxes/Reify.hs b/src/Symantic/Syntaxes/Reify.hs
index 915ad47..4327b22 100644
--- a/src/Symantic/Syntaxes/Reify.hs
+++ b/src/Symantic/Syntaxes/Reify.hs
@@ -2,7 +2,12 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
 
--- | Reify an Haskell value using type-directed normalisation-by-evaluation (NBE).
+-- | This module enables the lifting to any interpreter of any Haskell functions,
+-- taking as arguments only polymorphic types (possibly constrained)
+-- or functions using such types.
+--
+-- This reification of an Haskell value using type-directed normalisation-by-evaluation (NBE),
+-- is inspired by Oleg Kiselyov's [TDPE.hs](http://okmij.org/ftp/tagless-final/course/TDPE.hs).
 module Symantic.Syntaxes.Reify where
 
 import Control.Monad (Monad (..))
diff --git a/src/Symantic/Syntaxes/TuplesOfFunctions.hs b/src/Symantic/Syntaxes/TuplesOfFunctions.hs
index e2723d2..8337a6c 100644
--- a/src/Symantic/Syntaxes/TuplesOfFunctions.hs
+++ b/src/Symantic/Syntaxes/TuplesOfFunctions.hs
@@ -3,7 +3,8 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE UndecidableInstances #-}
 
--- | Tuples-of-Functions
+-- | This module enables the use of Tuples-of-Functions
+-- instead of Eithers-of-Tuples.
 module Symantic.Syntaxes.TuplesOfFunctions where
 
 import Data.Bool (Bool (..))
@@ -52,15 +53,15 @@ infixr 0 -->
 -- pattern-matched from a constructor
 -- of such algebraic datatype.
 type family ToFIf (t :: Bool) a next :: Type where
--- Curry on '<.>'.
+  -- Curry on '<.>'.
   ToFIf 'True (a, b) next = a --> b --> next
--- Branch on '<+>'.
+  -- Branch on '<+>'.
   ToFIf 'True (Either a b) next = (a --> next, b --> next)
--- Skip '()' as argument.
+  -- Skip '()' as argument.
   ToFIf 'True () next = next
--- Enable a different return value for each function.
+  -- Enable a different return value for each function.
   ToFIf 'True (Endpoint sem a) next = ToFEndpoint sem a next
--- Everything else becomes a new argument.
+  -- Everything else becomes a new argument.
   ToFIf 'False a next = a -> next
 
 -- ** Type family 'IsToF'
diff --git a/symantic-base.cabal b/symantic-base.cabal
index 0cd2dcc..4cad644 100644
--- a/symantic-base.cabal
+++ b/symantic-base.cabal
@@ -19,46 +19,7 @@ synopsis:
 
 description:
   This is a work-in-progress collection of basic tagless-final combinators,
-  along with some advanced utilities to exploit them.
-  * @Symantic.Syntaxes.Classes@
-  gathers commonly used tagless-final combinators
-  (the syntax part of symantics).
-  * @Symantic.Syntaxes.Data@ interprets combinators as data constructors
-  enabling to pattern-match on combinators while keeping their extensibility.
-  * @Symantic.Syntaxes.Derive@
-  to give a default value to combinators which avoids boilerplate code
-  when implementing combinators for an interpreter is factorizable.
-  * @Symantic.Syntaxes.EithersOfTuples@
-  leverages @GHC.Generics@ to generate reciprocal functions
-  between algebraic data type constructors and Eithers-of-Tuples.
-  * @Symantic.Syntaxes.TuplesOfFunctions@
-  enables the use of Tuples-of-Functions
-  instead of Eithers-of-Tuples.
-  * @Symantic.Syntaxes.CurryN@
-  gathers utilities for currying or uncurrying tuples
-  of size greater or equal to two.
-  * @Symantic.Semantics.SharingObserver@
-  interprets combinators to observe @let@ definitions
-  at the host language level (Haskell),
-  effectively turning infinite values into finite ones,
-  which is useful for example to inspect
-  and optimize recursive grammars.
-  Inspired by Andy Gill's [Type-safe observable sharing in Haskell](https://doi.org/10.1145/1596638.1596653).
-  For an example, see [symantic-parser](https://hackage.haskell.org/package/symantic-parser).
-  * @Symantic.Semantics.Viewer@
-  interprets combinators as human-readable text.
-  * @Symantic.Semantics.Viewer.Fixity@
-  gathers utilities for parsing or viewing
-  infix, prefix and postfix combinators.
-  * @Symantic.Syntaxes.Reader@
-  is an intermediate interpreter enabling to change
-  the syntax combinators using an environment.
-  * @Symantic.Utils.Reify@
-  enables the lifting to any interpreter
-  of any Haskell functions taking as arguments
-  only polymorphic types (possibly constrained)
-  or functions using such types.
-  Inspired by Oleg Kiselyov's [TDPE.hs](http://okmij.org/ftp/tagless-final/course/TDPE.hs).
+  along with some experimental utilities to exploit them.
 
 build-type:         Simple
 tested-with:        GHC ==8.10.4
-- 
2.44.1


From 0462d776051002896a5859cc9b26adc8087fb8ef Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Wed, 30 Aug 2023 23:46:34 +0200
Subject: [PATCH 13/16] iface: add semantic `Identity`

---
 src/Symantic/Semantics.hs          |  4 +++
 src/Symantic/Semantics/Identity.hs | 53 ++++++++++++++++++++++++++++++
 symantic-base.cabal                |  2 ++
 3 files changed, 59 insertions(+)
 create mode 100644 src/Symantic/Semantics/Identity.hs

diff --git a/src/Symantic/Semantics.hs b/src/Symantic/Semantics.hs
index 13ccce5..7b2fb73 100644
--- a/src/Symantic/Semantics.hs
+++ b/src/Symantic/Semantics.hs
@@ -1,11 +1,15 @@
 module Symantic.Semantics (
+  module Symantic.Semantics.Data,
   module Symantic.Semantics.Forall,
+  module Symantic.Semantics.Identity,
   module Symantic.Semantics.Reader,
   module Symantic.Semantics.SharingObserver,
   module Symantic.Semantics.Viewer,
 ) where
 
+import Symantic.Semantics.Data
 import Symantic.Semantics.Forall
+import Symantic.Semantics.Identity
 import Symantic.Semantics.Reader
 import Symantic.Semantics.SharingObserver
 import Symantic.Semantics.Viewer
diff --git a/src/Symantic/Semantics/Identity.hs b/src/Symantic/Semantics/Identity.hs
new file mode 100644
index 0000000..0d730cd
--- /dev/null
+++ b/src/Symantic/Semantics/Identity.hs
@@ -0,0 +1,53 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-- | This module provides the 'Identity' semantic
+-- which interprets the combinators as a Haskell value.
+module Symantic.Semantics.Identity
+  ( Identity(..)
+  ) where
+
+import Control.Applicative qualified as App
+import Data.Either qualified as Either
+import Data.Eq qualified as Eq
+import Data.Function qualified as Fun
+import Data.Functor.Identity (Identity(..))
+import Data.Maybe qualified as Maybe
+
+import Symantic.Syntaxes.Classes
+
+-- * Type 'Identity'
+
+instance Abstractable Identity where
+  lam f = Identity (runIdentity Fun.. f Fun.. Identity)
+instance Abstractable1 Identity where
+  lam1 f = Identity (runIdentity Fun.. f Fun.. Identity)
+instance Anythingable Identity
+instance Constantable c Identity where
+  constant = Identity
+instance Eitherable Identity where
+  either = Identity Either.either
+  left = Identity Either.Left
+  right = Identity Either.Right
+instance Equalable Identity where
+  equal = Identity (Eq.==)
+instance IfThenElseable Identity where
+  ifThenElse test ok ko = Identity
+    (if runIdentity test
+    then runIdentity ok
+    else runIdentity ko)
+instance Instantiable Identity where
+  Identity f .@ Identity x = Identity (f x)
+instance Listable Identity where
+  cons = Identity (:)
+  nil = Identity []
+instance Maybeable Identity where
+  nothing = Identity Maybe.Nothing
+  just = Identity Maybe.Just
+instance Unabstractable Identity where
+  ap = Identity (App.<*>)
+  const = Identity Fun.const
+  id = Identity Fun.id
+  (.) = Identity (Fun..)
+  flip = Identity Fun.flip
+  ($) = Identity (Fun.$)
+instance Varable Identity where
+  var = Fun.id
diff --git a/symantic-base.cabal b/symantic-base.cabal
index 4cad644..91573aa 100644
--- a/symantic-base.cabal
+++ b/symantic-base.cabal
@@ -42,7 +42,9 @@ library
   exposed-modules:
     Symantic
     Symantic.Semantics
+    Symantic.Semantics.Data
     Symantic.Semantics.Forall
+    Symantic.Semantics.Identity
     Symantic.Semantics.Reader
     Symantic.Semantics.SharingObserver
     Symantic.Semantics.Viewer
-- 
2.44.1


From 99fb33d91ee7945c27f7a801a99a23c07c97b832 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Wed, 30 Aug 2023 23:55:46 +0200
Subject: [PATCH 14/16] iface: move `Syntaxes.Data` to `Semantics.Data`

---
 src/Symantic/{Syntaxes => Semantics}/Data.hs | 2 +-
 src/Symantic/Semantics/Forall.hs             | 2 +-
 src/Symantic/Semantics/Viewer.hs             | 2 +-
 src/Symantic/Syntaxes.hs                     | 2 --
 symantic-base.cabal                          | 1 -
 5 files changed, 3 insertions(+), 6 deletions(-)
 rename src/Symantic/{Syntaxes => Semantics}/Data.hs (99%)

diff --git a/src/Symantic/Syntaxes/Data.hs b/src/Symantic/Semantics/Data.hs
similarity index 99%
rename from src/Symantic/Syntaxes/Data.hs
rename to src/Symantic/Semantics/Data.hs
index 6678e49..accd10d 100644
--- a/src/Symantic/Syntaxes/Data.hs
+++ b/src/Symantic/Semantics/Data.hs
@@ -10,7 +10,7 @@
 -- which interprets combinators as data constructors.
 -- This enables to pattern-match on combinators
 -- while keeping their extensibility.
-module Symantic.Syntaxes.Data where
+module Symantic.Semantics.Data where
 
 import Data.Bool (Bool)
 import Data.Either (Either)
diff --git a/src/Symantic/Semantics/Forall.hs b/src/Symantic/Semantics/Forall.hs
index 9c75c60..a739dc8 100644
--- a/src/Symantic/Semantics/Forall.hs
+++ b/src/Symantic/Semantics/Forall.hs
@@ -22,7 +22,7 @@ import Data.Kind (Type)
 import Text.Show (Show (..))
 import Unsafe.Coerce (unsafeCoerce)
 
-import Symantic.Syntaxes.Classes (Syntax, Syntaxes, Unabstractable (..), Abstractable(..))
+import Symantic.Syntaxes.Classes (Abstractable (..), Syntax, Syntaxes, Unabstractable (..))
 
 -- * Type 'Forall'
 newtype Forall (syns :: [Syntax]) (a :: Type)
diff --git a/src/Symantic/Semantics/Viewer.hs b/src/Symantic/Semantics/Viewer.hs
index e65ebbe..628eb57 100644
--- a/src/Symantic/Semantics/Viewer.hs
+++ b/src/Symantic/Semantics/Viewer.hs
@@ -15,9 +15,9 @@ import Data.String
 import Text.Show
 import Prelude qualified
 
+import Symantic.Semantics.Data
 import Symantic.Semantics.Viewer.Fixity
 import Symantic.Syntaxes.Classes
-import Symantic.Syntaxes.Data
 import Symantic.Syntaxes.Derive
 
 -- * Type 'Viewer'
diff --git a/src/Symantic/Syntaxes.hs b/src/Symantic/Syntaxes.hs
index ec361b4..f866dd4 100644
--- a/src/Symantic/Syntaxes.hs
+++ b/src/Symantic/Syntaxes.hs
@@ -1,7 +1,6 @@
 module Symantic.Syntaxes (
   module Symantic.Syntaxes.Classes,
   module Symantic.Syntaxes.CurryN,
-  module Symantic.Syntaxes.Data,
   module Symantic.Syntaxes.Derive,
   module Symantic.Syntaxes.EithersOfTuples,
   module Symantic.Syntaxes.Reify,
@@ -10,7 +9,6 @@ module Symantic.Syntaxes (
 
 import Symantic.Syntaxes.Classes
 import Symantic.Syntaxes.CurryN
-import Symantic.Syntaxes.Data
 import Symantic.Syntaxes.Derive
 import Symantic.Syntaxes.EithersOfTuples
 import Symantic.Syntaxes.Reify
diff --git a/symantic-base.cabal b/symantic-base.cabal
index 91573aa..0713d42 100644
--- a/symantic-base.cabal
+++ b/symantic-base.cabal
@@ -52,7 +52,6 @@ library
     Symantic.Syntaxes
     Symantic.Syntaxes.Classes
     Symantic.Syntaxes.CurryN
-    Symantic.Syntaxes.Data
     Symantic.Syntaxes.Derive
     Symantic.Syntaxes.EithersOfTuples
     Symantic.Syntaxes.Reify
-- 
2.44.1


From 1671e3447295c45967abd3bce176a9e1151923fb Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Tue, 5 Sep 2023 01:11:01 +0200
Subject: [PATCH 15/16] iface: rename syntax `Unabstractable` to `Instantiable`

---
 src/Symantic/Semantics/Data.hs   | 14 +++++++-------
 src/Symantic/Semantics/Forall.hs | 12 +++++-------
 src/Symantic/Semantics/Reader.hs |  6 +++---
 src/Symantic/Semantics/Viewer.hs |  2 +-
 src/Symantic/Syntaxes/Classes.hs | 12 ++++++------
 src/Symantic/Syntaxes/Reify.hs   |  4 ++--
 6 files changed, 24 insertions(+), 26 deletions(-)

diff --git a/src/Symantic/Semantics/Data.hs b/src/Symantic/Semantics/Data.hs
index accd10d..5266a4e 100644
--- a/src/Symantic/Semantics/Data.hs
+++ b/src/Symantic/Semantics/Data.hs
@@ -100,7 +100,7 @@ normalOrderReduction ::
   forall sem a.
   Abstractable sem =>
   Abstractable1 sem =>
-  Unabstractable sem =>
+  Instantiable sem =>
   Varable sem =>
   IfThenElseable sem =>
   SomeData sem a ->
@@ -128,19 +128,19 @@ normalOrderReduction = nor
         x' -> x' .@ y
       x -> x
 
--- Unabstractable
-data instance Data Unabstractable sem a where
-  (:@) :: SomeData sem (a -> b) -> SomeData sem a -> Data Unabstractable sem b
-instance Unabstractable sem => Derivable (Data Unabstractable sem) where
+-- Instantiable
+data instance Data Instantiable sem a where
+  (:@) :: SomeData sem (a -> b) -> SomeData sem a -> Data Instantiable sem b
+instance Instantiable sem => Derivable (Data Instantiable sem) where
   derive = \case
     f :@ x -> derive f .@ derive x
-instance Unabstractable sem => Unabstractable (SomeData sem) where
+instance Instantiable sem => Instantiable (SomeData sem) where
   f .@ x = SomeData (f :@ x)
 
 -- Functionable
 instance
   ( Abstractable sem
-  , Unabstractable sem
+  , Instantiable sem
   , Varable sem
   ) =>
   Functionable (SomeData sem)
diff --git a/src/Symantic/Semantics/Forall.hs b/src/Symantic/Semantics/Forall.hs
index a739dc8..30df501 100644
--- a/src/Symantic/Semantics/Forall.hs
+++ b/src/Symantic/Semantics/Forall.hs
@@ -22,7 +22,7 @@ import Data.Kind (Type)
 import Text.Show (Show (..))
 import Unsafe.Coerce (unsafeCoerce)
 
-import Symantic.Syntaxes.Classes (Abstractable (..), Syntax, Syntaxes, Unabstractable (..))
+import Symantic.Syntaxes.Classes (Abstractable (..), Syntax, Syntaxes, Instantiable (..), Unabstractable (..))
 
 -- * Type 'Forall'
 newtype Forall (syns :: [Syntax]) (a :: Type)
@@ -56,16 +56,14 @@ instance
   return = pure
   (>>) = (*>)
 instance
-  (forall sem. Syntaxes syns sem => Unabstractable sem) =>
-  Unabstractable (Forall syns)
+  (forall sem. Syntaxes syns sem => Instantiable sem) =>
+  Instantiable (Forall syns)
   where
   Forall a2b .@ Forall a = Forall (a2b .@ a)
 instance
   ( forall sem. Syntaxes syns sem => Abstractable sem
-  , forall sem. Syntaxes syns sem => Unabstractable sem
-  ) =>
-  Abstractable (Forall syns)
-  where
+  , forall sem. Syntaxes syns sem => Instantiable sem
+  ) => Abstractable (Forall syns) where
   lam f = Forall (lam (\a -> let Forall b = f (forallSem a) in b))
     where
       -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
diff --git a/src/Symantic/Semantics/Reader.hs b/src/Symantic/Semantics/Reader.hs
index e44ec72..4296a85 100644
--- a/src/Symantic/Semantics/Reader.hs
+++ b/src/Symantic/Semantics/Reader.hs
@@ -24,13 +24,13 @@ instance LiftDerived3 (Reader r sem) where
 instance LiftDerived4 (Reader r sem) where
   liftDerived4 f a b c d = Reader (\r -> f (unReader a r) (unReader b r) (unReader c r) (unReader d r))
 
-instance Unabstractable sem => Unabstractable (Reader r sem)
-instance Varable sem => Varable (Reader r sem)
 instance Abstractable sem => Abstractable (Reader r sem) where
   lam f = Reader (\r -> lam ((`unReader` r) . f . liftDerived))
 instance Abstractable1 sem => Abstractable1 (Reader r sem) where
   lam1 f = Reader (\r -> lam1 ((`unReader` r) . f . liftDerived))
-instance Functionable sem => Functionable (Reader r sem)
+instance Instantiable sem => Instantiable (Reader r sem)
+instance Unabstractable sem => Unabstractable (Reader r sem)
+instance Varable sem => Varable (Reader r sem)
 instance Anythingable sem => Anythingable (Reader r sem)
 instance Constantable c sem => Constantable c (Reader r sem)
 instance Eitherable sem => Eitherable (Reader r sem)
diff --git a/src/Symantic/Semantics/Viewer.hs b/src/Symantic/Semantics/Viewer.hs
index 628eb57..48450a4 100644
--- a/src/Symantic/Semantics/Viewer.hs
+++ b/src/Symantic/Semantics/Viewer.hs
@@ -88,7 +88,7 @@ instance Abstractable Viewer where
                 }
     where
       op = infixN 0
-instance Unabstractable Viewer where
+instance Instantiable Viewer where
   ViewerInfix op _name infixName .@ ViewerApp x y = Viewer Fun.$ \env ->
     pairViewer env op Fun.$
       runViewer x env{viewEnv_op = (op, SideL)}
diff --git a/src/Symantic/Syntaxes/Classes.hs b/src/Symantic/Syntaxes/Classes.hs
index 4c612f7..88d2f02 100644
--- a/src/Symantic/Syntaxes/Classes.hs
+++ b/src/Symantic/Syntaxes/Classes.hs
@@ -80,15 +80,15 @@ class Varable sem where
   var = liftDerived1 var
   default var :: FromDerived1 Varable sem => sem a -> sem a
 
--- ** Class 'Unabstractable'
-class Unabstractable sem where
-  -- | Application, aka. unabstract.
+-- ** Class 'Instantiable'
+class Instantiable sem where
+  -- | Instantiate.
   (.@) :: sem (a -> b) -> sem a -> sem b
 
   infixl 9 .@
   (.@) = liftDerived2 (.@)
   default (.@) ::
-    FromDerived2 Unabstractable sem =>
+    FromDerived2 Instantiable sem =>
     sem (a -> b) ->
     sem a ->
     sem b
@@ -171,7 +171,7 @@ class Equalable sem where
 infix 4 `equal`, ==
 (==) ::
   Abstractable sem =>
-  Unabstractable sem =>
+  Instantiable sem =>
   Equalable sem =>
   Eq a =>
   sem a ->
@@ -424,7 +424,7 @@ class Semigroupable sem where
 infixr 6 `concat`, <>
 (<>) ::
   Abstractable sem =>
-  Unabstractable sem =>
+  Instantiable sem =>
   Semigroupable sem =>
   Semigroup a =>
   sem a ->
diff --git a/src/Symantic/Syntaxes/Reify.hs b/src/Symantic/Syntaxes/Reify.hs
index 4327b22..2db58be 100644
--- a/src/Symantic/Syntaxes/Reify.hs
+++ b/src/Symantic/Syntaxes/Reify.hs
@@ -14,7 +14,7 @@ import Control.Monad (Monad (..))
 import Data.Function qualified as Fun
 import Language.Haskell.TH qualified as TH
 
-import Symantic.Syntaxes.Classes (Abstractable (..), Unabstractable (..))
+import Symantic.Syntaxes.Classes (Abstractable (..), Instantiable (..))
 
 -- | 'ReifyReflect' witnesses the duality between @meta@ and @(repr a)@.
 --  It indicates which type variables in @a@ are not to be instantiated
@@ -54,7 +54,7 @@ infixr 8 -->
 
 (-->) ::
   Abstractable repr =>
-  Unabstractable repr =>
+  Instantiable repr =>
   ReifyReflect repr m1 o1 ->
   ReifyReflect repr m2 o2 ->
   ReifyReflect repr (m1 -> m2) (o1 -> o2)
-- 
2.44.1


From 0d3539676f7c7316ef688c4fda92e5aae39a42cd Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Tue, 5 Sep 2023 01:11:39 +0200
Subject: [PATCH 16/16] iface: rename syntax `Functionable` to `Unabstractable`

---
 src/Symantic/Semantics/Data.hs   | 11 ++++-----
 src/Symantic/Semantics/Forall.hs | 25 ++++++++++++---------
 src/Symantic/Semantics/Viewer.hs |  7 ++++++
 src/Symantic/Syntaxes/Classes.hs | 38 +++++++++++++++++++++++---------
 4 files changed, 54 insertions(+), 27 deletions(-)

diff --git a/src/Symantic/Semantics/Data.hs b/src/Symantic/Semantics/Data.hs
index 5266a4e..1118470 100644
--- a/src/Symantic/Semantics/Data.hs
+++ b/src/Symantic/Semantics/Data.hs
@@ -137,19 +137,20 @@ instance Instantiable sem => Derivable (Data Instantiable sem) where
 instance Instantiable sem => Instantiable (SomeData sem) where
   f .@ x = SomeData (f :@ x)
 
--- Functionable
+-- Unabstractable
 instance
   ( Abstractable sem
   , Instantiable sem
   , Varable sem
   ) =>
-  Functionable (SomeData sem)
+  Unabstractable (SomeData sem)
   where
-  ($) = lam (\f -> lam (\x -> f .@ x))
-  (.) = lam (\f -> lam (\g -> lam (\x -> f .@ (g .@ x))))
+  ap = lam (\abc -> lam (\ab -> lam (\a -> abc .@ a .@ (ab .@ a))))
   const = lam (\x -> lam (\_y -> x))
-  flip = lam (\f -> lam (\x -> lam (\y -> f .@ y .@ x)))
   id = lam (\x -> x)
+  (.) = lam (\f -> lam (\g -> lam (\x -> f .@ (g .@ x))))
+  flip = lam (\f -> lam (\x -> lam (\y -> f .@ y .@ x)))
+  ($) = lam (\f -> lam (\x -> f .@ x))
 
 -- Anythingable
 data instance Data Anythingable sem a where
diff --git a/src/Symantic/Semantics/Forall.hs b/src/Symantic/Semantics/Forall.hs
index 30df501..c959c5f 100644
--- a/src/Symantic/Semantics/Forall.hs
+++ b/src/Symantic/Semantics/Forall.hs
@@ -16,11 +16,11 @@ import Control.Applicative (Applicative (..))
 import Control.Monad (Monad (..))
 import Data.Bool (Bool (..))
 import Data.Eq (Eq (..))
-import Data.Function ((.))
 import Data.Functor (Functor (..))
 import Data.Kind (Type)
 import Text.Show (Show (..))
 import Unsafe.Coerce (unsafeCoerce)
+import qualified Data.Function as Fun
 
 import Symantic.Syntaxes.Classes (Abstractable (..), Syntax, Syntaxes, Instantiable (..), Unabstractable (..))
 
@@ -30,17 +30,13 @@ newtype Forall (syns :: [Syntax]) (a :: Type)
 
 instance
   ( forall sem. Syntaxes syns sem => Functor sem
-  ) =>
-  Functor (Forall syns)
-  where
+  ) => Functor (Forall syns) where
   fmap f (Forall sem) = Forall (fmap f sem)
   a <$ (Forall sem) = Forall (a <$ sem)
 instance
   ( forall sem. Syntaxes syns sem => Applicative sem
   , Functor (Forall syns)
-  ) =>
-  Applicative (Forall syns)
-  where
+  ) => Applicative (Forall syns) where
   pure a = Forall (pure a)
   liftA2 f (Forall a) (Forall b) = Forall (liftA2 f a b)
   (<*>) (Forall f) (Forall a) = Forall ((<*>) f a)
@@ -49,9 +45,7 @@ instance
 instance
   ( forall sem. Syntaxes syns sem => Monad sem
   , Applicative (Forall syns)
-  ) =>
-  Monad (Forall syns)
-  where
+  ) => Monad (Forall syns) where
   (>>=) (Forall sa) f = Forall (sa >>= \a -> case f a of Forall sb -> sb)
   return = pure
   (>>) = (*>)
@@ -69,6 +63,15 @@ instance
       -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
       forallSem :: sem a -> Forall syns a
       forallSem a = Forall (unsafeCoerce a)
+instance
+  ( forall sem. Syntaxes syns sem => Unabstractable sem
+  ) => Unabstractable (Forall syns) where
+  ap = Forall ap
+  const = Forall const
+  id = Forall id
+  (.) = Forall (.)
+  flip = Forall flip
+  ($) = Forall ($)
 
 -- * Type 'PerSyntax'
 data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
@@ -105,4 +108,4 @@ class PerSyntaxable (syns :: [Syntax]) (syn :: Syntax) where
 instance {-# OVERLAPS #-} PerSyntaxable (syn ': syns) syn where
   perSyntax = PerSyntaxZ
 instance PerSyntaxable syns syn => PerSyntaxable (skipSyn ': syns) syn where
-  perSyntax = PerSyntaxS . perSyntax
+  perSyntax = PerSyntaxS Fun.. perSyntax
diff --git a/src/Symantic/Semantics/Viewer.hs b/src/Symantic/Semantics/Viewer.hs
index 48450a4..5fb6d6b 100644
--- a/src/Symantic/Semantics/Viewer.hs
+++ b/src/Symantic/Semantics/Viewer.hs
@@ -102,6 +102,13 @@ instance Instantiable Viewer where
         Fun.. showString " "
         Fun.. showString name
   f .@ x = ViewerApp f x
+instance Unabstractable Viewer where
+  ap = ViewerInfix (infixL 4) "(<*>)" "<*>"
+  const = "const"
+  id = "id"
+  (.) = ViewerInfix (infixR 9) "(.)" "."
+  flip = flip
+  ($) = ViewerInfix (infixR 0) "($)" "$"
 instance Varable Viewer where
   var = Fun.id
 instance Anythingable Viewer
diff --git a/src/Symantic/Syntaxes/Classes.hs b/src/Symantic/Syntaxes/Classes.hs
index 88d2f02..f72b6de 100644
--- a/src/Symantic/Syntaxes/Classes.hs
+++ b/src/Symantic/Syntaxes/Classes.hs
@@ -93,34 +93,50 @@ class Instantiable sem where
     sem a ->
     sem b
 
--- ** Class 'Functionable'
-class Functionable sem where
+-- ** Class 'Unabstractable'
+-- | All operations in lambda calculus can be encoded
+-- via abstraction elimination into the SK calculus
+-- as binary trees whose leaves are one
+-- of the three symbols S ('ap') and K ('const').
+class Unabstractable sem where
+  -- | S
+  ap :: sem ((a -> b -> c) -> (a -> b) -> a -> c)
+  -- | K
   const :: sem (a -> b -> a)
-  flip :: sem ((a -> b -> c) -> b -> a -> c)
+  -- | I
   id :: sem (a -> a)
+  -- | B
   (.) :: sem ((b -> c) -> (a -> b) -> a -> c)
   infixr 9 .
+  -- | C
+  flip :: sem ((a -> b -> c) -> b -> a -> c)
   ($) :: sem ((a -> b) -> a -> b)
   infixr 0 $
+
+  ap = liftDerived ap
   const = liftDerived const
-  flip = liftDerived flip
   id = liftDerived id
   (.) = liftDerived (.)
+  flip = liftDerived flip
   ($) = liftDerived ($)
+
+  default ap ::
+    FromDerived Unabstractable sem =>
+    sem ((a -> b -> c) -> (a -> b) -> a -> c)
   default const ::
-    FromDerived Functionable sem =>
+    FromDerived Unabstractable sem =>
     sem (a -> b -> a)
-  default flip ::
-    FromDerived Functionable sem =>
-    sem ((a -> b -> c) -> b -> a -> c)
   default id ::
-    FromDerived Functionable sem =>
+    FromDerived Unabstractable sem =>
     sem (a -> a)
   default (.) ::
-    FromDerived Functionable sem =>
+    FromDerived Unabstractable sem =>
     sem ((b -> c) -> (a -> b) -> a -> c)
+  default flip ::
+    FromDerived Unabstractable sem =>
+    sem ((a -> b -> c) -> b -> a -> c)
   default ($) ::
-    FromDerived Functionable sem =>
+    FromDerived Unabstractable sem =>
     sem ((a -> b) -> a -> b)
 
 -- * Class 'Anythingable'
-- 
2.44.1