diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,4 +1,70 @@
 
+## symantic-base-0.5.0.20221211 (2022-12-10)
+
+### Interface
+
+* Add `Endpoint`.
+* Add syntax for `either`.
+* Add syntax `IfSemantic`.
+* Add interpreter `Reader`.
+* Fix export of `ADT`.
+* Fix gather in submodules.
+* Move `(.@)` into `Unabstractable`.
+* Remove syntax `Routable`.
+* Remove `option`, only `optional` is correct.
+* Replace `adt` by `dataType`, and support `TuplesOfFunctions`.
+
+### Documentation
+
+* Fix remaining `<:>` to `<.>`.
+* Fix typos in comments.
+* Update `ChangeLog.md`.
+* Update public presence.
+
+### Implementation
+
+* Fix deprecated `StarIsType`.
+* Gather in submodules.
+* Rename module `ADT` to `EithersOfTuples`.
+* Rename type variable `repr` to `sem`.
+
+### Build
+
+* Check that the build before tagging.
+* Ignore `.pre-commit-config.yaml`.
+* Improve `ghcid` support.
+* Improve `flake.nix`.
+* Update nix input `nixpkgs`.
+
+
+## symantic-base-0.5.0.20221122 (2022-11-23)
+
+### Interface
+
+* Add syntax for `either`.
+* Add syntax `IfSemantic`.
+* Add interpreter `Reader`.
+* Fix gather in submodules.
+* Move `(.@)` into `Unabstractable`.
+* Remove `option`, only `optional` is correct.
+
+### Documentation
+
+* Fix typos in comments.
+* Update public presence.
+
+### Implementation
+
+* Fix deprecated `StarIsType`.
+* Gather in submodules.
+* Rename type variable `repr` to `sem`.
+
+### Build
+
+* Improve `flake.nix`.
+* Update nix input `nixpkgs`.
+
+
 ## symantic-base-0.4.0.20211106 (2021-11-18)
 
 ### Interface
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -1,12 +1,12 @@
-override GHCID_OPTIONS += --no-height-limit --reverse-errors 
-override REPL_OPTIONS += -ignore-dot-ghci
-
 cabal := $(wildcard *.cabal)
 package := $(notdir ./$(cabal:.cabal=))
 version := $(shell sed -ne 's/^version: *\(.*\)/\1/p' $(cabal))
 project := $(patsubst %.cabal,%,$(cabal))
 cabal_builddir ?= dist-newstyle
 
+override REPL_OPTIONS += -ignore-dot-ghci
+override GHCID_OPTIONS += --no-height-limit --reverse-errors --color=always --warnings --restart $(cabal)
+
 all: build
 build:
 	cabal build $(CABAL_BUILD_FLAGS)
@@ -32,7 +32,7 @@
 	git tag -d $(package)-$(version)
 	git add '$@'
 	git commit -m 'doc: update `$@`'
-tag: ChangeLog.md
+tag: build ChangeLog.md
 	git tag -s -m $(package)-$(version) $(package)-$(version)
 
 tar:
diff --git a/flake.lock b/flake.lock
--- a/flake.lock
+++ b/flake.lock
@@ -1,21 +1,59 @@
 {
   "nodes": {
+    "flake-utils": {
+      "locked": {
+        "lastModified": 1667077288,
+        "narHash": "sha256-bdC8sFNDpT0HK74u9fUkpbf1MEzVYJ+ka7NXCdgBoaA=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "6ee9ebb6b1ee695d2cacc4faa053a7b9baa76817",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1640319671,
-        "narHash": "sha256-ZkKmakwaOaLiZOpIZWbeJZwap5CzJ30s4UJTfydYIYc=",
-        "path": "/nix/store/293cqgx8pcmkcn9mx5ln6i9nwvxv274r-source",
-        "rev": "eac07edbd20ed4908b98790ba299250b5527ecdf",
-        "type": "path"
+        "lastModified": 1667050928,
+        "narHash": "sha256-xOn0ZgjImIyeecEsrjxuvlW7IW5genTwvvnDQRFncB8=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "fdebb81f45a1ba2c4afca5fd9f526e1653ad0949",
+        "type": "github"
       },
       "original": {
         "id": "nixpkgs",
         "type": "indirect"
       }
     },
+    "pre-commit-hooks": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": [
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1667992213,
+        "narHash": "sha256-8Ens8ozllvlaFMCZBxg6S7oUyynYx2v7yleC5M0jJsE=",
+        "owner": "cachix",
+        "repo": "pre-commit-hooks.nix",
+        "rev": "ebcbfe09d2bd6d15f68de3a0ebb1e4dcb5cd324b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "cachix",
+        "repo": "pre-commit-hooks.nix",
+        "type": "github"
+      }
+    },
     "root": {
       "inputs": {
-        "nixpkgs": "nixpkgs"
+        "nixpkgs": "nixpkgs",
+        "pre-commit-hooks": "pre-commit-hooks"
       }
     }
   },
diff --git a/flake.nix b/flake.nix
--- a/flake.nix
+++ b/flake.nix
@@ -1,31 +1,55 @@
 {
-inputs.nixpkgs.url = "flake:nixpkgs";
-outputs = inputs: let
-  pkg = "symantic-base";
-  lib = inputs.nixpkgs.lib;
-  forAllSystems = f: lib.genAttrs lib.systems.supported.hydra (system: f rec {
-    inherit system;
-    pkgs = inputs.nixpkgs.legacyPackages.${system};
-    haskellPackages = pkgs.haskellPackages.extend (with pkgs.haskell.lib; hfinal: hsuper: {
-      ${pkg} = buildFromSdist (hfinal.callCabal2nix pkg ./. {});
-    });
-  });
-  in {
-    # nix -L build
-    defaultPackage = forAllSystems ({haskellPackages, ...}: haskellPackages.${pkg});
-    # nix -L develop
-    devShell = forAllSystems ({pkgs, haskellPackages, ...}:
-      haskellPackages.shellFor {
-        packages = ps: [ ps.${pkg} ];
-        nativeBuildInputs = [
-          haskellPackages.cabal-install
-          haskellPackages.ghcid
-          haskellPackages.haskell-language-server
-          haskellPackages.hlint
-          pkgs.git-chglog
-          pkgs.reuse
-        ];
-        withHoogle = false;
-      });
+  inputs = {
+    nixpkgs.url = "flake:nixpkgs";
+    pre-commit-hooks.url = "github:cachix/pre-commit-hooks.nix";
+    pre-commit-hooks.inputs.nixpkgs.follows = "nixpkgs";
   };
+  outputs = inputs:
+    let
+      pkg = "symantic-base";
+      lib = inputs.nixpkgs.lib;
+      forAllSystems = f: lib.genAttrs lib.systems.flakeExposed (system: f rec {
+        inherit system;
+        pkgs = inputs.nixpkgs.legacyPackages.${system};
+        haskellPackages = pkgs.haskellPackages.extend (with pkgs.haskell.lib; hfinal: hsuper: {
+          ${pkg} = buildFromSdist (hfinal.callCabal2nix pkg ./. { });
+        });
+      });
+    in
+    rec {
+      # nix -L build
+      defaultPackage = forAllSystems ({ haskellPackages, ... }: haskellPackages.${pkg});
+      # nix -L develop  or  direnv allow
+      devShell = forAllSystems ({ pkgs, haskellPackages, system, ... }:
+        haskellPackages.shellFor {
+          packages = ps: [ ps.${pkg} ];
+          nativeBuildInputs = [
+            haskellPackages.cabal-install
+            haskellPackages.ghcid
+            haskellPackages.haskell-language-server
+            haskellPackages.hlint
+            pkgs.git-chglog
+            pkgs.reuse
+          ];
+          withHoogle = false;
+          inherit (checks.${system}.pre-commit-check) shellHook;
+        });
+      # nix flake check
+      checks = forAllSystems (args: with args; {
+        pre-commit-check = inputs.pre-commit-hooks.lib.${system}.run {
+          src = ./.;
+          #settings.ormolu.cabalDefaultExtensions = true;
+          settings.ormolu.defaultExtensions = [
+            "ImportQualifiedPost"
+            "TypeApplications"
+          ];
+          hooks = {
+            hlint.enable = true;
+            nixpkgs-fmt.enable = true;
+            fourmolu.enable = true;
+            cabal-fmt.enable = true;
+          };
+        };
+      });
+    };
 }
diff --git a/src/Symantic.hs b/src/Symantic.hs
--- a/src/Symantic.hs
+++ b/src/Symantic.hs
@@ -1,19 +1,7 @@
-module Symantic
- ( module Symantic.Classes
- , module Symantic.CurryN
- , module Symantic.Data
- , module Symantic.Derive
- , module Symantic.Optimize
- , module Symantic.Reify
- , module Symantic.SharingObserver
- , module Symantic.Viewer
- ) where
+module Symantic (
+  module Symantic.Semantics,
+  module Symantic.Syntaxes,
+) where
 
-import Symantic.Classes
-import Symantic.CurryN
-import Symantic.Data
-import Symantic.Derive
-import Symantic.Optimize
-import Symantic.Reify
-import Symantic.SharingObserver
-import Symantic.Viewer
+import Symantic.Semantics
+import Symantic.Syntaxes
diff --git a/src/Symantic/ADT.hs b/src/Symantic/ADT.hs
deleted file mode 100644
--- a/src/Symantic/ADT.hs
+++ /dev/null
@@ -1,197 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE EmptyCase #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE UndecidableInstances #-}
--- | EOT (Either of Tuples) to/from ADT (Algebraic Data Type).
--- to produce or consume custom ADT with @('<:>')@ and @('<+>')@.
---
--- 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@.
-module Symantic.ADT where
-
-import Data.Either (Either(..))
-import Data.Void (Void, absurd)
-import Data.Function (($), (.), id, const)
-import GHC.Generics as Generics
-
--- * Type family 'EoT'
--- Return an 'Either' of 'Tuples' from the given 'ADT',
--- matching the nesting occuring when using @('<:>')@ and ('<+>')@
--- and their associativity and precedence,
--- with no parenthesis messing around.
-type family EoT (adt :: [[*]]) :: * where
-  -- This is 'absurd'
-  EoT '[] = Void
-  -- There Is No Alternative
-  EoT '[ ps ] = Tuples ps
-  -- The right associativity of @('<+>')@
-  -- puts leaves on 'Left' and nodes on 'Right'
-  EoT (ps ': ss) = Either (Tuples ps) (EoT ss)
-
--- * Type family 'Tuples'
--- | Return the type of 'snd'-nested 2-tuples
--- from the given list of types.
-type family Tuples (as :: [*]) :: (r :: *) where
-  Tuples '[] = ()
-  Tuples '[a] = a
-  Tuples (a ': rest) = (a, Tuples rest)
-
--- * Type 'ADT'
--- | Normalized type-level representation of an Algebraic Data Type.
-type ADT (adt :: *) = ListOfRepSums (Rep adt) '[]
-
--- ** Type family 'ListOfRepSums'
--- | Collect the alternatives in a continuation passing-style.
-type family ListOfRepSums (a :: * -> *) (ss :: [[*]]) :: [[*]]
-type instance ListOfRepSums (a:+:b)     ss = ListOfRepSums a (ListOfRepSums b ss)
--- | Meta-information for datatypes
-type instance ListOfRepSums (M1 D _c a) ss = ListOfRepSums a ss
--- | Meta-information for constructors
-type instance ListOfRepSums (M1 C _c a) ss = ListOfRepProducts a '[] ': ss
--- | Empty datatypes
-type instance ListOfRepSums V1          ss = ss
-
--- ** Type family 'ListOfRepProducts'
--- | Collect the records in a continuation passing-style.
-type family ListOfRepProducts (a :: * -> *) (ps :: [*]) :: [*]
-type instance ListOfRepProducts (a:*:b)     ps = ListOfRepProducts a (ListOfRepProducts b ps)
--- | Meta-information for record selectors
-type instance ListOfRepProducts (M1 S _c a) ps = TypeOfRepField a ': ps
--- | Constructor without fields
-type instance ListOfRepProducts U1          ps = ps
-
--- ** Type family 'TypeOfRepField'
-type family TypeOfRepField (a :: * -> *) :: *
-type instance TypeOfRepField (K1 _i a) = a
-
--- * Class 'RepOfEoT'
-type RepOfEoT a = RepOfEithers (Rep a) '[]
-
--- | Morph the 'Either' of 'Tuples' corresponding to an 'ADT'
--- into a constructor of this 'ADT'.
--- This is the reverse of 'eotOfadt'.
-adtOfeot :: Generic a => RepOfEoT a => EoT (ADT a) -> a
-adtOfeot eot = Generics.to $ repOfEithers @_ @'[] eot id absurd
-
--- ** Class 'RepOfEithers'
-class RepOfEithers (a :: * -> *) ss where
-  -- | Parse the 'Either' (list-like) binary tree of 'EoT'
-  -- into the @(':+:')@ (balanced) binary tree of 'Rep',
-  -- using continuation passing-style for performance.
-  repOfEithers ::
-    EoT (ListOfRepSums a ss) ->
-    -- the 'a' 'Rep' is the current alternative in the 'EoT'
-    (a x -> r) ->
-    -- the 'a' 'Rep' is a following alternative in the 'EoT'
-    (EoT ss -> r) ->
-    r
-instance (RepOfEithers a (ListOfRepSums b ss), RepOfEithers b ss) => RepOfEithers (a:+:b) ss where
-  repOfEithers eot ok ko =
-    -- try to parse 'a' on the current 'eot'
-    repOfEithers @a @(ListOfRepSums b ss) eot
-     (ok . L1)
-     (\next ->
-      -- parsing 'a' failed
-      -- try to parse 'b' on the 'Right' of the current 'eot'
-      repOfEithers @b @ss next
-       (ok . R1)
-       ko -- parsing 'b' failed: backtrack
-     )
-instance RepOfEithers a ss => RepOfEithers (M1 D c a) ss where
-  repOfEithers eot ok = repOfEithers @a @ss eot (ok . M1)
-instance RepOfTuples a '[] => RepOfEithers (M1 C c a) (ps ': ss) where
-  repOfEithers eot ok ko =
-    case eot of
-      -- 'EoT' is a leaf, and 'Rep' too: parsing succeeds
-      Left ts -> ok $ M1 $ repOfTuples @a @'[] ts const
-      -- 'EoT' is a node, but 'Rep' is a leaf: parsing fails
-      Right ss -> ko ss
-instance RepOfTuples a '[] => RepOfEithers (M1 C c a) '[] where
-  repOfEithers eot ok _ko = ok $ M1 $ repOfTuples @_ @'[] eot const
-instance RepOfEithers V1 ss where
-  repOfEithers eot _ok ko = ko eot
-
--- ** Class 'RepOfTuples'
-class RepOfTuples (a :: * -> *) (xs::[*]) where
-  -- | Parse the 'Tuples' (list-like) binary tree of 'EoT'
-  -- into the @(':*:')@ (balanced) binary tree of 'Rep',
-  -- using continuation passing-style for performance.
-  repOfTuples ::
-    Tuples (ListOfRepProducts a xs) ->
-    (a x -> Tuples xs -> r) -> r
-instance (RepOfTuples a (ListOfRepProducts b ps), RepOfTuples b ps) => RepOfTuples (a:*:b) ps where
-  repOfTuples ts k =
-    -- uncons 'a'
-    repOfTuples @a @(ListOfRepProducts b ps) ts
-     (\a ts' ->
-      -- uncons 'b'
-      repOfTuples @b @ps ts'
-        (\b -> k (a:*:b)))
-instance RepOfField a => RepOfTuples (M1 S c a) (p ': ps) where
-  repOfTuples (a, ts) k = k (M1 (repOfField a)) ts
-instance RepOfField a => RepOfTuples (M1 S c a) '[] where
-  repOfTuples a k = k (M1 (repOfField a)) ()
-instance RepOfTuples U1 ps where
-  repOfTuples ts k = k U1 ts
-
--- ** Class 'RepOfField'
-class RepOfField (a :: * -> *) where
-  repOfField :: TypeOfRepField a -> a x
-instance RepOfField (K1 i a) where
-  repOfField = K1
-
--- * Class 'EoTOfRep'
-type EoTOfRep a = EithersOfRep (Rep a) '[]
-
--- | Morph the constructor of an 'ADT'
--- into the corresponding 'Either' of 'Tuples' of this 'ADT'.
--- This is the reverse of 'adtOfeot'.
-eotOfadt :: Generic a => EoTOfRep a => a -> EoT (ADT a)
-eotOfadt = eithersOfRepL @_ @'[] . Generics.from
-
--- ** Class 'EithersOfRep'
-class EithersOfRep (a :: * -> *) ss where
-  eithersOfRepL :: a x    -> EoT (ListOfRepSums a ss)
-  eithersOfRepR :: EoT ss -> EoT (ListOfRepSums a ss)
-instance (EithersOfRep a (ListOfRepSums b ss), EithersOfRep b ss) =>
- EithersOfRep (a:+:b) ss where
-  eithersOfRepL = \case
-    L1 a -> eithersOfRepL @a @(ListOfRepSums b ss) a
-    R1 b -> eithersOfRepR @a @(ListOfRepSums b ss) (eithersOfRepL @b @ss b)
-  eithersOfRepR ss = eithersOfRepR @a @(ListOfRepSums b ss) (eithersOfRepR @b @ss ss)
-instance EithersOfRep a ss => EithersOfRep (M1 D c a) ss where
-  eithersOfRepL (M1 a) = eithersOfRepL @a @ss a
-  eithersOfRepR = eithersOfRepR @a @ss
-instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) '[] where
-  eithersOfRepL (M1 a) = tuplesOfRep @_ @'[] a ()
-  eithersOfRepR = absurd
-instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) (ps ': ss) where
-  eithersOfRepL (M1 a) = Left $ tuplesOfRep @_ @'[] a ()
-  eithersOfRepR = Right
-instance EithersOfRep V1 ss where
-  eithersOfRepL = \case {}
-  eithersOfRepR = id
-
--- ** Class 'TuplesOfRep'
-class TuplesOfRep (a :: * -> *) (ps::[*]) where
-  tuplesOfRep :: a x -> Tuples ps -> Tuples (ListOfRepProducts a ps)
-instance (TuplesOfRep a (ListOfRepProducts b ps), TuplesOfRep b ps) => TuplesOfRep (a:*:b) ps where
-  tuplesOfRep (a:*:b) ps =
-    tuplesOfRep @a @(ListOfRepProducts b ps) a
-     (tuplesOfRep @b @ps b ps)
-instance TuplesOfRep U1 ps where
-  tuplesOfRep U1 xs = xs
-instance FieldOfRep a => TuplesOfRep (M1 S c a) (x ': ps) where
-  tuplesOfRep (M1 a) xs = (fieldOfRep a, xs)
-instance FieldOfRep a => TuplesOfRep (M1 S c a) '[] where
-  tuplesOfRep (M1 a) _xs = fieldOfRep a
-
--- ** Class 'FieldOfRep'
-class FieldOfRep (a :: * -> *) where
-  fieldOfRep :: a x -> TypeOfRepField a
-instance FieldOfRep (K1 i a) where
-  fieldOfRep (K1 a) = a
diff --git a/src/Symantic/Classes.hs b/src/Symantic/Classes.hs
deleted file mode 100644
--- a/src/Symantic/Classes.hs
+++ /dev/null
@@ -1,440 +0,0 @@
-{-# LANGUAGE DataKinds #-} -- For ReprKind
-{-# LANGUAGE PatternSynonyms #-} -- For (:!:)
-{-# LANGUAGE TypeFamilyDependencies #-} -- For Permutation
-{-# LANGUAGE UndecidableInstances #-} -- For Permutation
--- | Comibnators in this module conflict with usual ones from the @Prelude@
--- hence they are meant to be imported either explicitely or qualified.
-module Symantic.Classes where
-
-import Data.Bool (Bool(..))
-import Data.Char (Char)
-import Data.Either (Either(..))
-import Data.Eq (Eq)
-import Data.Int (Int)
-import Data.Kind (Type)
-import Data.Maybe (Maybe(..), fromJust)
-import Data.Proxy (Proxy(..))
-import Data.Semigroup (Semigroup)
-import Data.String (String)
-import GHC.Generics (Generic)
-import Numeric.Natural (Natural)
-import qualified Control.Category as Cat
-import qualified Data.Function as Fun
-import qualified Data.Tuple as Tuple
-
-import Symantic.Derive
-import Symantic.ADT
-import Symantic.CurryN
-
--- * Type 'ReprKind'
--- | The kind of @repr@(esentations) throughout this library.
-type ReprKind = Type -> Type
-
--- * Class 'Abstractable'
-class Abstractable repr where
-  -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
-  lam :: (repr a -> repr b) -> repr (a->b)
-  -- | Like 'lam' but whose argument must be used only once,
-  -- hence safe to beta-reduce (inline) without duplicating work.
-  lam1 :: (repr a -> repr b) -> repr (a->b)
-  var :: repr a -> repr a
-  -- | Application, aka. unabstract.
-  (.@) :: repr (a->b) -> repr a -> repr b; infixl 9 .@
-  lam f = liftDerived (lam (derive Fun.. f Fun.. liftDerived))
-  lam1 f = liftDerived (lam1 (derive Fun.. f Fun.. liftDerived))
-  var = liftDerived1 var
-  (.@) = liftDerived2 (.@)
-  default lam ::
-    FromDerived Abstractable repr => Derivable repr =>
-    (repr a -> repr b) -> repr (a->b)
-  default lam1 ::
-    FromDerived Abstractable repr => Derivable repr =>
-    (repr a -> repr b) -> repr (a->b)
-  default var ::
-    FromDerived1 Abstractable repr =>
-    repr a -> repr a
-  default (.@) ::
-    FromDerived2 Abstractable repr =>
-    repr (a->b) -> repr a -> repr b
-
--- ** Class 'Functionable'
-class Functionable repr where
-  const :: repr (a -> b -> a)
-  flip :: repr ((a -> b -> c) -> b -> a -> c)
-  id :: repr (a->a)
-  (.) :: repr ((b->c) -> (a->b) -> a -> c); infixr 9 .
-  ($) :: repr ((a->b) -> a -> b); infixr 0 $
-  const = liftDerived const
-  flip = liftDerived flip
-  id = liftDerived id
-  (.) = liftDerived (.)
-  ($) = liftDerived ($)
-  default const ::
-    FromDerived Functionable repr =>
-    repr (a -> b -> a)
-  default flip ::
-    FromDerived Functionable repr =>
-    repr ((a -> b -> c) -> b -> a -> c)
-  default id ::
-    FromDerived Functionable repr =>
-    repr (a->a)
-  default (.) ::
-    FromDerived Functionable repr =>
-    repr ((b->c) -> (a->b) -> a -> c)
-  default ($) ::
-    FromDerived Functionable repr =>
-    repr ((a->b) -> a -> b)
-
--- * Class 'Anythingable'
-class Anythingable repr where
-  anything :: repr a -> repr a
-  anything = Fun.id
-
--- * Class 'Bottomable'
-class Bottomable repr where
-  bottom :: repr a
-
--- * Class 'Constantable'
-class Constantable c repr where
-  constant :: c -> repr c
-  constant = liftDerived Fun.. constant
-  default constant ::
-    FromDerived (Constantable c) repr =>
-    c -> repr c
-
--- * Class 'Eitherable'
-class Eitherable repr where
-  left :: repr (l -> Either l r)
-  right :: repr (r -> Either l r)
-  left = liftDerived left
-  right = liftDerived right
-  default left ::
-    FromDerived Eitherable repr =>
-    repr (l -> Either l r)
-  default right ::
-    FromDerived Eitherable repr =>
-    repr (r -> Either l r)
-
--- * Class 'Equalable'
-class Equalable repr where
-  equal :: Eq a => repr (a -> a -> Bool)
-  equal = liftDerived equal
-  default equal ::
-    FromDerived Equalable repr =>
-    Eq a => repr (a -> a -> Bool)
-
-infix 4 `equal`, ==
-(==) ::
-  Abstractable repr => Equalable repr => Eq a =>
-  repr a -> repr a -> repr Bool
-(==) x y = equal .@ x .@ y
-
--- * Class 'IfThenElseable'
-class IfThenElseable repr where
-  ifThenElse :: repr Bool -> repr a -> repr a -> repr a
-  ifThenElse = liftDerived3 ifThenElse
-  default ifThenElse ::
-    FromDerived3 IfThenElseable repr =>
-    repr Bool -> repr a -> repr a -> repr a
-
--- * Class 'Inferable'
-class Inferable a repr where
-  infer :: repr a
-  default infer :: FromDerived (Inferable a) repr => repr a
-  infer = liftDerived infer
-
-unit :: Inferable () repr => repr ()
-unit = infer
-bool :: Inferable Bool repr => repr Bool
-bool = infer
-char :: Inferable Char repr => repr Char
-char = infer
-int :: Inferable Int repr => repr Int
-int = infer
-natural :: Inferable Natural repr => repr Natural
-natural = infer
-string :: Inferable String repr => repr String
-string = infer
-
--- * Class 'Listable'
-class Listable repr where
-  cons :: repr (a -> [a] -> [a])
-  nil :: repr [a]
-  cons = liftDerived cons
-  nil = liftDerived nil
-  default cons ::
-    FromDerived Listable repr =>
-    repr (a -> [a] -> [a])
-  default nil ::
-    FromDerived Listable repr =>
-    repr [a]
-
--- * Class 'Maybeable'
-class Maybeable repr where
-  nothing :: repr (Maybe a)
-  just :: repr (a -> Maybe a)
-  nothing = liftDerived nothing
-  just = liftDerived just
-  default nothing ::
-    FromDerived Maybeable repr =>
-    repr (Maybe a)
-  default just ::
-    FromDerived Maybeable repr =>
-    repr (a -> Maybe a)
-
--- * Class 'IsoFunctor'
-class IsoFunctor repr where
-  (<%>) :: Iso a b -> repr a -> repr b; infixl 4 <%>
-  (<%>) iso = liftDerived1 (iso <%>)
-  default (<%>) ::
-    FromDerived1 IsoFunctor repr =>
-    Iso a b -> repr a -> repr b
-
--- ** Type 'Iso'
-data Iso a b = Iso { a2b :: a->b, b2a :: b->a }
-instance Cat.Category Iso where
-  id = Iso Cat.id Cat.id
-  f . g = Iso (a2b f Cat.. a2b g) (b2a g Cat.. b2a f)
-
--- * Class 'ProductFunctor'
--- | Beware that this is an @infixr@,
--- not @infixl@ like 'Control.Applicative.<*>';
--- this is to follow what is expected by 'ADT'.
-class ProductFunctor repr where
-  (<.>) :: repr a -> repr b -> repr (a, b); infixr 4 <.>
-  (<.>) = liftDerived2 (<.>)
-  default (<.>) ::
-    FromDerived2 ProductFunctor repr =>
-    repr a -> repr b -> repr (a, b)
-  (<.) :: repr a -> repr () -> repr a; infixr 4 <.
-  ra <. rb = Iso Tuple.fst (, ()) <%> (ra <.> rb)
-  default (<.) :: IsoFunctor repr => repr a -> repr () -> repr a
-  (.>) :: repr () -> repr a -> repr a; infixr 4 .>
-  ra .> rb = Iso Tuple.snd (() ,) <%> (ra <.> rb)
-  default (.>) :: IsoFunctor repr => repr () -> repr a -> repr a
-
--- * Class 'SumFunctor'
--- | Beware that this is an @infixr@,
--- not @infixl@ like 'Control.Applicative.<|>';
--- this is to follow what is expected by 'ADT'.
-class SumFunctor repr where
-  (<+>) :: repr a -> repr b -> repr (Either a b); infixr 3 <+>
-  (<+>) = liftDerived2 (<+>)
-  default (<+>) ::
-    FromDerived2 SumFunctor repr =>
-    repr a -> repr b -> repr (Either a b)
-
--- * Class 'AlternativeFunctor'
--- | Beware that this is an @infixr@,
--- not @infixl@ like 'Control.Applicative.<|>';
--- this is to follow what is expected by 'ADT'.
-class AlternativeFunctor repr where
-  (<|>) :: repr a -> repr a -> repr a; infixr 3 <|>
-  (<|>) = liftDerived2 (<|>)
-  default (<|>) ::
-    FromDerived2 AlternativeFunctor repr =>
-    repr a -> repr a -> repr a
-
--- * Class 'Dicurryable'
-class Dicurryable repr where
-  dicurry ::
-    CurryN args =>
-    proxy args ->
-    (args-..->a) -> -- construction
-    (a->Tuples args) -> -- destruction
-    repr (Tuples args) ->
-    repr a
-  dicurry args constr destr = liftDerived1 (dicurry args constr destr)
-  default dicurry ::
-    FromDerived1 Dicurryable repr =>
-    CurryN args =>
-    proxy args ->
-    (args-..->a) ->
-    (a->Tuples args) ->
-    repr (Tuples args) ->
-    repr a
-
-construct ::
-  forall args a repr.
-  Dicurryable repr =>
-  Generic a =>
-  EoTOfRep a =>
-  CurryN args =>
-  Tuples args ~ EoT (ADT a) =>
-  (args ~ Args (args-..->a)) =>
-  (args-..->a) ->
-  repr (Tuples args) ->
-  repr a
-construct f = dicurry (Proxy::Proxy args) f eotOfadt
-
-adt ::
-  forall adt repr.
-  IsoFunctor repr =>
-  Generic adt =>
-  RepOfEoT adt =>
-  EoTOfRep adt =>
-  repr (EoT (ADT adt)) ->
-  repr adt
-adt = (<%>) (Iso adtOfeot eotOfadt)
-
--- * Class 'Monoidable'
-class
-  ( Emptyable repr
-  , Semigroupable repr
-  ) => Monoidable repr
-instance
-  ( Emptyable repr
-  , Semigroupable repr
-  ) => Monoidable repr
-
--- ** Class 'Emptyable'
-class Emptyable repr where
-  empty :: repr a
-  empty = liftDerived empty
-  default empty ::
-    FromDerived Emptyable repr =>
-    repr a
-
--- ** Class 'Semigroupable'
-class Semigroupable repr where
-  concat :: Semigroup a => repr (a -> a -> a)
-  concat = liftDerived concat
-  default concat ::
-    FromDerived Semigroupable repr =>
-    Semigroup a =>
-    repr (a -> a -> a)
-
-infixr 6 `concat`, <>
-(<>) ::
-  Abstractable repr => Semigroupable repr => Semigroup a =>
-  repr a -> repr a -> repr a
-(<>) x y = concat .@ x .@ y
-
--- ** Class 'Optionable'
-class Optionable repr where
-  option :: repr a -> repr a
-  optional :: repr a -> repr (Maybe a)
-  option = liftDerived1 option
-  optional = liftDerived1 optional
-  default option ::
-    FromDerived1 Optionable repr =>
-    repr a -> repr a
-  default optional ::
-    FromDerived1 Optionable repr =>
-    repr a -> repr (Maybe a)
-
--- * Class 'Repeatable'
-class Repeatable repr where
-  many0 :: repr a -> repr [a]
-  many1 :: repr a -> repr [a]
-  many0 = liftDerived1 many0
-  many1 = liftDerived1 many1
-  default many0 ::
-    FromDerived1 Repeatable repr =>
-    repr a -> repr [a]
-  default many1 ::
-    FromDerived1 Repeatable repr =>
-    repr a -> repr [a]
-
--- | Alias to 'many0'.
-many :: Repeatable repr => repr a -> repr [a]
-many = many0
-
--- | Alias to 'many1'.
-some :: Repeatable repr => repr a -> repr [a]
-some = many1
-
--- * Class 'Permutable'
-class Permutable repr where
-  -- Use @TypeFamilyDependencies@ to help type-inference infer @(repr)@.
-  type Permutation (repr:: ReprKind) = (r :: ReprKind) | r -> repr
-  type Permutation repr = Permutation (Derived repr)
-  permutable :: Permutation repr a -> repr a
-  perm :: repr a -> Permutation repr a
-  noPerm :: Permutation repr ()
-  permWithDefault :: a -> repr a -> Permutation repr a
-  optionalPerm ::
-    Eitherable repr => IsoFunctor repr => Permutable repr =>
-    repr a -> Permutation repr (Maybe a)
-  optionalPerm = permWithDefault Nothing Fun.. (<%>) (Iso Just fromJust)
-
-(<&>) ::
-  Permutable repr =>
-  ProductFunctor (Permutation repr) =>
-  repr a ->
-  Permutation repr b ->
-  Permutation repr (a, b)
-x <&> y = perm x <.> y
-infixr 4 <&>
-{-# INLINE (<&>)  #-}
-
-(<?&>) ::
-  Eitherable repr =>
-  IsoFunctor repr =>
-  Permutable repr =>
-  ProductFunctor (Permutation repr) =>
-  repr a ->
-  Permutation repr b ->
-  Permutation repr (Maybe a, b)
-x <?&> y = optionalPerm x <.> y
-infixr 4 <?&>
-{-# INLINE (<?&>) #-}
-
-(<*&>) ::
-  Eitherable repr =>
-  Repeatable repr =>
-  IsoFunctor repr =>
-  Permutable repr =>
-  ProductFunctor (Permutation repr) =>
-  repr a ->
-  Permutation repr b ->
-  Permutation repr ([a],b)
-x <*&> y = permWithDefault [] (many1 x) <.> y
-infixr 4 <*&>
-{-# INLINE (<*&>) #-}
-
-(<+&>) ::
-  Eitherable repr =>
-  Repeatable repr =>
-  IsoFunctor repr =>
-  Permutable repr =>
-  ProductFunctor (Permutation repr) =>
-  repr a ->
-  Permutation repr b ->
-  Permutation repr ([a], b)
-x <+&> y = perm (many1 x) <.> y
-infixr 4 <+&>
-{-# INLINE (<+&>) #-}
-
--- * Class 'Routable'
-class Routable repr where
-  (<!>) :: repr a -> repr b -> repr (a, b); infixr 4 <!>
-  (<!>) = liftDerived2 (<!>)
-  default (<!>) ::
-    FromDerived2 Routable repr =>
-    repr a -> repr b -> repr (a, b)
-
--- | Like @(,)@ but @infixr@.
--- Mostly useful for clarity when using 'Routable'.
-pattern (:!:) :: a -> b -> (a, b)
-pattern a:!:b <- (a, b)
-  where a:!:b = (a, b)
-infixr 4 :!:
-
--- * Class 'Voidable'
-class Voidable repr where
-  -- | Useful to supply @(a)@ to a @(repr)@ consuming @(a)@,
-  -- for example in the format of a printing interpreter.
-  void :: a -> repr a -> repr ()
-  void = liftDerived1 Fun.. void
-  default void ::
-    FromDerived1 Voidable repr =>
-    a -> repr a -> repr ()
-
--- * Class 'Substractable'
-class Substractable repr where
-  (<->) :: repr a -> repr b -> repr a; infixr 3 <->
-  (<->) = liftDerived2 (<->)
-  default (<->) ::
-    FromDerived2 Substractable repr =>
-    repr a -> repr b -> repr a
diff --git a/src/Symantic/CurryN.hs b/src/Symantic/CurryN.hs
deleted file mode 100644
--- a/src/Symantic/CurryN.hs
+++ /dev/null
@@ -1,40 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DataKinds #-}
-module Symantic.CurryN where
-
-import Data.Function (($), (.))
-
-import Symantic.ADT (Tuples)
-
--- * Class 'CurryN'
--- | Produce and consume 'Tuples'.
--- Not actually useful for the Generic side of this module,
--- but related through the use of 'Tuples'.
-class CurryN args where
-  -- Like 'curry' but for an arbitrary number of nested 2-tuples.
-  curryN :: (Tuples args -> res) -> args-..->res
-  -- Like 'uncurry' but for an arbitrary number of nested 2-tuples.
-  uncurryN :: (args-..->res) -> Tuples args -> res
-  -- Like 'fmap' on @('->')@ but for an arbitrary number of arguments.
-  mapresultN :: (a->b) -> (args-..->a) -> args-..->b
-instance CurryN '[a] where
-  curryN = ($)
-  uncurryN = ($)
-  mapresultN = (.)
-instance CurryN (b ': as) => CurryN (a ': b ': as) where
-  curryN f x = curryN @(b ': as) (\xs -> f (x, xs))
-  uncurryN f (x, xs) = uncurryN @(b ': as) (f x) xs
-  mapresultN f as2r = mapresultN @(b ': as) f . as2r
-
--- ** Type family ('-..->')
-type family (args :: [*]) -..-> (r :: *) :: * where
-  '[]        -..-> r = r
-  (a : args) -..-> r = a -> args -..-> r
--- ** Type family 'Args'
-type family Args (f :: *) :: [*] where
-  Args (a -> r) = a : Args r
-  Args r = '[]
--- ** Type family 'Result'
-type family Result (as :: *) :: * where
-  Result (a -> r) = Result r
-  Result r = r
diff --git a/src/Symantic/Data.hs b/src/Symantic/Data.hs
deleted file mode 100644
--- a/src/Symantic/Data.hs
+++ /dev/null
@@ -1,231 +0,0 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-} -- For ReprKind
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ViewPatterns #-}
-module Symantic.Data where
-
-import Data.Bool (Bool)
-import Data.Either (Either)
-import Data.Kind (Constraint)
-import Data.Maybe (Maybe)
-import Data.Semigroup (Semigroup)
-import Type.Reflection (Typeable, (:~~:)(..), eqTypeRep, typeRep)
-import qualified Data.Eq as Eq
-import qualified Data.Function as Fun
-import qualified Data.Maybe as Maybe
-
-import Symantic.Classes
-import Symantic.Derive
-
--- * Type 'SomeData'
-data SomeData repr a =
-  forall able.
-  ( Derivable (Data able repr)
-  , Typeable able
-  ) => SomeData (Data able repr a)
-
-type instance Derived (SomeData repr) = repr
-instance Derivable (SomeData repr) where
-  derive (SomeData x) = derive x
-
--- ** Type 'Data'
--- TODO: neither data families nor data instances
--- can have phantom roles with GHC-9's RoleAnnotations,
--- 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 :: ReprKind -> Constraint)
-  :: ReprKind -> ReprKind
-type instance Derived (Data able repr) = repr
-
--- | Convenient utility to pattern-match a 'SomeData'.
-pattern Data :: Typeable able => Data able repr a -> SomeData repr a
-pattern Data x <- (unSomeData -> Maybe.Just x)
-
--- | @(unSomeData c :: 'Maybe' ('Data' able repr a))@
--- extract the data-constructor from the given 'SomeData'
--- iif. it belongs to the @('Data' able repr a)@ data-instance.
-unSomeData ::
-  forall able repr a.
-  Typeable able =>
-  SomeData repr a -> Maybe (Data able repr a)
-unSomeData (SomeData (c::Data c repr a)) =
-  case typeRep @able `eqTypeRep` typeRep @c of
-    Maybe.Just HRefl -> Maybe.Just c
-    Maybe.Nothing -> Maybe.Nothing
-
--- Abstractable
-data instance Data Abstractable repr a where
-  (:@) :: SomeData repr (a->b) -> SomeData repr a -> Data Abstractable repr b
-  Lam :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
-  Lam1 :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
-  Var :: repr a -> Data Abstractable repr a
-  -- FIXME: add constructors
-instance
-  ( Abstractable repr
-  ) => Derivable (Data Abstractable repr) where
-  derive = \case
-    f :@ x -> derive f .@ derive x
-    Lam f -> lam (\x -> derive (f (SomeData (Var x))))
-    Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x))))
-    Var x -> var x
-instance
-  ( Abstractable repr
-  ) => Abstractable (SomeData repr) where
-  f .@ x = SomeData (f :@ x)
-  lam f = SomeData (Lam f)
-  lam1 f = SomeData (Lam1 f)
-  var = Fun.id
-
--- Functionable
-instance
-  ( Abstractable repr
-  ) => Functionable (SomeData repr) 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)
-
--- Anythingable
-data instance Data Anythingable repr a where
-  Anything :: repr a -> Data Anythingable repr a
-instance
-  ( Anythingable repr
-  ) => Derivable (Data Anythingable repr) where
-  derive = \case
-    Anything x -> anything x
-instance Anythingable (SomeData repr)
-instance Anythingable (Data Anythingable repr)
-
--- Bottomable
-data instance Data Bottomable repr a where
-  Bottom :: Data Bottomable repr a
-instance Bottomable repr => Derivable (Data Bottomable repr) where
-  derive Bottom{} = bottom
-
--- Constantable
-data instance Data (Constantable c) repr a where
-  Constant :: {-Typeable c =>-} c -> Data (Constantable c) repr c
-instance Constantable c repr => Derivable (Data (Constantable c) repr) where
-  derive = \case
-    Constant x -> constant x
-instance
-  ( Constantable c repr
-  , Typeable c
-  ) => Constantable c (SomeData repr) where
-  constant c = SomeData (Constant c)
-instance {-Typeable c =>-} Constantable c (Data (Constantable c) repr) where
-  constant = Constant
-
--- Eitherable
-data instance Data Eitherable repr a where
-  Left :: Data Eitherable repr (l -> Either l r)
-  Right :: Data Eitherable repr (r -> Either l r)
-instance Eitherable repr => Derivable (Data Eitherable repr) where
-  derive = \case
-    Left -> left
-    Right -> right
-instance
-  ( Eitherable repr
-  ) => Eitherable (SomeData repr) where
-  left = SomeData Left
-  right = SomeData Right
-instance Eitherable (Data Eitherable repr) where
-  left = Left
-  right = Right
-
--- Equalable
-data instance Data Equalable repr a where
-  Equal :: Eq.Eq a => Data Equalable repr (a -> a -> Bool)
-instance Equalable repr => Derivable (Data Equalable repr) where
-  derive = \case
-    Equal -> equal
-instance
-  ( Equalable repr
-  ) => Equalable (SomeData repr) where
-  equal = SomeData Equal
-instance Equalable (Data Equalable repr) where
-  equal = Equal
-
--- Emptyable
-data instance Data Emptyable repr a where
-  Empty :: Data Emptyable repr a
-instance Emptyable repr => Derivable (Data Emptyable repr) where
-  derive = \case
-    Empty -> empty
-instance
-  ( Emptyable repr
-  ) => Emptyable (SomeData repr) where
-  empty = SomeData Empty
-instance Emptyable (Data Emptyable repr) where
-  empty = Empty
-
--- Semigroupable
-data instance Data Semigroupable repr a where
-  Concat :: Semigroup a => Data Semigroupable repr (a -> a -> a)
-infixr 4 `Concat`
-instance Semigroupable repr => Derivable (Data Semigroupable repr) where
-  derive = \case
-    Concat -> concat
-instance
-  ( Semigroupable repr
-  ) => Semigroupable (SomeData repr) where
-  concat = SomeData Concat
-instance Semigroupable (Data Semigroupable repr) where
-  concat = Concat
-
--- IfThenElseable
-data instance Data IfThenElseable repr a where
-  IfThenElse ::
-    SomeData repr Bool ->
-    SomeData repr a ->
-    SomeData repr a ->
-    Data IfThenElseable repr a
-instance IfThenElseable repr => Derivable (Data IfThenElseable repr) where
-  derive = \case
-    IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
-instance
-  ( IfThenElseable repr
-  ) => IfThenElseable (SomeData repr) where
-  ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
-instance IfThenElseable repr => IfThenElseable (Data IfThenElseable repr) where
-  ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
-
--- Listable
-data instance Data Listable repr a where
-  Cons :: Data Listable repr (a -> [a] -> [a])
-  Nil :: Data Listable repr [a]
-infixr 4 `Cons`
-instance Listable repr => Derivable (Data Listable repr) where
-  derive = \case
-    Cons -> cons
-    Nil -> nil
-instance
-  ( Listable repr
-  ) => Listable (SomeData repr) where
-  cons = SomeData Cons
-  nil = SomeData Nil
-instance Listable (Data Listable repr) where
-  cons = Cons
-  nil = Nil
-
--- Maybeable
-data instance Data Maybeable repr a where
-  Nothing :: Data Maybeable repr (Maybe a)
-  Just :: Data Maybeable repr (a -> Maybe a)
-instance Maybeable repr => Derivable (Data Maybeable repr) where
-  derive = \case
-    Nothing -> nothing
-    Just -> just
-instance
-  ( Maybeable repr
-  ) => Maybeable (SomeData repr) where
-  nothing = SomeData Nothing
-  just = SomeData Just
-instance Maybeable (Data Maybeable repr) where
-  nothing = Nothing
-  just = Just
diff --git a/src/Symantic/Derive.hs b/src/Symantic/Derive.hs
deleted file mode 100644
--- a/src/Symantic/Derive.hs
+++ /dev/null
@@ -1,90 +0,0 @@
-{-# LANGUAGE ConstraintKinds #-} -- For type class synonyms
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE DefaultSignatures #-} -- For adding LiftDerived* constraints
-module Symantic.Derive where
-
-import Data.Function ((.))
-import Data.Kind (Type)
-
--- * Type family 'Derived'
--- | The representation that @(repr)@ derives to.
-type family Derived (repr :: Type -> Type) :: Type -> Type
-
--- * Class 'Derivable'
--- | Derive an interpreter to another interpreter
--- determined by the 'Derived' open type family.
--- This is mostly useful when running the interpreter stack,
--- but also when going back from an initial encoding to a final one.
---
--- Note that 'derive' and 'liftDerived' are not necessarily reciprocical functions.
-class Derivable repr where
-  derive :: repr a -> Derived repr a
-
--- * Class 'LiftDerived'
--- | Lift the 'Derived' interpreter of an interpreter, to that interpreter.
--- This is mostly useful to give default values to class methods
--- in order to skip their definition for interpreters
--- where 'liftDerived' can already apply the right semantic.
---
--- Note that 'derive' and 'liftDerived' are not necessarily reciprocical functions.
-class LiftDerived repr where
-  liftDerived :: Derived repr a -> repr a
-
--- * Class 'LiftDerived1'
--- | Convenient wrapper of 'derive' and 'liftDerived' for functions with a single argument.
-class LiftDerived1 repr where
-  liftDerived1 ::
-    (Derived repr a -> Derived repr b) ->
-    repr a -> repr b
-  liftDerived1 f = liftDerived . f . derive
-  default liftDerived1 ::
-    LiftDerived repr => Derivable repr =>
-    (Derived repr a -> Derived repr b) ->
-    repr a -> repr b
-
--- * Class 'LiftDerived2'
--- | Convenient wrapper of 'derive' and 'liftDerived' for functions with two arguments.
--- Note that the default instance relies upon 'LiftDerived', not 'LiftDerived1'.
-class LiftDerived2 repr where
-  liftDerived2 ::
-    (Derived repr a -> Derived repr b -> Derived repr c) ->
-    repr a -> repr b -> repr c
-  liftDerived2 f a b = liftDerived (f (derive a) (derive b))
-  default liftDerived2 ::
-    LiftDerived repr => Derivable repr =>
-    (Derived repr a -> Derived repr b -> Derived repr c) ->
-    repr a -> repr b -> repr c
-
--- * Class 'LiftDerived3'
--- | Convenient wrapper of 'derive' and 'liftDerived' for functions with three arguments.
--- Note that the default instance relies upon 'LiftDerived', not 'LiftDerived2'.
-class LiftDerived3 repr where
-  liftDerived3 ::
-    (Derived repr a -> Derived repr b -> Derived repr c -> Derived repr d) ->
-    repr a -> repr b -> repr c -> repr d
-  liftDerived3 f a b c = liftDerived (f (derive a) (derive b) (derive c))
-  default liftDerived3 ::
-    LiftDerived repr => Derivable repr =>
-    (Derived repr a -> Derived repr b -> Derived repr c -> Derived repr d) ->
-    repr a -> repr b -> repr c -> repr d
-
--- * Class 'LiftDerived4'
--- | Convenient wrapper of 'derive' and 'liftDerived' for functions with three arguments.
--- Note that the default instance relies upon 'LiftDerived', not 'LiftDerived3'.
-class LiftDerived4 repr where
-  liftDerived4 ::
-    (Derived repr a -> Derived repr b -> Derived repr c -> Derived repr d -> Derived repr e) ->
-    repr a -> repr b -> repr c -> repr d -> repr e
-  liftDerived4 f a b c d = liftDerived (f (derive a) (derive b) (derive c) (derive d))
-  default liftDerived4 ::
-    LiftDerived repr => Derivable repr =>
-    (Derived repr a -> Derived repr b -> Derived repr c -> Derived repr d -> Derived repr e) ->
-    repr a -> repr b -> repr c -> repr d -> repr e
-
--- * Type synonyms @FromDerived*@
--- | Convenient type synonym for using 'liftDerived' on symantic class @(sym)@.
-type FromDerived  sym repr = ( LiftDerived  repr, sym (Derived repr) )
-type FromDerived1 sym repr = ( LiftDerived1 repr, sym (Derived repr) )
-type FromDerived2 sym repr = ( LiftDerived2 repr, sym (Derived repr) )
-type FromDerived3 sym repr = ( LiftDerived3 repr, sym (Derived repr) )
-type FromDerived4 sym repr = ( LiftDerived4 repr, sym (Derived repr) )
diff --git a/src/Symantic/Fixity.hs b/src/Symantic/Fixity.hs
deleted file mode 100644
--- a/src/Symantic/Fixity.hs
+++ /dev/null
@@ -1,115 +0,0 @@
-module Symantic.Fixity where
-
-import Data.Bool
-import Data.Eq (Eq(..))
-import Data.Function ((.))
-import Data.Int (Int)
-import Data.Maybe (Maybe(..))
-import Data.Ord (Ord(..))
-import Data.Semigroup
-import Data.String (String, IsString(..))
-import Text.Show (Show(..))
-
--- * Type 'Fixity'
-data Fixity
- =   Fixity1 Unifix
- |   Fixity2 Infix
- deriving (Eq, Show)
-
--- ** Type 'Unifix'
-data Unifix
- =   Prefix  { unifix_precedence :: Precedence }
- |   Postfix { unifix_precedence :: Precedence }
- deriving (Eq, Show)
-
--- ** Type 'Infix'
-data Infix
- =   Infix
- {   infix_associativity :: Maybe Associativity
- ,   infix_precedence    :: Precedence
- } deriving (Eq, Show)
-
-infixL :: Precedence -> Infix
-infixL = Infix (Just AssocL)
-
-infixR :: Precedence -> Infix
-infixR = Infix (Just AssocR)
-
-infixB :: Side -> Precedence -> Infix
-infixB = Infix . Just . AssocB
-
-infixN :: Precedence -> Infix
-infixN = Infix Nothing
-
-infixN0 :: Infix
-infixN0 = infixN 0
-
-infixN5 :: Infix
-infixN5 = infixN 5
-
--- | Given 'Precedence' and 'Associativity' of its parent operator,
--- and the operand 'Side' it is in,
--- return whether an 'Infix' operator
--- needs to be enclosed by a 'Pair'.
-isPairNeeded :: (Infix, Side) -> Infix -> Bool
-isPairNeeded (po, lr) op =
-  infix_precedence op < infix_precedence po
-  || infix_precedence op == infix_precedence po
-  && not associate
-  where
-  associate =
-    case (lr, infix_associativity po) of
-     (_, Just AssocB{})   -> True
-     (SideL, Just AssocL) -> True
-     (SideR, Just AssocR) -> True
-     _ -> False
-
--- | If 'isPairNeeded' is 'True',
--- enclose the given 'IsString' by given 'Pair',
--- otherwise returns the same 'IsString'.
-pairIfNeeded ::
- Semigroup s => IsString s =>
- Pair -> (Infix, Side) -> Infix ->
- s -> s
-pairIfNeeded (o,c) po op s =
-  if isPairNeeded po op
-  then fromString o <> s <> fromString c
-  else s
-
--- * Type 'Precedence'
-type Precedence = Int
-
--- ** Class 'PrecedenceOf'
-class PrecedenceOf a where
-  precedence :: a -> Precedence
-instance PrecedenceOf Fixity where
-  precedence (Fixity1 uni) = precedence uni
-  precedence (Fixity2 inf) = precedence inf
-instance PrecedenceOf Unifix where
-  precedence = unifix_precedence
-instance PrecedenceOf Infix where
-  precedence = infix_precedence
-
--- * Type 'Associativity'
-data Associativity
- =   AssocL      -- ^ Associate to the left:  @a ¹ b ² c == (a ¹ b) ² c@
- |   AssocR      -- ^ Associate to the right: @a ¹ b ² c == a ¹ (b ² c)@
- |   AssocB Side -- ^ Associate to both sides, but to 'Side' when reading.
- deriving (Eq, Show)
-
--- ** Type 'Side'
-data Side
- =   SideL -- ^ Left
- |   SideR -- ^ Right
- deriving (Eq, Show)
-
--- ** Type 'Pair'
-type Pair = (String, String)
-pairAngle   :: Pair
-pairBrace   :: Pair
-pairBracket :: Pair
-pairParen   :: Pair
-pairAngle   = ("<",">")
-pairBrace   = ("{","}")
-pairBracket = ("[","]")
-pairParen   = ("(",")")
diff --git a/src/Symantic/Optimize.hs b/src/Symantic/Optimize.hs
deleted file mode 100644
--- a/src/Symantic/Optimize.hs
+++ /dev/null
@@ -1,41 +0,0 @@
-module Symantic.Optimize where
-
-import Data.Bool (Bool)
-import qualified Data.Function as Fun
-
-import Symantic.Classes
-import Symantic.Data
-
--- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
--- but to avoid duplication of work, only those manually marked
--- as using their variable at most once.
---
--- DOC: Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2001,
--- https://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf
-normalOrderReduction :: forall repr a.
-  Abstractable repr =>
-  IfThenElseable repr =>
-  SomeData repr a -> SomeData repr a
-normalOrderReduction = nor
-  where
-  -- | normal-order reduction
-  nor :: SomeData repr b -> SomeData repr b
-  nor = \case
-    Data (Lam f) -> lam (nor Fun.. f)
-    Data (Lam1 f) -> lam1 (nor Fun.. f)
-    Data (x :@ y) -> case whnf x of
-      Data (Lam1 f) -> nor (f y)
-      x' -> nor x' .@ nor y
-    Data (IfThenElse test ok ko) ->
-      case nor test of
-        Data (Constant b :: Data (Constantable Bool) repr Bool) ->
-          if b then nor ok else nor ko
-        t -> ifThenElse (nor t) (nor ok) (nor ko)
-    x -> x
-  -- | weak-head normal-form
-  whnf :: SomeData repr b -> SomeData repr b
-  whnf = \case
-    Data (x :@ y) -> case whnf x of
-      Data (Lam1 f) -> whnf (f y)
-      x' -> x' .@ y
-    x -> x
diff --git a/src/Symantic/Reify.hs b/src/Symantic/Reify.hs
deleted file mode 100644
--- a/src/Symantic/Reify.hs
+++ /dev/null
@@ -1,67 +0,0 @@
-{-# LANGUAGE TemplateHaskell #-}
-{-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- For reifyTH
--- | Reify an Haskell value using type-directed normalisation-by-evaluation (NBE).
-module Symantic.Reify where
-
-import Control.Monad (Monad(..))
-import qualified Data.Function as Fun
-import qualified Language.Haskell.TH as TH
-
-import Symantic.Classes (Abstractable(..))
-
--- | 'ReifyReflect' witnesses the duality between @meta@ and @(repr a)@.
---  It indicates which type variables in @a@ are not to be instantiated
---  with the arrow type, and instantiates them to @(repr _)@ in @meta@.
---  This is directly taken from: http://okmij.org/ftp/tagless-final/course/TDPE.hs
---
--- * @meta@ instantiates polymorphic types of the original Haskell expression
---   with @(repr _)@ types, according to how 'ReifyReflect' is constructed
---   using 'base' and @('-->')@. This is obviously not possible
---   if the orignal expression uses monomorphic types (like 'Int'),
---   but remains possible with constrained polymorphic types (like @(Num i => i)@),
---   because @(i)@ can still be inferred to @(repr _)@,
---   whereas the finally chosen @(repr)@
---   (eg. 'E', or 'Identity', or 'TH.CodeQ', or ...)
---   can have a 'Num' instance.
--- * @(repr a)@ is the symantic type as it would have been,
---   had the expression been written with explicit 'lam's
---   instead of bare haskell functions.
--- DOC: http://okmij.org/ftp/tagless-final/cookbook.html#TDPE
--- 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
-  }
-
--- | The base of induction : placeholder for a type which is not the arrow type.
-base :: ReifyReflect repr (repr a) a
-base = ReifyReflect{reify = Fun.id, reflect = Fun.id}
-
--- | The inductive case : the arrow type.
-infixr 8 -->
-(-->) :: Abstractable repr =>
-         ReifyReflect repr m1 o1 -> ReifyReflect repr m2 o2 ->
-         ReifyReflect repr (m1 -> m2) (o1 -> o2)
-r1 --> r2 = ReifyReflect
-  { reify   = \meta -> lam (reify r2 Fun.. meta Fun.. reflect r1)
-  , reflect = \repr -> reflect r2 Fun.. (.@) repr Fun.. reify r1
-  }
-
--- * Using TemplateHaskell to fully auto-generate 'ReifyReflect'
-
--- | @$(reifyTH 'Foo.bar)@ calls 'reify' on 'Foo.bar'
--- with an 'ReifyReflect' generated from the infered type of 'Foo.bar'.
-reifyTH :: TH.Name -> TH.Q TH.Exp
-reifyTH name = do
-  info <- TH.reify name
-  case info of
-    TH.VarI n (TH.ForallT _vs _ctx ty) _dec ->
-      [| reify $(genReifyReflect ty) $(return (TH.VarE n)) |]
-    where
-    genReifyReflect (TH.AppT (TH.AppT TH.ArrowT a) b) = [| $(genReifyReflect a) --> $(genReifyReflect b) |]
-    genReifyReflect TH.VarT{} = [| base |]
diff --git a/src/Symantic/Semantics.hs b/src/Symantic/Semantics.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Semantics.hs
@@ -0,0 +1,11 @@
+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/Reader.hs b/src/Symantic/Semantics/Reader.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Semantics/Reader.hs
@@ -0,0 +1,53 @@
+module Symantic.Semantics.Reader where
+
+import Data.Function (const, (.))
+
+import Symantic.Syntaxes.Classes hiding (const, (.))
+import Symantic.Syntaxes.Derive
+
+-- * Type 'Reader'
+
+-- | An intermediate interpreter exposing an environment.
+newtype Reader r sem a = Reader {unReader :: r -> sem a}
+
+type instance Derived (Reader r sem) = sem
+instance LiftDerived (Reader r sem) where
+  liftDerived = Reader . const
+instance LiftDerived1 (Reader r sem) where
+  liftDerived1 f a = Reader (f . unReader a)
+instance LiftDerived2 (Reader r sem) where
+  liftDerived2 f a b = Reader (\r -> f (unReader a r) (unReader b r))
+instance LiftDerived3 (Reader r sem) where
+  liftDerived3 f a b c = Reader (\r -> f (unReader a r) (unReader b r) (unReader c r))
+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 Abstractable sem => Abstractable (Reader r sem) where
+  lam f = Reader (\r -> lam ((`unReader` r) . f . liftDerived))
+  lam1 f = Reader (\r -> lam1 ((`unReader` r) . f . liftDerived))
+instance Functionable sem => Functionable (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)
+instance Equalable sem => Equalable (Reader r sem)
+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 Listable sem => Listable (Reader r sem)
+instance Maybeable sem => Maybeable (Reader r sem)
+instance IsoFunctor sem => IsoFunctor (Reader r sem)
+instance (ProductFunctor sem, IsoFunctor sem) => ProductFunctor (Reader r sem)
+instance (SumFunctor sem, IsoFunctor sem) => SumFunctor (Reader r sem)
+instance AlternativeFunctor sem => AlternativeFunctor (Reader r sem)
+instance Dicurryable sem => Dicurryable (Reader r sem)
+instance Emptyable sem => Emptyable (Reader r sem)
+instance Semigroupable sem => Semigroupable (Reader r sem)
+instance Optionable sem => Optionable (Reader r sem)
+instance Repeatable sem => Repeatable (Reader r sem)
+
+-- instance Permutable sem => Permutable (Reader r sem)
+instance Voidable sem => Voidable (Reader r sem)
+instance Substractable sem => Substractable (Reader r sem)
diff --git a/src/Symantic/Semantics/SharingObserver.hs b/src/Symantic/Semantics/SharingObserver.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Semantics/SharingObserver.hs
@@ -0,0 +1,460 @@
+-- For ShowLetName
+{-# LANGUAGE AllowAmbiguousTypes #-}
+-- For makeSharingName
+{-# LANGUAGE BangPatterns #-}
+-- For ShowLetName
+{-# LANGUAGE DataKinds #-}
+-- For SharingName
+{-# LANGUAGE ExistentialQuantification #-}
+
+-- {-# LANGUAGE MagicHash #-} -- For unsafeCoerce#
+module Symantic.Semantics.SharingObserver where
+
+import Control.Applicative (Applicative (..))
+import Control.Monad (Monad (..))
+import Data.Bool
+import Data.Eq (Eq (..))
+import Data.Function (($), (.))
+import Data.Functor (Functor, (<$>))
+import Data.Functor.Compose (Compose (..))
+import Data.HashMap.Strict (HashMap)
+import Data.HashSet (HashSet)
+import Data.Hashable (Hashable, hash, hashWithSalt)
+import Data.Int (Int)
+import Data.Maybe (Maybe (..), isNothing)
+import Data.Monoid (Monoid (..))
+import Data.Ord (Ord (..))
+
+-- import GHC.Exts (Int(..))
+-- import GHC.Prim (unsafeCoerce#)
+import GHC.StableName (StableName (..), eqStableName, hashStableName, makeStableName)
+
+-- import Numeric (showHex)
+
+import Control.Monad.Trans.Class qualified as MT
+import Control.Monad.Trans.Reader qualified as MT
+import Control.Monad.Trans.State qualified as MT
+import Control.Monad.Trans.Writer qualified as MT
+import Data.HashMap.Strict qualified as HM
+import Data.HashSet qualified as HS
+import System.IO (IO)
+import System.IO.Unsafe (unsafePerformIO)
+import Text.Show (Show (..))
+import Prelude (error, (+))
+
+import Symantic.Syntaxes.Derive
+
+-- * Class 'Referenceable'
+
+-- | This class is not for end-users like usual symantic operators,
+-- though it will have to be defined on end-users' interpreters.
+class Referenceable letName sem where
+  -- | @('ref' isRec letName)@ is a reference to @(letName)@.
+  -- It is introduced by 'observeSharing'.
+  -- @(isRec)@ is 'True' iif. this 'ref'erence is recursive,
+  -- ie. appears within its 'define'.
+  --
+  -- TODO: index 'letName' with 'a' to enable dependent-map
+  ref :: Bool -> letName -> sem a
+  ref isRec name = liftDerived (ref isRec name)
+  default ref ::
+    FromDerived (Referenceable letName) sem =>
+    Bool ->
+    letName ->
+    sem a
+
+-- * Class 'Definable'
+
+-- | This class is not for end-users like usual symantic operators.
+-- There should be not need to use it outside this module,
+-- because used 'define's are gathered in 'Letsable'.
+class Definable letName sem where
+  -- | @('define' letName sub)@ let-binds @(letName)@ to be equal to @(sub)@.
+  -- This is a temporary node either replaced
+  -- by 'ref' and an entry in 'lets''s 'LetBindings',
+  -- or removed when no 'ref'erence is made to it.
+  define :: letName -> sem a -> sem a
+  define name = liftDerived1 (define name)
+  default define ::
+    FromDerived1 (Definable letName) sem =>
+    letName ->
+    sem a ->
+    sem a
+
+-- * Class 'MakeLetName'
+class MakeLetName letName where
+  makeLetName :: SharingName -> IO letName
+
+-- * Type 'SharingName'
+
+-- | Note that the observable sharing enabled by 'StableName'
+-- is not perfect as it will not observe all the sharing explicitely done.
+--
+-- Note also that the observed sharing could be different between ghc and ghci.
+data SharingName = forall a. SharingName (StableName a)
+
+-- | @('makeSharingName' x)@ is like @('makeStableName' x)@ but it also forces
+-- evaluation of @(x)@ to ensure that the 'StableName' is correct first time,
+-- which avoids to produce a tree bigger than needed.
+--
+-- Note that this function uses 'unsafePerformIO' instead of returning in 'IO',
+-- this is apparently required to avoid infinite loops due to unstable 'StableName'
+-- in compiled code, and sometimes also in ghci.
+--
+-- Note that maybe [pseq should be used here](https://gitlab.haskell.org/ghc/ghc/-/issues/2916).
+makeSharingName :: a -> SharingName
+makeSharingName !x = SharingName $ unsafePerformIO $ makeStableName x
+
+instance Eq SharingName where
+  SharingName x == SharingName y = eqStableName x y
+instance Hashable SharingName where
+  hash (SharingName n) = hashStableName n
+  hashWithSalt salt (SharingName n) = hashWithSalt salt n
+
+{-
+instance Show SharingName where
+  showsPrec _ (SharingName n) = showHex (I# (unsafeCoerce# n))
+-}
+
+-- * Type 'SharingObserver'
+newtype SharingObserver letName sem a = SharingObserver
+  { unSharingObserver ::
+      MT.ReaderT
+        (HashSet SharingName)
+        (MT.State (SharingObserverState letName))
+        (SharingFinalizer letName sem a)
+  }
+
+-- | Interpreter detecting some (Haskell embedded) @let@ definitions used at
+-- least once and/or recursively, in order to replace them
+-- with the 'lets' and 'ref' combinators.
+-- See [Type-safe observable sharing in Haskell](https://doi.org/10.1145/1596638.1596653)
+--
+-- Beware not to apply 'observeSharing' more than once on the same term
+-- otherwise some 'define' introduced by the first call
+-- would be removed by the second call.
+observeSharing ::
+  Eq letName =>
+  Hashable letName =>
+  Show letName =>
+  SharingObserver letName sem a ->
+  WithSharing letName sem a
+observeSharing (SharingObserver m) =
+  let (fs, st) =
+        MT.runReaderT m mempty
+          `MT.runState` SharingObserverState
+            { oss_refs = HM.empty
+            , oss_recs = HS.empty
+            }
+   in let refs =
+            HS.fromList
+              [ letName
+              | (letName, refCount) <- HM.elems (oss_refs st)
+              , refCount > 0
+              ]
+       in --trace (show refs) $
+          MT.runWriter $
+            (`MT.runReaderT` refs) $
+              unFinalizeSharing fs
+
+-- ** Type 'WithSharing'
+type WithSharing letName sem a =
+  (sem a, HM.HashMap letName (SomeLet sem))
+
+{-
+-- * Type 'WithSharing'
+data WithSharing letName sem a = WithSharing
+  { lets :: HM.HashMap letName (SomeLet sem)
+  , body :: sem a
+  }
+mapWithSharing ::
+  (forall v. sem v -> sem v) ->
+  WithSharing letName sem a ->
+  WithSharing letName sem a
+mapWithSharing f ws = WithSharing
+  { lets = (\(SomeLet sem) -> SomeLet (f sem)) <$> lets ws
+  , body = f (body ws)
+  }
+-}
+
+-- ** Type 'SharingObserverState'
+data SharingObserverState letName = SharingObserverState
+  { oss_refs :: HashMap SharingName (letName, Int)
+  , oss_recs :: HashSet SharingName
+  }
+
+observeSharingNode ::
+  Eq letName =>
+  Hashable letName =>
+  Show letName =>
+  Referenceable letName sem =>
+  MakeLetName letName =>
+  SharingObserver letName sem a ->
+  SharingObserver letName sem a
+observeSharingNode (SharingObserver m) = SharingObserver $ do
+  let nodeName = makeSharingName m
+  st <- MT.lift MT.get
+  ((letName, seenBefore), seen) <-
+    getCompose $
+      HM.alterF
+        ( \seenBefore ->
+            -- Compose is used to return (letName, seenBefore) along seen
+            -- in the same HashMap lookup.
+            Compose $
+              return $ case seenBefore of
+                Nothing ->
+                  ((letName, seenBefore), Just (letName, 0))
+                  where
+                    letName = unsafePerformIO $ makeLetName nodeName
+                Just (letName, refCount) ->
+                  ((letName, seenBefore), Just (letName, refCount + 1))
+        )
+        nodeName
+        (oss_refs st)
+  parentNames <- MT.ask
+  if nodeName `HS.member` parentNames
+    then do
+      -- recursive reference to nodeName:
+      -- update seen references
+      -- and mark nodeName as recursive
+      MT.lift $
+        MT.put
+          st
+            { oss_refs = seen
+            , oss_recs = HS.insert nodeName (oss_recs st)
+            }
+      return $ ref True letName
+    else do
+      -- non-recursive reference to nodeName:
+      -- update seen references
+      -- and recurse if the nodeName hasn't been seen before
+      -- (would be in a preceding sibling branch, not in parentNames).
+      MT.lift $ MT.put st{oss_refs = seen}
+      if isNothing seenBefore
+        then MT.local (HS.insert nodeName) (define letName <$> m)
+        else return $ ref False letName
+
+type instance Derived (SharingObserver letName sem) = SharingFinalizer letName sem
+instance
+  ( Referenceable letName sem
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  , Show letName
+  ) =>
+  LiftDerived (SharingObserver letName sem)
+  where
+  liftDerived = observeSharingNode . SharingObserver . return
+instance
+  ( Referenceable letName sem
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  , Show letName
+  ) =>
+  LiftDerived1 (SharingObserver letName sem)
+  where
+  liftDerived1 f a =
+    observeSharingNode $
+      SharingObserver $
+        f <$> unSharingObserver a
+instance
+  ( Referenceable letName sem
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  , Show letName
+  ) =>
+  LiftDerived2 (SharingObserver letName sem)
+  where
+  liftDerived2 f a b =
+    observeSharingNode $
+      SharingObserver $
+        f <$> unSharingObserver a
+          <*> unSharingObserver b
+instance
+  ( Referenceable letName sem
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  , Show letName
+  ) =>
+  LiftDerived3 (SharingObserver letName sem)
+  where
+  liftDerived3 f a b c =
+    observeSharingNode $
+      SharingObserver $
+        f <$> unSharingObserver a
+          <*> unSharingObserver b
+          <*> unSharingObserver c
+instance
+  ( Referenceable letName sem
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  , Show letName
+  ) =>
+  LiftDerived4 (SharingObserver letName sem)
+  where
+  liftDerived4 f a b c d =
+    observeSharingNode $
+      SharingObserver $
+        f <$> unSharingObserver a
+          <*> unSharingObserver b
+          <*> unSharingObserver c
+          <*> unSharingObserver d
+instance Referenceable letName (SharingObserver letName sem) where
+  ref = error "[BUG]: observeSharing MUST NOT be applied twice"
+instance Definable letName (SharingObserver letName sem) where
+  define = error "[BUG]: observeSharing MUST NOT be applied twice"
+instance Letsable letName (SharingObserver letName sem) where
+  lets = error "[BUG]: observeSharing MUST NOT be applied twice"
+
+-- * Type 'SharingFinalizer'
+
+-- | Remove 'define' when non-recursive or unused
+-- or replace it by 'ref', moving 'define's to the top.
+newtype SharingFinalizer letName sem a = SharingFinalizer
+  { unFinalizeSharing ::
+      MT.ReaderT
+        (HS.HashSet letName)
+        (MT.Writer (LetBindings letName sem))
+        (sem a)
+  }
+
+type instance Derived (SharingFinalizer _letName sem) = sem
+instance
+  (Eq letName, Hashable letName) =>
+  LiftDerived (SharingFinalizer letName sem)
+  where
+  liftDerived = SharingFinalizer . pure
+instance
+  (Eq letName, Hashable letName) =>
+  LiftDerived1 (SharingFinalizer letName sem)
+  where
+  liftDerived1 f a = SharingFinalizer $ f <$> unFinalizeSharing a
+instance
+  (Eq letName, Hashable letName) =>
+  LiftDerived2 (SharingFinalizer letName sem)
+  where
+  liftDerived2 f a b =
+    SharingFinalizer $
+      f <$> unFinalizeSharing a
+        <*> unFinalizeSharing b
+instance
+  (Eq letName, Hashable letName) =>
+  LiftDerived3 (SharingFinalizer letName sem)
+  where
+  liftDerived3 f a b c =
+    SharingFinalizer $
+      f <$> unFinalizeSharing a
+        <*> unFinalizeSharing b
+        <*> unFinalizeSharing c
+instance
+  (Eq letName, Hashable letName) =>
+  LiftDerived4 (SharingFinalizer letName sem)
+  where
+  liftDerived4 f a b c d =
+    SharingFinalizer $
+      f <$> unFinalizeSharing a
+        <*> unFinalizeSharing b
+        <*> unFinalizeSharing c
+        <*> unFinalizeSharing d
+instance
+  ( Referenceable letName sem
+  , Eq letName
+  , Hashable letName
+  , Show letName
+  ) =>
+  Referenceable letName (SharingFinalizer letName sem)
+  where
+  ref isRec = liftDerived . ref isRec
+instance
+  ( Referenceable letName sem
+  , Eq letName
+  , Hashable letName
+  , Show letName
+  ) =>
+  Definable letName (SharingFinalizer letName sem)
+  where
+  define name body = SharingFinalizer $ do
+    refs <- MT.ask
+    let (sem, defs) =
+          MT.runWriter $ MT.runReaderT (unFinalizeSharing body) refs
+    if name `HS.member` refs
+      then do
+        -- This 'define' is 'ref'erenced: move it into the result,
+        -- to put it in scope even when some 'ref' to it exists outside of 'body'
+        -- (which can happen when a body-expression is shared),
+        -- and replace it by a 'ref'.
+        MT.lift $ MT.tell $ HM.insert name (SomeLet sem) defs
+        return $ ref False name
+      else -- Remove this unreferenced 'define' node.
+        unFinalizeSharing body
+
+-- * Class 'Letsable'
+class Letsable letName sem where
+  -- | @('lets' defs x)@ let-binds @(defs)@ in @(x)@.
+  lets :: LetBindings letName sem -> sem a -> sem a
+  lets defs = liftDerived1 (lets ((\(SomeLet val) -> SomeLet (derive val)) <$> defs))
+  default lets ::
+    Derivable sem =>
+    FromDerived1 (Letsable letName) sem =>
+    LetBindings letName sem ->
+    sem a ->
+    sem a
+
+-- ** Type 'SomeLet'
+data SomeLet sem = forall a. SomeLet (sem a)
+
+-- ** Type 'LetBindings'
+type LetBindings letName sem = HM.HashMap letName (SomeLet sem)
+
+{-
+-- | Not used but can be written nonetheless.
+instance
+  ( Letsable letName sem
+  , Eq letName
+  , Hashable letName
+  , Show letName
+  ) => Letsable letName (SharingFinalizer letName sem) where
+  lets defs x = SharingFinalizer $ do
+    ds <- traverse (\(SomeLet v) -> do
+      r <- unFinalizeSharing v
+      return (SomeLet r)
+      ) defs
+    MT.lift $ MT.tell ds
+    unFinalizeSharing x
+-}
+
+-- ** Type 'OpenRecs'
+
+-- | Mutually recursive terms, in open recursion style.
+type OpenRecs letName a = LetRecs letName (OpenRec letName a)
+
+-- | Mutually recursive term, in open recursion style.
+-- The term is given a @final@ (aka. @self@) map
+-- of other terms it can refer to (including itself).
+type OpenRec letName a = LetRecs letName a -> a
+
+-- | Recursive let bindings.
+type LetRecs letName = HM.HashMap letName
+
+-- | Least fixpoint combinator.
+fix :: (a -> a) -> a
+fix f = final where final = f final
+
+-- | Least fixpoint combinator of mutually recursive terms.
+-- @('mutualFix' opens)@ takes a container of terms
+-- in the open recursion style @(opens)@,
+-- and return that container of terms with their knots tied-up.
+--
+-- Used to express mutual recursion and to transparently introduce memoization.
+--
+-- Here all mutually dependent functions are restricted to the same polymorphic type @(a)@.
+-- See http://okmij.org/ftp/Computation/fixed-point-combinators.html#Poly-variadic
+mutualFix :: forall recs a. Functor recs => recs ({-finals-} recs a -> a) -> recs a
+mutualFix opens = fix f
+  where
+    f :: recs a -> recs a
+    f recs = ($ recs) <$> opens
diff --git a/src/Symantic/Semantics/ToFer.hs b/src/Symantic/Semantics/ToFer.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Semantics/ToFer.hs
@@ -0,0 +1,81 @@
+{-# 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, if 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 =>
+    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/Semantics/Viewer.hs b/src/Symantic/Semantics/Viewer.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Semantics/Viewer.hs
@@ -0,0 +1,125 @@
+-- For Viewer
+{-# LANGUAGE GADTs #-}
+-- For convenience
+{-# LANGUAGE OverloadedStrings #-}
+-- For Show (SomeData a)
+{-# LANGUAGE UndecidableInstances #-}
+
+module Symantic.Semantics.Viewer where
+
+import Data.Function qualified as Fun
+import Data.Int (Int)
+import Data.String
+import Text.Show
+import Prelude qualified
+
+import Symantic.Semantics.Viewer.Fixity
+import Symantic.Syntaxes.Classes
+import Symantic.Syntaxes.Data
+import Symantic.Syntaxes.Derive
+
+data Viewer a where
+  Viewer :: (ViewerEnv -> ShowS) -> Viewer a
+  ViewerUnifix :: Unifix -> String -> String -> Viewer (a -> b)
+  ViewerInfix :: Infix -> String -> String -> Viewer (a -> b -> c)
+  ViewerApp :: Viewer (b -> a) -> Viewer b -> Viewer a
+
+runViewer :: Viewer a -> ViewerEnv -> ShowS
+runViewer (Viewer v) env = v env
+runViewer (ViewerInfix _op name _infixName) _env = showString name
+runViewer (ViewerUnifix _op name _unifixName) _env = showString name
+runViewer (ViewerApp f x) env =
+  pairViewer env op Fun.$
+    runViewer f env{viewEnv_op = (op, SideL)}
+      Fun.. showString " "
+      Fun.. runViewer x env{viewEnv_op = (op, SideR)}
+  where
+    op = infixN 10
+
+-- | Unusual, but enables to leverage default definition of methods.
+type instance Derived Viewer = Viewer
+
+instance LiftDerived Viewer where
+  liftDerived = Fun.id
+
+instance IsString (Viewer a) where
+  fromString s = Viewer Fun.$ \_env -> showString s
+instance Show (Viewer a) where
+  showsPrec p =
+    ( `runViewer`
+        ViewerEnv
+          { viewEnv_op = (infixN p, SideL)
+          , viewEnv_pair = pairParen
+          , viewEnv_lamDepth = 1
+          }
+    )
+instance Show (SomeData Viewer a) where
+  showsPrec p (SomeData x) = showsPrec p (derive x :: Viewer a)
+
+data ViewerEnv = ViewerEnv
+  { viewEnv_op :: (Infix, Side)
+  , viewEnv_pair :: Pair
+  , viewEnv_lamDepth :: Int
+  }
+
+pairViewer :: ViewerEnv -> Infix -> ShowS -> ShowS
+pairViewer env op s =
+  if isPairNeeded (viewEnv_op env) op
+    then showString o Fun.. s Fun.. showString c
+    else s
+  where
+    (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
+instance Unabstractable Viewer where
+  ViewerInfix op _name infixName .@ ViewerApp x y = Viewer Fun.$ \env ->
+    pairViewer env op Fun.$
+      runViewer x env{viewEnv_op = (op, SideL)}
+        Fun.. showString " "
+        Fun.. showString infixName
+        Fun.. showString " "
+        Fun.. runViewer y env{viewEnv_op = (op, SideR)}
+  ViewerInfix op name _infixName .@ x = Viewer Fun.$ \env ->
+    showParen Prelude.True Fun.$
+      runViewer x env{viewEnv_op = (op, SideL)}
+        Fun.. showString " "
+        Fun.. showString name
+  f .@ x = ViewerApp f x
+instance Anythingable Viewer
+instance Bottomable Viewer where
+  bottom = "<hidden>"
+instance Show c => Constantable c Viewer where
+  constant c = Viewer Fun.$ \_env -> shows c
+instance Eitherable Viewer where
+  either = "either"
+  left = "Left"
+  right = "Right"
+instance Equalable Viewer where
+  equal = ViewerInfix (infixN 4) "(==)" "=="
+instance Listable Viewer where
+  cons = ViewerInfix (infixR 5) "(:)" ":"
+  nil = "[]"
+instance Maybeable Viewer where
+  nothing = "Nothing"
+  just = "Just"
diff --git a/src/Symantic/Semantics/Viewer/Fixity.hs b/src/Symantic/Semantics/Viewer/Fixity.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Semantics/Viewer/Fixity.hs
@@ -0,0 +1,124 @@
+module Symantic.Semantics.Viewer.Fixity where
+
+import Data.Bool
+import Data.Eq (Eq (..))
+import Data.Function ((.))
+import Data.Int (Int)
+import Data.Maybe (Maybe (..))
+import Data.Ord (Ord (..))
+import Data.Semigroup
+import Data.String (IsString (..), String)
+import Text.Show (Show (..))
+
+-- * Type 'Fixity'
+data Fixity
+  = Fixity1 Unifix
+  | Fixity2 Infix
+  deriving (Eq, Show)
+
+-- ** Type 'Unifix'
+data Unifix
+  = Prefix {unifix_precedence :: Precedence}
+  | Postfix {unifix_precedence :: Precedence}
+  deriving (Eq, Show)
+
+-- ** Type 'Infix'
+data Infix = Infix
+  { infix_associativity :: Maybe Associativity
+  , infix_precedence :: Precedence
+  }
+  deriving (Eq, Show)
+
+infixL :: Precedence -> Infix
+infixL = Infix (Just AssocL)
+
+infixR :: Precedence -> Infix
+infixR = Infix (Just AssocR)
+
+infixB :: Side -> Precedence -> Infix
+infixB = Infix . Just . AssocB
+
+infixN :: Precedence -> Infix
+infixN = Infix Nothing
+
+infixN0 :: Infix
+infixN0 = infixN 0
+
+infixN5 :: Infix
+infixN5 = infixN 5
+
+-- | Given 'Precedence' and 'Associativity' of its parent operator,
+-- and the operand 'Side' it is in,
+-- return whether an 'Infix' operator
+-- needs to be enclosed by a 'Pair'.
+isPairNeeded :: (Infix, Side) -> Infix -> Bool
+isPairNeeded (po, lr) op =
+  infix_precedence op < infix_precedence po
+    || infix_precedence op == infix_precedence po
+    && not associate
+  where
+    associate =
+      case (lr, infix_associativity po) of
+        (_, Just AssocB{}) -> True
+        (SideL, Just AssocL) -> True
+        (SideR, Just AssocR) -> True
+        _ -> False
+
+-- | If 'isPairNeeded' is 'True',
+-- enclose the given 'IsString' by given 'Pair',
+-- otherwise returns the same 'IsString'.
+pairIfNeeded ::
+  Semigroup s =>
+  IsString s =>
+  Pair ->
+  (Infix, Side) ->
+  Infix ->
+  s ->
+  s
+pairIfNeeded (o, c) po op s =
+  if isPairNeeded po op
+    then fromString o <> s <> fromString c
+    else s
+
+-- * Type 'Precedence'
+type Precedence = Int
+
+-- ** Class 'PrecedenceOf'
+class PrecedenceOf a where
+  precedence :: a -> Precedence
+instance PrecedenceOf Fixity where
+  precedence (Fixity1 uni) = precedence uni
+  precedence (Fixity2 inf) = precedence inf
+instance PrecedenceOf Unifix where
+  precedence = unifix_precedence
+instance PrecedenceOf Infix where
+  precedence = infix_precedence
+
+-- * Type 'Associativity'
+data Associativity
+  = -- | Associate to the left:  @a ¹ b ² c == (a ¹ b) ² c@
+    AssocL
+  | -- | Associate to the right: @a ¹ b ² c == a ¹ (b ² c)@
+    AssocR
+  | -- | Associate to both sides, but to 'Side' when reading.
+    AssocB Side
+  deriving (Eq, Show)
+
+-- ** Type 'Side'
+data Side
+  = -- | Left
+    SideL
+  | -- | Right
+    SideR
+  deriving (Eq, Show)
+
+-- ** Type 'Pair'
+type Pair = (String, String)
+pairAngle :: Pair
+pairBrace :: Pair
+pairBracket :: Pair
+pairParen :: Pair
+pairAngle = ("<", ">")
+pairBrace = ("{", "}")
+pairBracket = ("[", "]")
+pairParen = ("(", ")")
diff --git a/src/Symantic/SharingObserver.hs b/src/Symantic/SharingObserver.hs
deleted file mode 100644
--- a/src/Symantic/SharingObserver.hs
+++ /dev/null
@@ -1,385 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-} -- For ShowLetName
-{-# LANGUAGE BangPatterns #-} -- For makeSharingName
-{-# LANGUAGE DataKinds #-} -- For ShowLetName
-{-# LANGUAGE ExistentialQuantification #-} -- For SharingName
--- {-# LANGUAGE MagicHash #-} -- For unsafeCoerce#
-module Symantic.SharingObserver where
-
-import Control.Applicative (Applicative(..))
-import Control.Monad (Monad(..))
-import Data.Bool
-import Data.Eq (Eq(..))
-import Data.Function (($), (.))
-import Data.Functor (Functor, (<$>))
-import Data.Functor.Compose (Compose(..))
-import Data.HashMap.Strict (HashMap)
-import Data.HashSet (HashSet)
-import Data.Hashable (Hashable, hashWithSalt, hash)
-import Data.Int (Int)
-import Data.Maybe (Maybe(..), isNothing)
-import Data.Monoid (Monoid(..))
-import Data.Ord (Ord(..))
--- import GHC.Exts (Int(..))
--- import GHC.Prim (unsafeCoerce#)
-import GHC.StableName (StableName(..), makeStableName, hashStableName, eqStableName)
--- import Numeric (showHex)
-import Prelude ((+), error)
-import System.IO (IO)
-import System.IO.Unsafe (unsafePerformIO)
-import Text.Show (Show(..))
-import qualified Control.Monad.Trans.Class as MT
-import qualified Control.Monad.Trans.Reader as MT
-import qualified Control.Monad.Trans.State as MT
-import qualified Control.Monad.Trans.Writer as MT
-import qualified Data.HashMap.Strict as HM
-import qualified Data.HashSet as HS
-
-import Symantic.Derive
-
--- * Class 'Referenceable'
--- | This class is not for end-users like usual symantic operators,
--- though it will have to be defined on end-users' interpreters.
-class Referenceable letName repr where
-  -- | @('ref' isRec letName)@ is a reference to @(letName)@.
-  -- It is introduced by 'observeSharing'.
-  -- @(isRec)@ is 'True' iif. this 'ref'erence is recursive,
-  -- ie. appears within its 'define'.
-  --
-  -- TODO: index 'letName' with 'a' to enable dependent-map
-  ref :: Bool -> letName -> repr a
-  ref isRec name = liftDerived (ref isRec name)
-  default ref ::
-    FromDerived (Referenceable letName) repr =>
-    Bool -> letName -> repr a
-
--- * Class 'Definable'
--- | This class is not for end-users like usual symantic operators.
--- There should be not need to use it outside this module,
--- because used 'define's are gathered in 'Letsable'.
-class Definable letName repr where
-  -- | @('define' letName sub)@ let-binds @(letName)@ to be equal to @(sub)@.
-  -- This is a temporary node either replaced
-  -- by 'ref' and an entry in 'lets''s 'LetBindings',
-  -- or removed when no 'ref'erence is made to it.
-  define :: letName -> repr a -> repr a
-  define name = liftDerived1 (define name)
-  default define ::
-    FromDerived1 (Definable letName) repr =>
-    letName -> repr a -> repr a
-
--- * Class 'MakeLetName'
-class MakeLetName letName where
-  makeLetName :: SharingName -> IO letName
-
--- * Type 'SharingName'
--- | Note that the observable sharing enabled by 'StableName'
--- is not perfect as it will not observe all the sharing explicitely done.
---
--- Note also that the observed sharing could be different between ghc and ghci.
-data SharingName = forall a. SharingName (StableName a)
--- | @('makeSharingName' x)@ is like @('makeStableName' x)@ but it also forces
--- evaluation of @(x)@ to ensure that the 'StableName' is correct first time,
--- which avoids to produce a tree bigger than needed.
---
--- Note that this function uses 'unsafePerformIO' instead of returning in 'IO',
--- this is apparently required to avoid infinite loops due to unstable 'StableName'
--- in compiled code, and sometimes also in ghci.
---
--- Note that maybe [pseq should be used here](https://gitlab.haskell.org/ghc/ghc/-/issues/2916).
-makeSharingName :: a -> SharingName
-makeSharingName !x = SharingName $ unsafePerformIO $ makeStableName x
-
-instance Eq SharingName where
-  SharingName x == SharingName y = eqStableName x y
-instance Hashable SharingName where
-  hash (SharingName n) = hashStableName n
-  hashWithSalt salt (SharingName n) = hashWithSalt salt n
-{-
-instance Show SharingName where
-  showsPrec _ (SharingName n) = showHex (I# (unsafeCoerce# n))
--}
-
--- * Type 'SharingObserver'
-newtype SharingObserver letName repr a = SharingObserver { unSharingObserver ::
-  MT.ReaderT (HashSet SharingName)
-             (MT.State (SharingObserverState letName))
-             (SharingFinalizer letName repr a) }
-
--- | Interpreter detecting some (Haskell embedded) @let@ definitions used at
--- least once and/or recursively, in order to replace them
--- with the 'lets' and 'ref' combinators.
--- See [Type-safe observable sharing in Haskell](https://doi.org/10.1145/1596638.1596653)
---
--- Beware not to apply 'observeSharing' more than once on the same term
--- otherwise some 'define' introduced by the first call
--- would be removed by the second call.
-observeSharing ::
-  Eq letName =>
-  Hashable letName =>
-  Show letName =>
-  SharingObserver letName repr a ->
-  WithSharing letName repr a
-observeSharing (SharingObserver m) =
-  let (fs, st) = MT.runReaderT m mempty `MT.runState`
-        SharingObserverState
-          { oss_refs = HM.empty
-          , oss_recs = HS.empty
-          } in
-  let refs = HS.fromList
-        [ letName
-        | (letName, refCount) <- HM.elems (oss_refs st)
-        , refCount > 0
-        ] in
-  --trace (show refs) $
-  MT.runWriter $
-  (`MT.runReaderT` refs) $
-  unFinalizeSharing fs
-
--- ** Type 'WithSharing'
-type WithSharing letName repr a =
-  (repr a, HM.HashMap letName (SomeLet repr))
-{-
--- * Type 'WithSharing'
-data WithSharing letName repr a = WithSharing
-  { lets :: HM.HashMap letName (SomeLet repr)
-  , body :: repr a
-  }
-mapWithSharing ::
-  (forall v. repr v -> repr v) ->
-  WithSharing letName repr a ->
-  WithSharing letName repr a
-mapWithSharing f ws = WithSharing
-  { lets = (\(SomeLet repr) -> SomeLet (f repr)) <$> lets ws
-  , body = f (body ws)
-  }
--}
-
--- ** Type 'SharingObserverState'
-data SharingObserverState letName = SharingObserverState
-  { oss_refs :: HashMap SharingName (letName, Int)
-  , oss_recs :: HashSet SharingName
-  }
-
-observeSharingNode ::
-  Eq letName =>
-  Hashable letName =>
-  Show letName =>
-  Referenceable letName repr =>
-  MakeLetName letName =>
-  SharingObserver letName repr a ->
-  SharingObserver letName repr a
-observeSharingNode (SharingObserver m) = SharingObserver $ do
-  let nodeName = makeSharingName m
-  st <- MT.lift MT.get
-  ((letName, seenBefore), seen) <- getCompose $ HM.alterF (\seenBefore ->
-    -- Compose is used to return (letName, seenBefore) along seen
-    -- in the same HashMap lookup.
-    Compose $ return $ case seenBefore of
-      Nothing ->
-        ((letName, seenBefore), Just (letName, 0))
-        where letName = unsafePerformIO $ makeLetName nodeName
-      Just (letName, refCount) ->
-        ((letName, seenBefore), Just (letName, refCount + 1))
-    ) nodeName (oss_refs st)
-  parentNames <- MT.ask
-  if nodeName `HS.member` parentNames
-  then do -- recursive reference to nodeName:
-          -- update seen references
-          -- and mark nodeName as recursive
-    MT.lift $ MT.put st
-      { oss_refs = seen
-      , oss_recs = HS.insert nodeName (oss_recs st)
-      }
-    return $ ref True letName
-  else do -- non-recursive reference to nodeName
-          -- update seen references
-          -- and recurse if the nodeName hasn't been seen before
-          -- (would be in a preceding sibling branch, not in parentNames).
-    MT.lift $ MT.put st{ oss_refs = seen }
-    if isNothing seenBefore
-      then MT.local (HS.insert nodeName) (define letName <$> m)
-      else return $ ref False letName
-
-type instance Derived (SharingObserver letName repr) = SharingFinalizer letName repr
-instance
-  ( Referenceable letName repr
-  , MakeLetName letName
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => LiftDerived (SharingObserver letName repr) where
-  liftDerived = observeSharingNode . SharingObserver . return
-instance
-  ( Referenceable letName repr
-  , MakeLetName letName
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => LiftDerived1 (SharingObserver letName repr) where
-  liftDerived1 f a = observeSharingNode $ SharingObserver $
-    f <$> unSharingObserver a
-instance
-  ( Referenceable letName repr
-  , MakeLetName letName
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => LiftDerived2 (SharingObserver letName repr) where
-  liftDerived2 f a b = observeSharingNode $ SharingObserver $
-    f <$> unSharingObserver a
-      <*> unSharingObserver b
-instance
-  ( Referenceable letName repr
-  , MakeLetName letName
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => LiftDerived3 (SharingObserver letName repr) where
-  liftDerived3 f a b c = observeSharingNode $ SharingObserver $
-    f <$> unSharingObserver a
-      <*> unSharingObserver b
-      <*> unSharingObserver c
-instance
-  ( Referenceable letName repr
-  , MakeLetName letName
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => LiftDerived4 (SharingObserver letName repr) where
-  liftDerived4 f a b c d = observeSharingNode $ SharingObserver $
-    f <$> unSharingObserver a
-      <*> unSharingObserver b
-      <*> unSharingObserver c
-      <*> unSharingObserver d
-instance Referenceable letName (SharingObserver letName repr) where
-  ref = error "[BUG]: observeSharing MUST NOT be applied twice"
-instance Definable letName (SharingObserver letName repr) where
-  define = error "[BUG]: observeSharing MUST NOT be applied twice"
-instance Letsable letName (SharingObserver letName repr) where
-  lets = error "[BUG]: observeSharing MUST NOT be applied twice"
-
--- * Type 'SharingFinalizer'
--- | Remove 'define' when non-recursive or unused
--- or replace it by 'ref', moving 'define's to the top.
-newtype SharingFinalizer letName repr a = SharingFinalizer { unFinalizeSharing ::
-  MT.ReaderT (HS.HashSet letName)
-    (MT.Writer (LetBindings letName repr))
-      (repr a) }
-
-type instance Derived (SharingFinalizer _letName repr) = repr
-instance (Eq letName, Hashable letName) =>
-  LiftDerived (SharingFinalizer letName repr) where
-  liftDerived = SharingFinalizer . pure
-instance (Eq letName, Hashable letName) =>
-  LiftDerived1 (SharingFinalizer letName repr) where
-  liftDerived1 f a = SharingFinalizer $ f <$> unFinalizeSharing a
-instance (Eq letName, Hashable letName) =>
-  LiftDerived2 (SharingFinalizer letName repr) where
-  liftDerived2 f a b = SharingFinalizer $
-    f <$> unFinalizeSharing a
-      <*> unFinalizeSharing b
-instance (Eq letName, Hashable letName) =>
-  LiftDerived3 (SharingFinalizer letName repr) where
-  liftDerived3 f a b c = SharingFinalizer $
-    f <$> unFinalizeSharing a
-      <*> unFinalizeSharing b
-      <*> unFinalizeSharing c
-instance (Eq letName, Hashable letName) =>
-  LiftDerived4 (SharingFinalizer letName repr) where
-  liftDerived4 f a b c d = SharingFinalizer $
-    f <$> unFinalizeSharing a
-      <*> unFinalizeSharing b
-      <*> unFinalizeSharing c
-      <*> unFinalizeSharing d
-instance
-  ( Referenceable letName repr
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => Referenceable letName (SharingFinalizer letName repr) where
-  ref isRec = liftDerived . ref isRec
-instance
-  ( Referenceable letName repr
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => Definable letName (SharingFinalizer letName repr) where
-  define name body = SharingFinalizer $ do
-    refs <- MT.ask
-    let (repr, defs) =
-          MT.runWriter $ MT.runReaderT (unFinalizeSharing body) refs
-    if name `HS.member` refs
-      then do
-        -- This 'define' is 'ref'erenced: move it into the result,
-        -- to put it in scope even when some 'ref' to it exists outside of 'body'
-        -- (which can happen when a body-expression is shared),
-        -- and replace it by a 'ref'.
-        MT.lift $ MT.tell $ HM.insert name (SomeLet repr) defs
-        return $ ref False name
-      else
-        -- Remove this unreferenced 'define' node.
-        unFinalizeSharing body
-
--- * Class 'Letsable'
-class Letsable letName repr where
-  -- | @('lets' defs x)@ let-binds @(defs)@ in @(x)@.
-  lets :: LetBindings letName repr -> repr a -> repr a
-  lets defs = liftDerived1 (lets ((\(SomeLet val) -> SomeLet (derive val)) <$> defs))
-  default lets ::
-    Derivable repr =>
-    FromDerived1 (Letsable letName) repr =>
-    LetBindings letName repr -> repr a -> repr a
-
--- ** Type 'SomeLet'
-data SomeLet repr = forall a. SomeLet (repr a)
-
--- ** Type 'LetBindings'
-type LetBindings letName repr = HM.HashMap letName (SomeLet repr)
-
-{-
--- | Not used but can be written nonetheless.
-instance
-  ( Letsable letName repr
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => Letsable letName (SharingFinalizer letName repr) where
-  lets defs x = SharingFinalizer $ do
-    ds <- traverse (\(SomeLet v) -> do
-      r <- unFinalizeSharing v
-      return (SomeLet r)
-      ) defs
-    MT.lift $ MT.tell ds
-    unFinalizeSharing x
--}
-
--- ** Type 'OpenRecs'
--- | Mutually recursive terms, in open recursion style.
-type OpenRecs letName a = LetRecs letName (OpenRec letName a)
--- | Mutually recursive term, in open recursion style.
--- The term is given a @final@ (aka. @self@) map
--- of other terms it can refer to (including itself).
-type OpenRec letName a = LetRecs letName a -> a
--- | Recursive let bindings.
-type LetRecs letName = HM.HashMap letName
-
--- | Least fixpoint combinator.
-fix :: (a -> a) -> a
-fix f = final where final = f final
-
--- | Lest fixpoint combinator of mutually recursive terms.
--- @('mutualFix' opens)@ takes a container of terms
--- in the open recursion style @(opens)@,
--- and return that container of terms with their knots tied-up.
---
--- Used to express mutual recursion and to transparently introduce memoization,
--- between observed sharing ('defLet', 'call', 'jump')
--- and also between join points ('defJoin', 'refJoin').
---
--- Here all mutually dependent functions are restricted to the same polymorphic type @(a)@.
--- See http://okmij.org/ftp/Computation/fixed-point-combinators.html#Poly-variadic
-mutualFix :: forall recs a. Functor recs => recs ({-finals-}recs a -> a) -> recs a
-mutualFix opens = fix f
-  where
-  f :: recs a -> recs a
-  f recs = ($ recs) <$> opens
diff --git a/src/Symantic/Syntaxes.hs b/src/Symantic/Syntaxes.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Syntaxes.hs
@@ -0,0 +1,17 @@
+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,
+  module Symantic.Syntaxes.TuplesOfFunctions,
+) where
+
+import Symantic.Syntaxes.Classes
+import Symantic.Syntaxes.CurryN
+import Symantic.Syntaxes.Data
+import Symantic.Syntaxes.Derive
+import Symantic.Syntaxes.EithersOfTuples
+import Symantic.Syntaxes.Reify
+import Symantic.Syntaxes.TuplesOfFunctions
diff --git a/src/Symantic/Syntaxes/Classes.hs b/src/Symantic/Syntaxes/Classes.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Syntaxes/Classes.hs
@@ -0,0 +1,551 @@
+-- For ifSemantic
+{-# LANGUAGE AllowAmbiguousTypes #-}
+-- For Syntax
+{-# LANGUAGE DataKinds #-}
+-- For (:!:)
+{-# LANGUAGE PatternSynonyms #-}
+-- For ifSemantic
+{-# LANGUAGE RankNTypes #-}
+-- For Permutation
+{-# LANGUAGE TypeFamilyDependencies #-}
+-- For Permutation
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | 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
+
+import Control.Category qualified as Cat
+import Data.Bool (Bool (..))
+import Data.Char (Char)
+import Data.Either (Either (..))
+import Data.Eq (Eq)
+import Data.Function qualified as Fun
+import Data.Int (Int)
+import Data.Kind (Constraint)
+import Data.Maybe (Maybe (..), fromJust)
+import Data.Proxy (Proxy (..))
+import Data.Semigroup (Semigroup)
+import Data.String (String)
+import Data.Tuple qualified as Tuple
+import GHC.Generics (Generic)
+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
+
+-- ** Type family 'Syntaxes'
+
+-- | Merge several 'Syntax'es into a single one.
+--
+-- Useful in 'IfSemantic'.
+type family Syntaxes (syns :: [Syntax]) (sem :: Semantic) :: Constraint where
+  Syntaxes '[] sem = ()
+  Syntaxes (syn ': syns) sem = (syn sem, Syntaxes syns sem)
+
+-- * Class 'Abstractable'
+class Unabstractable sem => 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)
+  default lam1 ::
+    FromDerived Abstractable sem =>
+    Derivable sem =>
+    (sem a -> sem b) ->
+    sem (a -> b)
+  default var ::
+    FromDerived1 Abstractable sem =>
+    sem a ->
+    sem a
+
+-- ** Class 'Unabstractable'
+class Unabstractable sem where
+  -- | Application, aka. unabstract.
+  (.@) :: sem (a -> b) -> sem a -> sem b
+
+  infixl 9 .@
+  (.@) = liftDerived2 (.@)
+  default (.@) ::
+    FromDerived2 Unabstractable sem =>
+    sem (a -> b) ->
+    sem a ->
+    sem b
+
+-- ** Class 'Functionable'
+class Functionable sem where
+  const :: sem (a -> b -> a)
+  flip :: sem ((a -> b -> c) -> b -> a -> c)
+  id :: sem (a -> a)
+  (.) :: sem ((b -> c) -> (a -> b) -> a -> c)
+  infixr 9 .
+  ($) :: sem ((a -> b) -> a -> b)
+  infixr 0 $
+  const = liftDerived const
+  flip = liftDerived flip
+  id = liftDerived id
+  (.) = liftDerived (.)
+  ($) = liftDerived ($)
+  default const ::
+    FromDerived Functionable sem =>
+    sem (a -> b -> a)
+  default flip ::
+    FromDerived Functionable sem =>
+    sem ((a -> b -> c) -> b -> a -> c)
+  default id ::
+    FromDerived Functionable sem =>
+    sem (a -> a)
+  default (.) ::
+    FromDerived Functionable sem =>
+    sem ((b -> c) -> (a -> b) -> a -> c)
+  default ($) ::
+    FromDerived Functionable sem =>
+    sem ((a -> b) -> a -> b)
+
+-- * Class 'Anythingable'
+class Anythingable sem where
+  anything :: sem a -> sem a
+  anything = Fun.id
+
+-- * Class 'Bottomable'
+class Bottomable sem where
+  bottom :: sem a
+
+-- * Class 'Constantable'
+class Constantable c sem where
+  constant :: c -> sem c
+  constant = liftDerived Fun.. constant
+  default constant ::
+    FromDerived (Constantable c) sem =>
+    c ->
+    sem c
+
+-- * Class 'Eitherable'
+class Eitherable sem where
+  either :: sem ((l -> a) -> (r -> a) -> Either l r -> a)
+  left :: sem (l -> Either l r)
+  right :: sem (r -> Either l r)
+  either = liftDerived either
+  left = liftDerived left
+  right = liftDerived right
+  default either ::
+    FromDerived Eitherable sem =>
+    sem ((l -> a) -> (r -> a) -> Either l r -> a)
+  default left ::
+    FromDerived Eitherable sem =>
+    sem (l -> Either l r)
+  default right ::
+    FromDerived Eitherable sem =>
+    sem (r -> Either l r)
+
+-- * Class 'Equalable'
+class Equalable sem where
+  equal :: Eq a => sem (a -> a -> Bool)
+  equal = liftDerived equal
+  default equal ::
+    FromDerived Equalable sem =>
+    Eq a =>
+    sem (a -> a -> Bool)
+
+infix 4 `equal`, ==
+(==) ::
+  Abstractable sem =>
+  Equalable sem =>
+  Eq a =>
+  sem a ->
+  sem a ->
+  sem Bool
+(==) x y = equal .@ x .@ y
+
+-- * Class 'IfThenElseable'
+class IfThenElseable sem where
+  ifThenElse :: sem Bool -> sem a -> sem a -> sem a
+  ifThenElse = liftDerived3 ifThenElse
+  default ifThenElse ::
+    FromDerived3 IfThenElseable sem =>
+    sem Bool ->
+    sem a ->
+    sem a ->
+    sem a
+
+-- * Class 'Inferable'
+class Inferable a sem where
+  infer :: sem a
+  default infer :: FromDerived (Inferable a) sem => sem a
+  infer = liftDerived infer
+
+unit :: Inferable () sem => sem ()
+unit = infer
+bool :: Inferable Bool sem => sem Bool
+bool = infer
+char :: Inferable Char sem => sem Char
+char = infer
+int :: Inferable Int sem => sem Int
+int = infer
+natural :: Inferable Natural sem => sem Natural
+natural = infer
+string :: Inferable String sem => sem String
+string = infer
+
+-- * Class 'Listable'
+class Listable sem where
+  cons :: sem (a -> [a] -> [a])
+  nil :: sem [a]
+  cons = liftDerived cons
+  nil = liftDerived nil
+  default cons ::
+    FromDerived Listable sem =>
+    sem (a -> [a] -> [a])
+  default nil ::
+    FromDerived Listable sem =>
+    sem [a]
+
+-- * Class 'Maybeable'
+class Maybeable sem where
+  nothing :: sem (Maybe a)
+  just :: sem (a -> Maybe a)
+  nothing = liftDerived nothing
+  just = liftDerived just
+  default nothing ::
+    FromDerived Maybeable sem =>
+    sem (Maybe a)
+  default just ::
+    FromDerived Maybeable sem =>
+    sem (a -> Maybe a)
+
+-- * Class 'IsoFunctor'
+class IsoFunctor sem where
+  (<%>) :: Iso a b -> sem a -> sem b
+  infixl 4 <%>
+  (<%>) iso = liftDerived1 (iso <%>)
+  default (<%>) ::
+    FromDerived1 IsoFunctor sem =>
+    Iso a b ->
+    sem a ->
+    sem b
+
+-- ** Type 'Iso'
+data Iso a b = Iso {a2b :: a -> b, b2a :: b -> a}
+instance Cat.Category Iso where
+  id = Iso Cat.id Cat.id
+  f . g = Iso (a2b f Cat.. a2b g) (b2a g Cat.. b2a f)
+
+-- * Class 'ProductFunctor'
+
+-- | Beware that this is an @infixr@,
+-- not @infixl@ like 'Control.Applicative.<*>';
+-- this is to follow what is expected by 'ADT'.
+class ProductFunctor sem where
+  (<.>) :: sem a -> sem b -> sem (a, b)
+  infixr 4 <.>
+  (<.>) = liftDerived2 (<.>)
+  default (<.>) ::
+    FromDerived2 ProductFunctor sem =>
+    sem a ->
+    sem b ->
+    sem (a, b)
+  (<.) :: sem a -> sem () -> sem a
+  infixr 4 <.
+  ra <. rb = Iso Tuple.fst (,()) <%> (ra <.> rb)
+  default (<.) :: IsoFunctor sem => sem a -> sem () -> sem a
+  (.>) :: sem () -> sem a -> sem a
+  infixr 4 .>
+  ra .> rb = Iso Tuple.snd ((),) <%> (ra <.> rb)
+  default (.>) :: IsoFunctor sem => sem () -> sem a -> sem a
+
+-- * Class 'SumFunctor'
+
+-- | Beware that this is an @infixr@,
+-- not @infixl@ like 'Control.Applicative.<|>';
+-- this is to follow what is expected by 'ADT'.
+class SumFunctor sem where
+  (<+>) :: sem a -> sem b -> sem (Either a b)
+  infixr 3 <+>
+  (<+>) = liftDerived2 (<+>)
+  default (<+>) ::
+    FromDerived2 SumFunctor sem =>
+    sem a ->
+    sem b ->
+    sem (Either a b)
+
+-- | Like @(,)@ but @infixr@.
+-- Mostly useful for clarity when using 'SumFunctor'.
+pattern (:!:) :: a -> b -> (a, b)
+pattern a :!: b <-
+  (a, b)
+  where
+    a :!: b = (a, b)
+
+infixr 4 :!:
+
+-- * Class 'AlternativeFunctor'
+
+-- | Beware that this is an @infixr@,
+-- not @infixl@ like 'Control.Applicative.<|>';
+-- this is to follow what is expected by 'ADT'.
+class AlternativeFunctor sem where
+  (<|>) :: sem a -> sem a -> sem a
+  infixr 3 <|>
+  (<|>) = liftDerived2 (<|>)
+  default (<|>) ::
+    FromDerived2 AlternativeFunctor sem =>
+    sem a ->
+    sem a ->
+    sem a
+
+-- * Class 'Dicurryable'
+class Dicurryable sem where
+  dicurry ::
+    CurryN args =>
+    proxy args ->
+    (args -..-> a) -> -- construction
+    (a -> Tuples args) -> -- destruction
+    sem (Tuples args) ->
+    sem a
+  dicurry args constr destr = liftDerived1 (dicurry args constr destr)
+  default dicurry ::
+    FromDerived1 Dicurryable sem =>
+    CurryN args =>
+    proxy args ->
+    (args -..-> a) ->
+    (a -> Tuples args) ->
+    sem (Tuples args) ->
+    sem a
+
+construct ::
+  forall args a sem.
+  Dicurryable sem =>
+  Generic a =>
+  EoTOfRep a =>
+  CurryN args =>
+  Tuples args ~ EoT (ADT a) =>
+  (args ~ Args (args -..-> a)) =>
+  (args -..-> a) ->
+  sem (Tuples args) ->
+  sem a
+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
+  data_ :: Generic a => RepOfEoT a => UnToF a => sem (EoT (ADT a)) -> sem a
+  default data_ ::
+    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 => UnToF a => sem (EoT (ADT a)) -> sem a
+dataType = data_
+
+-- * Class 'IfSemantic'
+
+-- | 'IfSemantic' enables to change the 'Syntax' for a specific 'Semantic'.
+--
+-- Useful when a 'Semantic' does not implement some 'Syntax'es used by other 'Semantic's.
+class
+  IfSemantic
+    (thenSyntaxes :: [Syntax])
+    (elseSyntaxes :: [Syntax])
+    thenSemantic
+    elseSemantic
+  where
+  ifSemantic ::
+    (Syntaxes thenSyntaxes thenSemantic => thenSemantic a) ->
+    (Syntaxes elseSyntaxes elseSemantic => elseSemantic a) ->
+    elseSemantic a
+
+instance
+  {-# OVERLAPPING #-}
+  Syntaxes thenSyntaxes thenSemantic =>
+  IfSemantic thenSyntaxes elseSyntaxes thenSemantic thenSemantic
+  where
+  ifSemantic thenSyntax _elseSyntax = thenSyntax
+instance
+  Syntaxes elseSyntaxes elseSemantic =>
+  IfSemantic thenSyntaxes elseSyntaxes thenSemantic elseSemantic
+  where
+  ifSemantic _thenSyntax elseSyntax = elseSyntax
+
+-- * Class 'Monoidable'
+class
+  ( Emptyable sem
+  , Semigroupable sem
+  ) =>
+  Monoidable sem
+instance
+  ( Emptyable sem
+  , Semigroupable sem
+  ) =>
+  Monoidable sem
+
+-- ** Class 'Emptyable'
+class Emptyable sem where
+  empty :: sem a
+  empty = liftDerived empty
+  default empty ::
+    FromDerived Emptyable sem =>
+    sem a
+
+-- ** Class 'Semigroupable'
+class Semigroupable sem where
+  concat :: Semigroup a => sem (a -> a -> a)
+  concat = liftDerived concat
+  default concat ::
+    FromDerived Semigroupable sem =>
+    Semigroup a =>
+    sem (a -> a -> a)
+
+infixr 6 `concat`, <>
+(<>) ::
+  Abstractable sem =>
+  Semigroupable sem =>
+  Semigroup a =>
+  sem a ->
+  sem a ->
+  sem a
+(<>) x y = concat .@ x .@ y
+
+-- ** Class 'Optionable'
+class Optionable sem where
+  optional :: sem a -> sem (Maybe a)
+  optional = liftDerived1 optional
+  default optional ::
+    FromDerived1 Optionable sem =>
+    sem a ->
+    sem (Maybe a)
+
+-- * Class 'Repeatable'
+class Repeatable sem where
+  many0 :: sem a -> sem [a]
+  many1 :: sem a -> sem [a]
+  many0 = liftDerived1 many0
+  many1 = liftDerived1 many1
+  default many0 ::
+    FromDerived1 Repeatable sem =>
+    sem a ->
+    sem [a]
+  default many1 ::
+    FromDerived1 Repeatable sem =>
+    sem a ->
+    sem [a]
+
+-- | Alias to 'many0'.
+many :: Repeatable sem => sem a -> sem [a]
+many = many0
+
+-- | Alias to 'many1'.
+some :: Repeatable sem => sem a -> sem [a]
+some = many1
+
+-- * Class 'Permutable'
+class Permutable sem where
+  -- Use @TypeFamilyDependencies@ to help type-inference infer @(sem)@.
+  type Permutation (sem :: Semantic) = (r :: Semantic) | r -> sem
+  type Permutation sem = Permutation (Derived sem)
+  permutable :: Permutation sem a -> sem a
+  perm :: sem a -> Permutation sem a
+  noPerm :: Permutation sem ()
+  permWithDefault :: a -> sem a -> Permutation sem a
+  optionalPerm ::
+    Eitherable sem =>
+    IsoFunctor sem =>
+    Permutable sem =>
+    sem a ->
+    Permutation sem (Maybe a)
+  optionalPerm = permWithDefault Nothing Fun.. (<%>) (Iso Just fromJust)
+
+(<&>) ::
+  Permutable sem =>
+  ProductFunctor (Permutation sem) =>
+  sem a ->
+  Permutation sem b ->
+  Permutation sem (a, b)
+x <&> y = perm x <.> y
+infixr 4 <&>
+{-# INLINE (<&>) #-}
+
+(<?&>) ::
+  Eitherable sem =>
+  IsoFunctor sem =>
+  Permutable sem =>
+  ProductFunctor (Permutation sem) =>
+  sem a ->
+  Permutation sem b ->
+  Permutation sem (Maybe a, b)
+x <?&> y = optionalPerm x <.> y
+infixr 4 <?&>
+{-# INLINE (<?&>) #-}
+
+(<*&>) ::
+  Eitherable sem =>
+  Repeatable sem =>
+  IsoFunctor sem =>
+  Permutable sem =>
+  ProductFunctor (Permutation sem) =>
+  sem a ->
+  Permutation sem b ->
+  Permutation sem ([a], b)
+x <*&> y = permWithDefault [] (many1 x) <.> y
+infixr 4 <*&>
+{-# INLINE (<*&>) #-}
+
+(<+&>) ::
+  Eitherable sem =>
+  Repeatable sem =>
+  IsoFunctor sem =>
+  Permutable sem =>
+  ProductFunctor (Permutation sem) =>
+  sem a ->
+  Permutation sem b ->
+  Permutation sem ([a], b)
+x <+&> y = perm (many1 x) <.> y
+infixr 4 <+&>
+{-# INLINE (<+&>) #-}
+
+-- * Class 'Voidable'
+class Voidable sem where
+  -- | Useful to supply @(a)@ to a @(sem)@ consuming @(a)@,
+  -- for example in the format of a printing interpreter.
+  void :: a -> sem a -> sem ()
+  void = liftDerived1 Fun.. void
+  default void ::
+    FromDerived1 Voidable sem =>
+    a ->
+    sem a ->
+    sem ()
+
+-- * Class 'Substractable'
+class Substractable sem where
+  (<->) :: sem a -> sem b -> sem a
+  infixr 3 <->
+  (<->) = liftDerived2 (<->)
+  default (<->) ::
+    FromDerived2 Substractable sem =>
+    sem a ->
+    sem b ->
+    sem a
diff --git a/src/Symantic/Syntaxes/CurryN.hs b/src/Symantic/Syntaxes/CurryN.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Syntaxes/CurryN.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+
+module Symantic.Syntaxes.CurryN where
+
+import Data.Function (($), (.))
+import Data.Kind (Type)
+
+import Symantic.Syntaxes.EithersOfTuples (Tuples)
+
+-- * Class 'CurryN'
+
+-- | Produce and consume 'Tuples'.
+-- Not actually useful for the Generic side of this module,
+-- but related through the use of 'Tuples'.
+class CurryN args where
+  -- Like 'curry' but for an arbitrary number of nested 2-tuples.
+  curryN :: (Tuples args -> res) -> args -..-> res
+
+  -- Like 'uncurry' but for an arbitrary number of nested 2-tuples.
+  uncurryN :: (args -..-> res) -> Tuples args -> res
+
+  -- Like 'fmap' on @('->')@ but for an arbitrary number of arguments.
+  mapresultN :: (a -> b) -> (args -..-> a) -> args -..-> b
+
+instance CurryN '[a] where
+  curryN = ($)
+  uncurryN = ($)
+  mapresultN = (.)
+instance CurryN (b ': as) => CurryN (a ': b ': as) where
+  curryN f x = curryN @(b ': as) (\xs -> f (x, xs))
+  uncurryN f (x, xs) = uncurryN @(b ': as) (f x) xs
+  mapresultN f as2r = mapresultN @(b ': as) f . as2r
+
+-- ** Type family ('-..->')
+type family (args :: [Type]) -..-> (r :: Type) :: Type where
+  '[] -..-> r = r
+  (a : args) -..-> r = a -> args -..-> r
+
+-- ** Type family 'Args'
+type family Args (f :: Type) :: [Type] where
+  Args (a -> r) = a : Args r
+  Args r = '[]
+
+-- ** Type family 'Result'
+type family Result (as :: Type) :: Type where
+  Result (a -> r) = Result r
+  Result r = r
diff --git a/src/Symantic/Syntaxes/Data.hs b/src/Symantic/Syntaxes/Data.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Syntaxes/Data.hs
@@ -0,0 +1,289 @@
+{-# LANGUAGE ConstraintKinds #-}
+-- For Semantic
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module Symantic.Syntaxes.Data where
+
+import Data.Bool (Bool)
+import Data.Either (Either)
+import Data.Eq qualified as Eq
+import Data.Function qualified as Fun
+import Data.Maybe (Maybe)
+import Data.Maybe qualified as Maybe
+import Data.Semigroup (Semigroup)
+import Type.Reflection (Typeable, eqTypeRep, typeRep, (:~~:) (..))
+
+import Symantic.Syntaxes.Classes
+import Symantic.Syntaxes.Derive
+
+-- * Type 'SomeData'
+data SomeData sem a
+  = forall able.
+    ( Derivable (Data able sem)
+    , Typeable able
+    ) =>
+    SomeData (Data able sem a)
+
+type instance Derived (SomeData sem) = sem
+instance Derivable (SomeData sem) where
+  derive (SomeData x) = derive x
+
+-- ** Type 'Data'
+
+-- TODO: neither data families nor data instances
+-- can have phantom roles with GHC-9's RoleAnnotations,
+-- 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
+
+-- | Convenient utility to pattern-match a 'SomeData'.
+pattern Data :: Typeable able => Data able 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 ::
+  forall able sem a.
+  Typeable able =>
+  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.Nothing -> Maybe.Nothing
+
+-- 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
+  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
+  lam f = SomeData (Lam f)
+  lam1 f = SomeData (Lam1 f)
+  var = Fun.id
+
+-- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
+-- but to avoid duplication of work, only those manually marked
+-- as using their variable at most once.
+--
+-- DOC: Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2001,
+-- https://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf
+normalOrderReduction ::
+  forall sem a.
+  Abstractable sem =>
+  IfThenElseable sem =>
+  SomeData sem a ->
+  SomeData sem a
+normalOrderReduction = nor
+  where
+    nor :: SomeData sem b -> SomeData sem b
+    nor = \case
+      Data (Lam f) -> lam (nor Fun.. f)
+      Data (Lam1 f) -> lam1 (nor Fun.. f)
+      Data (x :@ y) -> case whnf x of
+        Data (Lam1 f) -> nor (f y)
+        x' -> nor x' .@ nor y
+      Data (IfThenElse test ok ko) ->
+        case nor test of
+          Data (Constant b :: Data (Constantable Bool) sem Bool) ->
+            if b then nor ok else nor ko
+          t -> ifThenElse (nor t) (nor ok) (nor ko)
+      x -> x
+
+    whnf :: SomeData sem b -> SomeData sem b
+    whnf = \case
+      Data (x :@ y) -> case whnf x of
+        Data (Lam1 f) -> whnf (f y)
+        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
+  derive = \case
+    f :@ x -> derive f .@ derive x
+instance Unabstractable sem => Unabstractable (SomeData sem) where
+  f .@ x = SomeData (f :@ x)
+
+-- Functionable
+instance
+  ( Abstractable 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)
+
+-- Anythingable
+data instance Data Anythingable sem a where
+  Anything :: sem a -> Data Anythingable sem a
+instance
+  ( Anythingable sem
+  ) =>
+  Derivable (Data Anythingable sem)
+  where
+  derive = \case
+    Anything x -> anything x
+instance Anythingable (SomeData sem)
+instance Anythingable (Data Anythingable sem)
+
+-- Bottomable
+data instance Data Bottomable sem a where
+  Bottom :: Data Bottomable sem a
+instance Bottomable sem => Derivable (Data Bottomable sem) where
+  derive Bottom{} = bottom
+
+-- Constantable
+data instance Data (Constantable c) sem a where
+  Constant {-Typeable c =>-} :: c -> Data (Constantable c) sem c
+instance Constantable c sem => Derivable (Data (Constantable c) sem) where
+  derive = \case
+    Constant x -> constant x
+instance
+  ( Constantable c sem
+  , Typeable c
+  ) =>
+  Constantable c (SomeData sem)
+  where
+  constant c = SomeData (Constant c)
+instance{-Typeable c =>-} Constantable c (Data (Constantable c) sem) where
+  constant = Constant
+
+-- Eitherable
+data instance Data Eitherable sem a where
+  Either :: Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
+  Left :: Data Eitherable sem (l -> Either l r)
+  Right :: Data Eitherable sem (r -> Either l r)
+instance Eitherable sem => Derivable (Data Eitherable sem) where
+  derive = \case
+    Either -> either
+    Left -> left
+    Right -> right
+instance Eitherable sem => Eitherable (SomeData sem) where
+  either = SomeData Either
+  left = SomeData Left
+  right = SomeData Right
+instance Eitherable (Data Eitherable sem) where
+  either = Either
+  left = Left
+  right = Right
+
+-- Equalable
+data instance Data Equalable sem a where
+  Equal :: Eq.Eq a => Data Equalable sem (a -> a -> Bool)
+instance Equalable sem => Derivable (Data Equalable sem) where
+  derive = \case
+    Equal -> equal
+instance
+  ( Equalable sem
+  ) =>
+  Equalable (SomeData sem)
+  where
+  equal = SomeData Equal
+instance Equalable (Data Equalable sem) where
+  equal = Equal
+
+-- Emptyable
+data instance Data Emptyable sem a where
+  Empty :: Data Emptyable sem a
+instance Emptyable sem => Derivable (Data Emptyable sem) where
+  derive = \case
+    Empty -> empty
+instance
+  ( Emptyable sem
+  ) =>
+  Emptyable (SomeData sem)
+  where
+  empty = SomeData Empty
+instance Emptyable (Data Emptyable sem) where
+  empty = Empty
+
+-- Semigroupable
+data instance Data Semigroupable sem a where
+  Concat :: Semigroup a => Data Semigroupable sem (a -> a -> a)
+infixr 4 `Concat`
+instance Semigroupable sem => Derivable (Data Semigroupable sem) where
+  derive = \case
+    Concat -> concat
+instance
+  ( Semigroupable sem
+  ) =>
+  Semigroupable (SomeData sem)
+  where
+  concat = SomeData Concat
+instance Semigroupable (Data Semigroupable sem) where
+  concat = Concat
+
+-- IfThenElseable
+data instance Data IfThenElseable sem a where
+  IfThenElse ::
+    SomeData sem Bool ->
+    SomeData sem a ->
+    SomeData sem a ->
+    Data IfThenElseable sem a
+instance IfThenElseable sem => Derivable (Data IfThenElseable sem) where
+  derive = \case
+    IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
+instance
+  ( IfThenElseable sem
+  ) =>
+  IfThenElseable (SomeData sem)
+  where
+  ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
+instance IfThenElseable sem => IfThenElseable (Data IfThenElseable sem) where
+  ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
+
+-- Listable
+data instance Data Listable sem a where
+  Cons :: Data Listable sem (a -> [a] -> [a])
+  Nil :: Data Listable sem [a]
+infixr 4 `Cons`
+instance Listable sem => Derivable (Data Listable sem) where
+  derive = \case
+    Cons -> cons
+    Nil -> nil
+instance
+  ( Listable sem
+  ) =>
+  Listable (SomeData sem)
+  where
+  cons = SomeData Cons
+  nil = SomeData Nil
+instance Listable (Data Listable sem) where
+  cons = Cons
+  nil = Nil
+
+-- Maybeable
+data instance Data Maybeable sem a where
+  Nothing :: Data Maybeable sem (Maybe a)
+  Just :: Data Maybeable sem (a -> Maybe a)
+instance Maybeable sem => Derivable (Data Maybeable sem) where
+  derive = \case
+    Nothing -> nothing
+    Just -> just
+instance
+  ( Maybeable sem
+  ) =>
+  Maybeable (SomeData sem)
+  where
+  nothing = SomeData Nothing
+  just = SomeData Just
+instance Maybeable (Data Maybeable sem) where
+  nothing = Nothing
+  just = Just
diff --git a/src/Symantic/Syntaxes/Derive.hs b/src/Symantic/Syntaxes/Derive.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Syntaxes/Derive.hs
@@ -0,0 +1,133 @@
+-- For type class synonyms
+{-# LANGUAGE ConstraintKinds #-}
+-- For Semantic
+{-# LANGUAGE DataKinds #-}
+-- For adding LiftDerived* constraints
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+
+module Symantic.Syntaxes.Derive where
+
+import Data.Function ((.))
+import Data.Kind (Type)
+
+-- * Type 'Semantic'
+
+-- | The kind of @sem@(antics) throughout this library.
+type Semantic = Type -> Type
+
+-- * Type family 'Derived'
+
+-- | The next 'Semantic' that @(sem)@ derives to.
+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,
+-- but also when going back from an initial encoding to a final one.
+--
+-- Note that 'derive' and 'liftDerived' are not necessarily reciprocical functions.
+class Derivable sem where
+  derive :: sem a -> Derived sem a
+
+-- * Class 'LiftDerived'
+
+-- | Lift the 'Derived' interpreter of an interpreter, to that interpreter.
+-- This is mostly useful to give default values to class methods
+-- in order to skip their definition for interpreters
+-- where 'liftDerived' can already apply the right semantic.
+--
+-- Note that 'derive' and 'liftDerived' are not necessarily reciprocical functions.
+class LiftDerived sem where
+  liftDerived :: Derived sem a -> sem a
+
+-- * Class 'LiftDerived1'
+
+-- | Convenient wrapper of 'derive' and 'liftDerived' for functions with a single argument.
+class LiftDerived1 sem where
+  liftDerived1 ::
+    (Derived sem a -> Derived sem b) ->
+    sem a ->
+    sem b
+  liftDerived1 f = liftDerived . f . derive
+  default liftDerived1 ::
+    LiftDerived sem =>
+    Derivable sem =>
+    (Derived sem a -> Derived sem b) ->
+    sem a ->
+    sem b
+
+-- * Class 'LiftDerived2'
+
+-- | Convenient wrapper of 'derive' and 'liftDerived' for functions with two arguments.
+-- Note that the default instance relies upon 'LiftDerived', not 'LiftDerived1'.
+class LiftDerived2 sem where
+  liftDerived2 ::
+    (Derived sem a -> Derived sem b -> Derived sem c) ->
+    sem a ->
+    sem b ->
+    sem c
+  liftDerived2 f a b = liftDerived (f (derive a) (derive b))
+  default liftDerived2 ::
+    LiftDerived sem =>
+    Derivable sem =>
+    (Derived sem a -> Derived sem b -> Derived sem c) ->
+    sem a ->
+    sem b ->
+    sem c
+
+-- * Class 'LiftDerived3'
+
+-- | Convenient wrapper of 'derive' and 'liftDerived' for functions with three arguments.
+-- Note that the default instance relies upon 'LiftDerived', not 'LiftDerived2'.
+class LiftDerived3 sem where
+  liftDerived3 ::
+    (Derived sem a -> Derived sem b -> Derived sem c -> Derived sem d) ->
+    sem a ->
+    sem b ->
+    sem c ->
+    sem d
+  liftDerived3 f a b c = liftDerived (f (derive a) (derive b) (derive c))
+  default liftDerived3 ::
+    LiftDerived sem =>
+    Derivable sem =>
+    (Derived sem a -> Derived sem b -> Derived sem c -> Derived sem d) ->
+    sem a ->
+    sem b ->
+    sem c ->
+    sem d
+
+-- * Class 'LiftDerived4'
+
+-- | Convenient wrapper of 'derive' and 'liftDerived' for functions with three arguments.
+-- Note that the default instance relies upon 'LiftDerived', not 'LiftDerived3'.
+class LiftDerived4 sem where
+  liftDerived4 ::
+    (Derived sem a -> Derived sem b -> Derived sem c -> Derived sem d -> Derived sem e) ->
+    sem a ->
+    sem b ->
+    sem c ->
+    sem d ->
+    sem e
+  liftDerived4 f a b c d = liftDerived (f (derive a) (derive b) (derive c) (derive d))
+  default liftDerived4 ::
+    LiftDerived sem =>
+    Derivable sem =>
+    (Derived sem a -> Derived sem b -> Derived sem c -> Derived sem d -> Derived sem e) ->
+    sem a ->
+    sem b ->
+    sem c ->
+    sem d ->
+    sem e
+
+-- * Type synonyms @FromDerived*@
+
+-- | Convenient type synonym for using 'liftDerived' on 'Syntax' @(syn)@.
+type FromDerived syn sem = (LiftDerived sem, syn (Derived sem))
+
+type FromDerived1 syn sem = (LiftDerived1 sem, syn (Derived sem))
+type FromDerived2 syn sem = (LiftDerived2 sem, syn (Derived sem))
+type FromDerived3 syn sem = (LiftDerived3 sem, syn (Derived sem))
+type FromDerived4 syn sem = (LiftDerived4 sem, syn (Derived sem))
diff --git a/src/Symantic/Syntaxes/EithersOfTuples.hs b/src/Symantic/Syntaxes/EithersOfTuples.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Syntaxes/EithersOfTuples.hs
@@ -0,0 +1,220 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | EOT (Either of Tuples) to/from ADT (Algebraic Data Type).
+-- to produce or consume custom ADT with @('<.>')@ and @('<+>')@.
+--
+-- 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@.
+module Symantic.Syntaxes.EithersOfTuples where
+
+import Data.Either (Either (..))
+import Data.Function (const, id, ($), (.))
+import Data.Kind (Type)
+import Data.Void (Void, absurd)
+import GHC.Generics as Generics
+
+-- * Type family 'EoT'
+
+-- Return an 'Either' of 'Tuples' from the given 'ADT',
+-- matching the nesting occuring when using @('<.>')@ and ('<+>')@
+-- and their associativity and precedence,
+-- with no parenthesis messing around.
+type family EoT (adt :: [[Type]]) :: Type where
+-- This is 'absurd'
+  EoT '[] = Void
+-- There Is No Alternative
+  EoT '[ps] = Tuples ps
+-- The right associativity of @('<+>')@
+-- puts leaves on 'Left' and nodes on 'Right'
+  EoT (ps ': ss) = Either (Tuples ps) (EoT ss)
+
+-- * Type family 'Tuples'
+
+-- | Return the type of 'snd'-nested 2-tuples
+-- from the given list of types.
+type family Tuples (as :: [Type]) :: (r :: Type) where
+  Tuples '[] = ()
+  Tuples '[a] = a
+  Tuples (a ': rest) = (a, Tuples rest)
+
+-- * Type 'ADT'
+
+-- | Normalized type-level representation of an Algebraic Data Type.
+type ADT (adt :: Type) = ListOfRepSums (Rep adt) '[]
+
+-- ** Type family 'ListOfRepSums'
+
+-- | Collect the alternatives in a continuation passing-style.
+type family ListOfRepSums (a :: Type -> Type) (ss :: [[Type]]) :: [[Type]]
+
+type instance ListOfRepSums (a :+: b) ss = ListOfRepSums a (ListOfRepSums b ss)
+
+-- | Meta-information for datatypes
+type instance ListOfRepSums (M1 D _c a) ss = ListOfRepSums a ss
+
+-- | Meta-information for constructors
+type instance ListOfRepSums (M1 C _c a) ss = ListOfRepProducts a '[] ': ss
+
+-- | Empty datatypes
+type instance ListOfRepSums V1 ss = ss
+
+-- ** Type family 'ListOfRepProducts'
+
+-- | Collect the records in a continuation passing-style.
+type family ListOfRepProducts (a :: Type -> Type) (ps :: [Type]) :: [Type]
+
+type instance ListOfRepProducts (a :*: b) ps = ListOfRepProducts a (ListOfRepProducts b ps)
+
+-- | Meta-information for record selectors
+type instance ListOfRepProducts (M1 S _c a) ps = TypeOfRepField a ': ps
+
+-- | Constructor without fields
+type instance ListOfRepProducts U1 ps = ps
+
+-- ** Type family 'TypeOfRepField'
+type family TypeOfRepField (a :: Type -> Type) :: Type
+type instance TypeOfRepField (K1 _i a) = a
+
+-- * Class 'RepOfEoT'
+type RepOfEoT a = RepOfEithers (Rep a) '[]
+
+-- | Morph the 'Either' of 'Tuples' corresponding to an 'ADT'
+-- into a constructor of this 'ADT'.
+-- This is the reverse of 'eotOfadt'.
+adtOfeot :: Generic a => RepOfEoT a => EoT (ADT a) -> a
+adtOfeot eot = Generics.to $ repOfEithers @_ @'[] eot id absurd
+
+-- ** Class 'RepOfEithers'
+class RepOfEithers (a :: Type -> Type) ss where
+  -- | Parse the 'Either' (list-like) binary tree of 'EoT'
+  -- into the @(':+:')@ (balanced) binary tree of 'Rep',
+  -- using continuation passing-style for performance.
+  repOfEithers ::
+    EoT (ListOfRepSums a ss) ->
+    -- the 'a' 'Rep' is the current alternative in the 'EoT'
+    (a x -> r) ->
+    -- the 'a' 'Rep' is a following alternative in the 'EoT'
+    (EoT ss -> r) ->
+    r
+instance (RepOfEithers a (ListOfRepSums b ss), RepOfEithers b ss) => RepOfEithers (a :+: b) ss where
+  repOfEithers eot ok ko =
+    -- try to parse 'a' on the current 'eot'
+    repOfEithers @a @(ListOfRepSums b ss)
+      eot
+      (ok . L1)
+      ( \next ->
+          -- parsing 'a' failed
+          -- try to parse 'b' on the 'Right' of the current 'eot'
+          repOfEithers @b @ss
+            next
+            (ok . R1)
+            ko -- parsing 'b' failed: backtrack
+      )
+instance RepOfEithers a ss => RepOfEithers (M1 D c a) ss where
+  repOfEithers eot ok = repOfEithers @a @ss eot (ok . M1)
+instance RepOfTuples a '[] => RepOfEithers (M1 C c a) (ps ': ss) where
+  repOfEithers eot ok ko =
+    case eot of
+      -- 'EoT' is a leaf, and 'Rep' too: parsing succeeds
+      Left ts -> ok $ M1 $ repOfTuples @a @'[] ts const
+      -- 'EoT' is a node, but 'Rep' is a leaf: parsing fails
+      Right ss -> ko ss
+instance RepOfTuples a '[] => RepOfEithers (M1 C c a) '[] where
+  repOfEithers eot ok _ko = ok $ M1 $ repOfTuples @_ @'[] eot const
+instance RepOfEithers V1 ss where
+  repOfEithers eot _ok ko = ko eot
+
+-- ** Class 'RepOfTuples'
+class RepOfTuples (a :: Type -> Type) (xs :: [Type]) where
+  -- | Parse the 'Tuples' (list-like) binary tree of 'EoT'
+  -- into the @(':*:')@ (balanced) binary tree of 'Rep',
+  -- using continuation passing-style for performance.
+  repOfTuples ::
+    Tuples (ListOfRepProducts a xs) ->
+    (a x -> Tuples xs -> r) ->
+    r
+instance (RepOfTuples a (ListOfRepProducts b ps), RepOfTuples b ps) => RepOfTuples (a :*: b) ps where
+  repOfTuples ts k =
+    -- uncons 'a'
+    repOfTuples @a @(ListOfRepProducts b ps)
+      ts
+      ( \a ts' ->
+          -- uncons 'b'
+          repOfTuples @b @ps
+            ts'
+            (\b -> k (a :*: b))
+      )
+instance RepOfField a => RepOfTuples (M1 S c a) (p ': ps) where
+  repOfTuples (a, ts) k = k (M1 (repOfField a)) ts
+instance RepOfField a => RepOfTuples (M1 S c a) '[] where
+  repOfTuples a k = k (M1 (repOfField a)) ()
+instance RepOfTuples U1 ps where
+  repOfTuples ts k = k U1 ts
+
+-- ** Class 'RepOfField'
+class RepOfField (a :: Type -> Type) where
+  repOfField :: TypeOfRepField a -> a x
+instance RepOfField (K1 i a) where
+  repOfField = K1
+
+-- * Class 'EoTOfRep'
+type EoTOfRep a = EithersOfRep (Rep a) '[]
+
+-- | Morph the constructor of an 'ADT'
+-- into the corresponding 'Either' of 'Tuples' of this 'ADT'.
+-- This is the reverse of 'adtOfeot'.
+eotOfadt :: Generic a => EoTOfRep a => a -> EoT (ADT a)
+eotOfadt = eithersOfRepL @_ @'[] . Generics.from
+
+-- ** Class 'EithersOfRep'
+class EithersOfRep (a :: Type -> Type) ss where
+  eithersOfRepL :: a x -> EoT (ListOfRepSums a ss)
+  eithersOfRepR :: EoT ss -> EoT (ListOfRepSums a ss)
+instance
+  (EithersOfRep a (ListOfRepSums b ss), EithersOfRep b ss) =>
+  EithersOfRep (a :+: b) ss
+  where
+  eithersOfRepL = \case
+    L1 a -> eithersOfRepL @a @(ListOfRepSums b ss) a
+    R1 b -> eithersOfRepR @a @(ListOfRepSums b ss) (eithersOfRepL @b @ss b)
+  eithersOfRepR ss = eithersOfRepR @a @(ListOfRepSums b ss) (eithersOfRepR @b @ss ss)
+instance EithersOfRep a ss => EithersOfRep (M1 D c a) ss where
+  eithersOfRepL (M1 a) = eithersOfRepL @a @ss a
+  eithersOfRepR = eithersOfRepR @a @ss
+instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) '[] where
+  eithersOfRepL (M1 a) = tuplesOfRep @_ @'[] a ()
+  eithersOfRepR = absurd
+instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) (ps ': ss) where
+  eithersOfRepL (M1 a) = Left $ tuplesOfRep @_ @'[] a ()
+  eithersOfRepR = Right
+instance EithersOfRep V1 ss where
+  eithersOfRepL = \case {}
+  eithersOfRepR = id
+
+-- ** Class 'TuplesOfRep'
+class TuplesOfRep (a :: Type -> Type) (ps :: [Type]) where
+  tuplesOfRep :: a x -> Tuples ps -> Tuples (ListOfRepProducts a ps)
+instance (TuplesOfRep a (ListOfRepProducts b ps), TuplesOfRep b ps) => TuplesOfRep (a :*: b) ps where
+  tuplesOfRep (a :*: b) ps =
+    tuplesOfRep @a @(ListOfRepProducts b ps)
+      a
+      (tuplesOfRep @b @ps b ps)
+instance TuplesOfRep U1 ps where
+  tuplesOfRep U1 xs = xs
+instance FieldOfRep a => TuplesOfRep (M1 S c a) (x ': ps) where
+  tuplesOfRep (M1 a) xs = (fieldOfRep a, xs)
+instance FieldOfRep a => TuplesOfRep (M1 S c a) '[] where
+  tuplesOfRep (M1 a) _xs = fieldOfRep a
+
+-- ** Class 'FieldOfRep'
+class FieldOfRep (a :: Type -> Type) where
+  fieldOfRep :: a x -> TypeOfRepField a
+instance FieldOfRep (K1 i a) where
+  fieldOfRep (K1 a) = a
diff --git a/src/Symantic/Syntaxes/Reify.hs b/src/Symantic/Syntaxes/Reify.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Syntaxes/Reify.hs
@@ -0,0 +1,73 @@
+-- For reifyTH
+{-# LANGUAGE TemplateHaskell #-}
+{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
+
+-- | Reify an Haskell value using type-directed normalisation-by-evaluation (NBE).
+module Symantic.Syntaxes.Reify where
+
+import Control.Monad (Monad (..))
+import Data.Function qualified as Fun
+import Language.Haskell.TH qualified as TH
+
+import Symantic.Syntaxes.Classes (Abstractable (..), Unabstractable (..))
+
+-- | 'ReifyReflect' witnesses the duality between @meta@ and @(repr a)@.
+--  It indicates which type variables in @a@ are not to be instantiated
+--  with the arrow type, and instantiates them to @(repr _)@ in @meta@.
+--  This is directly taken from: http://okmij.org/ftp/tagless-final/course/TDPE.hs
+--
+-- * @meta@ instantiates polymorphic types of the original Haskell expression
+--   with @(repr _)@ types, according to how 'ReifyReflect' is constructed
+--   using 'base' and @('-->')@. This is obviously not possible
+--   if the orignal expression uses monomorphic types (like 'Int'),
+--   but remains possible with constrained polymorphic types (like @(Num i => i)@),
+--   because @(i)@ can still be inferred to @(repr _)@,
+--   whereas the finally chosen @(repr)@
+--   (eg. 'E', or 'Identity', or 'TH.CodeQ', or ...)
+--   can have a 'Num' instance.
+-- * @(repr a)@ is the symantic type as it would have been,
+--   had the expression been written with explicit 'lam's
+--   instead of bare haskell functions.
+-- DOC: http://okmij.org/ftp/tagless-final/cookbook.html#TDPE
+-- 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
+  }
+
+-- | The base of induction : placeholder for a type which is not the arrow type.
+base :: ReifyReflect repr (repr a) a
+base = ReifyReflect{reify = Fun.id, reflect = Fun.id}
+
+-- | The inductive case : the arrow type.
+infixr 8 -->
+
+(-->) ::
+  Abstractable repr =>
+  ReifyReflect repr m1 o1 ->
+  ReifyReflect repr m2 o2 ->
+  ReifyReflect repr (m1 -> m2) (o1 -> o2)
+r1 --> r2 =
+  ReifyReflect
+    { reify = \meta -> lam (reify r2 Fun.. meta Fun.. reflect r1)
+    , reflect = \repr -> reflect r2 Fun.. (.@) repr Fun.. reify r1
+    }
+
+-- * Using TemplateHaskell to fully auto-generate 'ReifyReflect'
+
+-- | @$(reifyTH 'Foo.bar)@ calls 'reify' on 'Foo.bar'
+-- with an 'ReifyReflect' generated from the infered type of 'Foo.bar'.
+reifyTH :: TH.Name -> TH.Q TH.Exp
+reifyTH name = do
+  info <- TH.reify name
+  case info of
+    TH.VarI n (TH.ForallT _vs _ctx ty) _dec ->
+      [|reify $(genReifyReflect ty) $(return (TH.VarE n))|]
+  where
+    genReifyReflect (TH.AppT (TH.AppT TH.ArrowT a) b) = [|$(genReifyReflect a) --> $(genReifyReflect b)|]
+    genReifyReflect TH.VarT{} = [|base|]
diff --git a/src/Symantic/Syntaxes/TuplesOfFunctions.hs b/src/Symantic/Syntaxes/TuplesOfFunctions.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Syntaxes/TuplesOfFunctions.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Tuples-of-Functions
+module Symantic.Syntaxes.TuplesOfFunctions where
+
+import Data.Bool (Bool (..))
+import Data.Either (Either (..))
+import Data.Function qualified as Fun
+import Data.Kind (Type)
+import Type.Reflection ((:~:) (..))
+
+-- * Type 'ToF'
+type ToF a next = ToFIf (IsToF a) a next
+
+-- ** Type 'ToFIf'
+
+-- | 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.
+  ToFIf 'True () next = next
+-- Enable a different return value for each function.
+  ToFIf 'True (Endpoint end a) next = (next :~: end, a)
+-- Everything else becomes a new argument.
+  ToFIf 'False a next = a -> next
+
+-- ** Type 'IsToF'
+
+-- | This 'Bool' is added to 'ToFIf' to avoid overlapping instances.
+type family IsToF a :: Bool where
+  IsToF () = 'True
+  IsToF (a, b) = 'True
+  IsToF (Either l r) = 'True
+  IsToF (Endpoint end a) = 'True
+  IsToF a = 'False
+
+-- ** Type 'Endpoint'
+newtype Endpoint end a = Endpoint {unEndpoint :: a}
+
+endpoint :: a -> ToF (Endpoint end a) end
+endpoint = (Refl,)
+
+-- * Type 'UnToF'
+type UnToF a = UnToFIf (IsToF a) a
+
+-- * 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
diff --git a/src/Symantic/Viewer.hs b/src/Symantic/Viewer.hs
deleted file mode 100644
--- a/src/Symantic/Viewer.hs
+++ /dev/null
@@ -1,107 +0,0 @@
-{-# LANGUAGE GADTs #-} -- For Viewer
-{-# LANGUAGE OverloadedStrings #-} -- For convenience
-{-# LANGUAGE UndecidableInstances #-} -- For Show (SomeData a)
-module Symantic.Viewer where
-
-import Data.Int (Int)
-import Data.String
-import Text.Show
-import qualified Data.Function as Fun
-import qualified Prelude
-
-import Symantic.Classes
-import Symantic.Data
-import Symantic.Derive
-import Symantic.Fixity
-
-data Viewer a where
-  Viewer :: (ViewerEnv -> ShowS) -> Viewer a
-  ViewerUnifix :: Unifix -> String -> String -> Viewer (a -> b)
-  ViewerInfix :: Infix -> String -> String -> Viewer (a -> b -> c)
-  ViewerApp :: Viewer (b -> a) -> Viewer b -> Viewer a
-
-runViewer :: Viewer a -> ViewerEnv -> ShowS
-runViewer (Viewer v) env = v env
-runViewer (ViewerInfix _op name _infixName) _env = showString name
-runViewer (ViewerUnifix _op name _unifixName) _env = showString name
-runViewer (ViewerApp f x) env =
-  pairViewer env op Fun.$
-    runViewer f env{viewEnv_op = (op, SideL) } Fun..
-    showString " " Fun..
-    runViewer x env{viewEnv_op = (op, SideR) }
-  where op = infixN 10
-
--- | Unusual, but enables to leverage default definition of methods.
-type instance Derived Viewer = Viewer
-instance LiftDerived Viewer where
-  liftDerived = Fun.id
-
-instance IsString (Viewer a) where
-  fromString s = Viewer Fun.$ \_env -> showString s
-instance Show (Viewer a) where
-  showsPrec p = (`runViewer` ViewerEnv
-    { viewEnv_op = (infixN p, SideL)
-    , viewEnv_pair = pairParen
-    , viewEnv_lamDepth = 1
-    })
-instance Show (SomeData Viewer a) where
-  showsPrec p (SomeData x) = showsPrec p (derive x :: Viewer a)
-
-data ViewerEnv
-  = ViewerEnv
-  { viewEnv_op :: (Infix, Side)
-  , viewEnv_pair :: Pair
-  , viewEnv_lamDepth :: Int
-  }
-
-pairViewer :: ViewerEnv -> Infix -> ShowS -> ShowS
-pairViewer env op s =
-  if isPairNeeded (viewEnv_op env) op
-  then showString o Fun.. s Fun.. showString c
-  else s
-  where (o,c) = viewEnv_pair env
-
-instance Abstractable Viewer where
-  var = Fun.id
-  lam f = viewLam "x" f
-  lam1 f = viewLam "u" f
-  ViewerInfix op _name infixName .@ ViewerApp x y = Viewer Fun.$ \env ->
-    pairViewer env op Fun.$
-      runViewer x env{viewEnv_op=(op, SideL)} Fun..
-      showString " " Fun.. showString infixName Fun.. showString " " Fun..
-      runViewer y env{viewEnv_op=(op, SideR)}
-  ViewerInfix op name _infixName .@ x = Viewer Fun.$ \env ->
-    showParen Prelude.True Fun.$
-      runViewer x env{viewEnv_op=(op, SideL)} Fun..
-      showString " " Fun.. showString name
-  f .@ x = ViewerApp f x
-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)
-      }
-    -- . showString ")"
-  where
-  op = infixN 0
-instance Anythingable Viewer
-instance Bottomable Viewer where
-  bottom = "<hidden>"
-instance Show c => Constantable c Viewer where
-  constant c = Viewer Fun.$ \_env -> shows c
-instance Eitherable Viewer where
-  left = "Left"
-  right = "Right"
-instance Equalable Viewer where
-  equal = ViewerInfix (infixN 4) "(==)" "=="
-instance Listable Viewer where
-  cons = ViewerInfix (infixR 5) "(:)" ":"
-  nil = "[]"
-instance Maybeable Viewer where
-  nothing = "Nothing"
-  just = "Just"
diff --git a/symantic-base.cabal b/symantic-base.cabal
--- a/symantic-base.cabal
+++ b/symantic-base.cabal
@@ -1,110 +1,129 @@
-cabal-version: 3.0
-name: symantic-base
-maintainer: mailto:~julm/symantic-base@todo.code.sourcephile.fr
-bug-reports: https://todo.code.sourcephile.fr/~julm/symantic-base
-homepage: https://git.code.sourcephile.fr/~julm/symantic-base
-author: Julien Moutinho <julm+symantic-base@sourcephile.fr>
-copyright: Julien Moutinho <julm+symantic-base@sourcephile.fr>
-license: AGPL-3.0-or-later
-license-file: LICENSES/AGPL-3.0-or-later.txt
+cabal-version:      3.0
+name:               symantic-base
+maintainer:         mailto:symantic-base@sourcephile.fr
+bug-reports:        https://mails.sourcephile.fr/inbox/symantic-base
+homepage:           https://git.sourcephile.fr/haskell/symantic-base
+author:             Julien Moutinho <julm+symantic-base@sourcephile.fr>
+copyright:          Julien Moutinho <julm+symantic-base@sourcephile.fr>
+license:            AGPL-3.0-or-later
+license-file:       LICENSES/AGPL-3.0-or-later.txt
+
 -- PVP:  +-+------- breaking API changes
 --       | | +----- non-breaking API additions
 --       | | | +--- code changes with no API change
-version: 0.4.0.20211106
-stability: experimental
-category: Data Structures
-synopsis: Basic symantic combinators for Embedded Domain-Specific Languages (EDSL)
+version:            0.5.0.20221211
+stability:          experimental
+category:           Data Structures
+synopsis:
+  Basic symantic combinators for Embedded Domain-Specific Languages (EDSL)
+
 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.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@
+  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).
 
-  * @Symantic.Classes@
-    gathers commonly used tagless-final combinators
-    (the syntax part of symantics).
-  * @Symantic.Data@ interprets combinators as data constructors
-    enabling to pattern-match on combinators while keeping their extensibility.
-  * @Symantic.Derive@
-     to give a default value to combinators which avoids boilerplate code
-    when implementing combinators for an interpreter is factorizable.
-  * @Symantic.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.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).
-  * @Symantic.Viewer@
-    interprets combinators as human-readable text.
-  * @Symantic.ADT@
-    enables to derive reciprocal functions between
-    algebraic data type constructors and @Either@s of tuples.
-  * @Symantic.CurryN@
-    gathers utilities for currying or uncurrying tuples
-    of size greater or equal to two.
-  * @Symantic.Fixity@
-    gathers utilities for parsing or viewing
-    infix, prefix and postfix combinators.
-build-type: Simple
-tested-with: GHC==8.10.4
-extra-doc-files:
-  ChangeLog.md
+build-type:         Simple
+tested-with:        GHC ==8.10.4
+extra-doc-files:    ChangeLog.md
 extra-source-files:
-  cabal.project
   .envrc
+  cabal.project
   flake.lock
   flake.nix
   Makefile
+
 extra-tmp-files:
 
 source-repository head
-  type: git
-  location: https://git.code.sourcephile.fr/~julm/symantic-base
+  type:     git
+  location: git://git.sourcephile.fr/haskell/symantic-base
 
 library
-  hs-source-dirs: src
+  hs-source-dirs:     src
   exposed-modules:
     Symantic
-    Symantic.ADT
-    Symantic.Classes
-    Symantic.CurryN
-    Symantic.Data
-    Symantic.Derive
-    Symantic.Fixity
-    Symantic.Optimize
-    Symantic.Reify
-    Symantic.SharingObserver
-    Symantic.Viewer
-  default-language: Haskell2010
+    Symantic.Semantics
+    Symantic.Semantics.Reader
+    Symantic.Semantics.SharingObserver
+    Symantic.Semantics.ToFer
+    Symantic.Semantics.Viewer
+    Symantic.Semantics.Viewer.Fixity
+    Symantic.Syntaxes
+    Symantic.Syntaxes.Classes
+    Symantic.Syntaxes.CurryN
+    Symantic.Syntaxes.Data
+    Symantic.Syntaxes.Derive
+    Symantic.Syntaxes.EithersOfTuples
+    Symantic.Syntaxes.Reify
+    Symantic.Syntaxes.TuplesOfFunctions
+
+  default-language:   Haskell2010
   default-extensions:
+    NoImplicitPrelude
     DefaultSignatures
     FlexibleContexts
     FlexibleInstances
     GeneralizedNewtypeDeriving
+    ImportQualifiedPost
     LambdaCase
     MultiParamTypeClasses
     NamedFieldPuns
-    NoImplicitPrelude
     RecordWildCards
     ScopedTypeVariables
     TupleSections
     TypeApplications
     TypeFamilies
     TypeOperators
+
   ghc-options:
-    -Wall
-    -Wincomplete-uni-patterns
-    -Wincomplete-record-updates
-    -Wpartial-fields
-    -fprint-potential-instances
+    -Wall -Wincomplete-uni-patterns -Wincomplete-record-updates
+    -Wpartial-fields -fprint-potential-instances
+
   build-depends:
-    base >= 4.10 && < 5,
-    containers,
-    hashable,
-    template-haskell,
-    transformers,
-    unordered-containers
+    , base                  >=4.10 && <5
+    , containers
+    , hashable
+    , template-haskell
+    , transformers
+    , unordered-containers