diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,4 +1,25 @@
 
+## symantic-base-0.4.0.20211106 (2021-11-18)
+
+### Interface
+
+* Rename `Symantic.{View => Viewer}`.
+* Rename `Symantic.{ObserveSharing => SharingObserver}`.
+* Rename `Symantic.{Class => Classes}`.
+* Update release `version`.
+
+### Documentation
+
+* Fix minor shortcomings.
+* Update `ChangeLog.md`.
+
+### Build
+
+* Fix `flake.lock` to use a public Nixpkgs.
+* Move all Nix config into `flake.nix`.
+* Update nix input `nixpkgs`.
+
+
 ## symantic-base-0.3.0.20211007 (2021-10-07)
 
 ### Interface
diff --git a/default.nix b/default.nix
deleted file mode 100644
--- a/default.nix
+++ /dev/null
@@ -1,29 +0,0 @@
-{ pkgs ? import <nixpkgs> {}
-, inputs ? {}
-, ghc ? null
-, withHoogle ? false
-, ...
-}:
-let
-  haskellPackages =
-    if ghc == null
-    then pkgs.haskellPackages
-    else pkgs.haskell.packages.${ghc};
-  hs = haskellPackages.extend (with pkgs.haskell.lib; hself: hsuper: {
-    symantic-base = buildFromSdist (hself.callCabal2nix "symantic-base" ./. {});
-  });
-in hs.symantic-base // {
-  shell = hs.shellFor {
-    doBenchmark = true;
-    packages = p: [ p.symantic-base ];
-    nativeBuildInputs = [
-      hs.cabal-install
-      hs.ghcid
-      hs.haskell-language-server
-      hs.hlint
-      pkgs.git-chglog
-      pkgs.reuse
-    ];
-    inherit withHoogle;
-  };
-}
diff --git a/flake.lock b/flake.lock
--- a/flake.lock
+++ b/flake.lock
@@ -2,8 +2,10 @@
   "nodes": {
     "nixpkgs": {
       "locked": {
-        "narHash": "sha256-1XuSYfeI9j4jBnJo2Au1OKaPzfq7HUl4YPqxE5JvrN0=",
-        "path": "/nix/store/q1aqjzvpwwb3crfv0awr60x63s6xfb66-nixpkgs-patched",
+        "lastModified": 1640319671,
+        "narHash": "sha256-ZkKmakwaOaLiZOpIZWbeJZwap5CzJ30s4UJTfydYIYc=",
+        "path": "/nix/store/293cqgx8pcmkcn9mx5ln6i9nwvxv274r-source",
+        "rev": "eac07edbd20ed4908b98790ba299250b5527ecdf",
         "type": "path"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
--- a/flake.nix
+++ b/flake.nix
@@ -1,14 +1,31 @@
 {
 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 {
-    inherit inputs system;
+  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
-  rec {
-    defaultPackage = forAllSystems (import ./default.nix);
-    devShell = lib.mapAttrs (_: x: x.shell) defaultPackage;
+  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;
+      });
   };
 }
diff --git a/src/Symantic.hs b/src/Symantic.hs
--- a/src/Symantic.hs
+++ b/src/Symantic.hs
@@ -1,19 +1,19 @@
 module Symantic
- ( module Symantic.Class
+ ( module Symantic.Classes
  , module Symantic.CurryN
  , module Symantic.Data
  , module Symantic.Derive
- , module Symantic.ObserveSharing
  , module Symantic.Optimize
  , module Symantic.Reify
- , module Symantic.View
+ , module Symantic.SharingObserver
+ , module Symantic.Viewer
  ) where
 
-import Symantic.Class
+import Symantic.Classes
 import Symantic.CurryN
 import Symantic.Data
 import Symantic.Derive
-import Symantic.ObserveSharing
 import Symantic.Optimize
 import Symantic.Reify
-import Symantic.View
+import Symantic.SharingObserver
+import Symantic.Viewer
diff --git a/src/Symantic/Class.hs b/src/Symantic/Class.hs
deleted file mode 100644
--- a/src/Symantic/Class.hs
+++ /dev/null
@@ -1,428 +0,0 @@
-{-# LANGUAGE DataKinds #-} -- For ReprKind
-{-# LANGUAGE PatternSynonyms #-} -- For (:!:)
-{-# LANGUAGE TypeFamilyDependencies #-} -- For Permutation
-{-# LANGUAGE UndecidableInstances #-} -- For Permutation
-module Symantic.Class 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'
-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 is 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 to '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 to '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 to '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]
-
--- * 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'
--- | FIXME: this class should likely be removed
-class Voidable repr where
-  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/Classes.hs b/src/Symantic/Classes.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Classes.hs
@@ -0,0 +1,440 @@
+{-# 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/Data.hs b/src/Symantic/Data.hs
--- a/src/Symantic/Data.hs
+++ b/src/Symantic/Data.hs
@@ -16,7 +16,7 @@
 import qualified Data.Function as Fun
 import qualified Data.Maybe as Maybe
 
-import Symantic.Class
+import Symantic.Classes
 import Symantic.Derive
 
 -- * Type 'SomeData'
diff --git a/src/Symantic/Derive.hs b/src/Symantic/Derive.hs
--- a/src/Symantic/Derive.hs
+++ b/src/Symantic/Derive.hs
@@ -11,7 +11,7 @@
 type family Derived (repr :: Type -> Type) :: Type -> Type
 
 -- * Class 'Derivable'
--- | Derive an interpreter to a another interpreter
+-- | 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.
diff --git a/src/Symantic/ObserveSharing.hs b/src/Symantic/ObserveSharing.hs
deleted file mode 100644
--- a/src/Symantic/ObserveSharing.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.ObserveSharing 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 'ObserveSharing'
-newtype ObserveSharing letName repr a = ObserveSharing { unObserveSharing ::
-  MT.ReaderT (HashSet SharingName)
-             (MT.State (ObserveSharingState letName))
-             (FinalizeSharing 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 =>
-  ObserveSharing letName repr a ->
-  WithSharing letName repr a
-observeSharing (ObserveSharing m) =
-  let (fs, st) = MT.runReaderT m mempty `MT.runState`
-        ObserveSharingState
-          { 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 'ObserveSharingState'
-data ObserveSharingState letName = ObserveSharingState
-  { oss_refs :: HashMap SharingName (letName, Int)
-  , oss_recs :: HashSet SharingName
-  }
-
-observeSharingNode ::
-  Eq letName =>
-  Hashable letName =>
-  Show letName =>
-  Referenceable letName repr =>
-  MakeLetName letName =>
-  ObserveSharing letName repr a ->
-  ObserveSharing letName repr a
-observeSharingNode (ObserveSharing m) = ObserveSharing $ 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 (ObserveSharing letName repr) = FinalizeSharing letName repr
-instance
-  ( Referenceable letName repr
-  , MakeLetName letName
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => LiftDerived (ObserveSharing letName repr) where
-  liftDerived = observeSharingNode . ObserveSharing . return
-instance
-  ( Referenceable letName repr
-  , MakeLetName letName
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => LiftDerived1 (ObserveSharing letName repr) where
-  liftDerived1 f a = observeSharingNode $ ObserveSharing $
-    f <$> unObserveSharing a
-instance
-  ( Referenceable letName repr
-  , MakeLetName letName
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => LiftDerived2 (ObserveSharing letName repr) where
-  liftDerived2 f a b = observeSharingNode $ ObserveSharing $
-    f <$> unObserveSharing a
-      <*> unObserveSharing b
-instance
-  ( Referenceable letName repr
-  , MakeLetName letName
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => LiftDerived3 (ObserveSharing letName repr) where
-  liftDerived3 f a b c = observeSharingNode $ ObserveSharing $
-    f <$> unObserveSharing a
-      <*> unObserveSharing b
-      <*> unObserveSharing c
-instance
-  ( Referenceable letName repr
-  , MakeLetName letName
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => LiftDerived4 (ObserveSharing letName repr) where
-  liftDerived4 f a b c d = observeSharingNode $ ObserveSharing $
-    f <$> unObserveSharing a
-      <*> unObserveSharing b
-      <*> unObserveSharing c
-      <*> unObserveSharing d
-instance Referenceable letName (ObserveSharing letName repr) where
-  ref = error "[BUG]: observeSharing MUST NOT be applied twice"
-instance Definable letName (ObserveSharing letName repr) where
-  define = error "[BUG]: observeSharing MUST NOT be applied twice"
-instance Letsable letName (ObserveSharing letName repr) where
-  lets = error "[BUG]: observeSharing MUST NOT be applied twice"
-
--- * Type 'FinalizeSharing'
--- | Remove 'define' when non-recursive or unused
--- or replace it by 'ref', moving 'define's to the top.
-newtype FinalizeSharing letName repr a = FinalizeSharing { unFinalizeSharing ::
-  MT.ReaderT (HS.HashSet letName)
-    (MT.Writer (LetBindings letName repr))
-      (repr a) }
-
-type instance Derived (FinalizeSharing _letName repr) = repr
-instance (Eq letName, Hashable letName) =>
-  LiftDerived (FinalizeSharing letName repr) where
-  liftDerived = FinalizeSharing . pure
-instance (Eq letName, Hashable letName) =>
-  LiftDerived1 (FinalizeSharing letName repr) where
-  liftDerived1 f a = FinalizeSharing $ f <$> unFinalizeSharing a
-instance (Eq letName, Hashable letName) =>
-  LiftDerived2 (FinalizeSharing letName repr) where
-  liftDerived2 f a b = FinalizeSharing $
-    f <$> unFinalizeSharing a
-      <*> unFinalizeSharing b
-instance (Eq letName, Hashable letName) =>
-  LiftDerived3 (FinalizeSharing letName repr) where
-  liftDerived3 f a b c = FinalizeSharing $
-    f <$> unFinalizeSharing a
-      <*> unFinalizeSharing b
-      <*> unFinalizeSharing c
-instance (Eq letName, Hashable letName) =>
-  LiftDerived4 (FinalizeSharing letName repr) where
-  liftDerived4 f a b c d = FinalizeSharing $
-    f <$> unFinalizeSharing a
-      <*> unFinalizeSharing b
-      <*> unFinalizeSharing c
-      <*> unFinalizeSharing d
-instance
-  ( Referenceable letName repr
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => Referenceable letName (FinalizeSharing letName repr) where
-  ref isRec = liftDerived . ref isRec
-instance
-  ( Referenceable letName repr
-  , Eq letName
-  , Hashable letName
-  , Show letName
-  ) => Definable letName (FinalizeSharing letName repr) where
-  define name body = FinalizeSharing $ 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 (FinalizeSharing letName repr) where
-  lets defs x = FinalizeSharing $ 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/Optimize.hs b/src/Symantic/Optimize.hs
--- a/src/Symantic/Optimize.hs
+++ b/src/Symantic/Optimize.hs
@@ -3,7 +3,7 @@
 import Data.Bool (Bool)
 import qualified Data.Function as Fun
 
-import Symantic.Class
+import Symantic.Classes
 import Symantic.Data
 
 -- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
diff --git a/src/Symantic/Reify.hs b/src/Symantic/Reify.hs
--- a/src/Symantic/Reify.hs
+++ b/src/Symantic/Reify.hs
@@ -7,7 +7,7 @@
 import qualified Data.Function as Fun
 import qualified Language.Haskell.TH as TH
 
-import Symantic.Class (Abstractable(..))
+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
diff --git a/src/Symantic/SharingObserver.hs b/src/Symantic/SharingObserver.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/SharingObserver.hs
@@ -0,0 +1,385 @@
+{-# 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/View.hs b/src/Symantic/View.hs
deleted file mode 100644
--- a/src/Symantic/View.hs
+++ /dev/null
@@ -1,107 +0,0 @@
-{-# LANGUAGE GADTs #-} -- For View
-{-# LANGUAGE OverloadedStrings #-} -- For convenience
-{-# LANGUAGE UndecidableInstances #-} -- For Show (SomeData a)
-module Symantic.View where
-
-import Data.Int (Int)
-import Data.String
-import Text.Show
-import qualified Data.Function as Fun
-import qualified Prelude
-
-import Symantic.Class
-import Symantic.Data
-import Symantic.Derive
-import Symantic.Fixity
-
-data View a where
-  View :: (ViewEnv -> ShowS) -> View a
-  ViewUnifix :: Unifix -> String -> String -> View (a -> b)
-  ViewInfix :: Infix -> String -> String -> View (a -> b -> c)
-  ViewApp :: View (b -> a) -> View b -> View a
-
-runView :: View a -> ViewEnv -> ShowS
-runView (View v) env = v env
-runView (ViewInfix _op name _infixName) _env = showString name
-runView (ViewUnifix _op name _unifixName) _env = showString name
-runView (ViewApp f x) env =
-  pairView env op Fun.$
-    runView f env{viewEnv_op = (op, SideL) } Fun..
-    showString " " Fun..
-    runView x env{viewEnv_op = (op, SideR) }
-  where op = infixN 10
-
--- | Unusual, but enables to leverage default definition of methods.
-type instance Derived View = View
-instance LiftDerived View where
-  liftDerived = Fun.id
-
-instance IsString (View a) where
-  fromString s = View Fun.$ \_env -> showString s
-instance Show (View a) where
-  showsPrec p = (`runView` ViewEnv
-    { viewEnv_op = (infixN p, SideL)
-    , viewEnv_pair = pairParen
-    , viewEnv_lamDepth = 1
-    })
-instance Show (SomeData View a) where
-  showsPrec p (SomeData x) = showsPrec p (derive x :: View a)
-
-data ViewEnv
-  = ViewEnv
-  { viewEnv_op :: (Infix, Side)
-  , viewEnv_pair :: Pair
-  , viewEnv_lamDepth :: Int
-  }
-
-pairView :: ViewEnv -> Infix -> ShowS -> ShowS
-pairView 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 View where
-  var = Fun.id
-  lam f = viewLam "x" f
-  lam1 f = viewLam "u" f
-  ViewInfix op _name infixName .@ ViewApp x y = View Fun.$ \env ->
-    pairView env op Fun.$
-      runView x env{viewEnv_op=(op, SideL)} Fun..
-      showString " " Fun.. showString infixName Fun.. showString " " Fun..
-      runView y env{viewEnv_op=(op, SideR)}
-  ViewInfix op name _infixName .@ x = View Fun.$ \env ->
-    showParen Prelude.True Fun.$
-      runView x env{viewEnv_op=(op, SideL)} Fun..
-      showString " " Fun.. showString name
-  f .@ x = ViewApp f x
-viewLam :: String -> (View a -> View b) -> View (a -> b)
-viewLam varPrefix f = View Fun.$ \env ->
-  pairView env op Fun.$
-    let x = showString varPrefix Fun..
-            showsPrec 0 (viewEnv_lamDepth env) in
-    -- showString "Lam1 (" .
-    showString "\\" Fun.. x Fun.. showString " -> " Fun..
-    runView (f (View (\_env -> x))) env
-      { viewEnv_op = (op, SideL)
-      , viewEnv_lamDepth = Prelude.succ (viewEnv_lamDepth env)
-      }
-    -- . showString ")"
-  where
-  op = infixN 0
-instance Anythingable View
-instance Bottomable View where
-  bottom = "<hidden>"
-instance Show c => Constantable c View where
-  constant c = View Fun.$ \_env -> shows c
-instance Eitherable View where
-  left = "Left"
-  right = "Right"
-instance Equalable View where
-  equal = ViewInfix (infixN 4) "(==)" "=="
-instance Listable View where
-  cons = ViewInfix (infixR 5) "(:)" ":"
-  nil = "[]"
-instance Maybeable View where
-  nothing = "Nothing"
-  just = "Just"
diff --git a/src/Symantic/Viewer.hs b/src/Symantic/Viewer.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Viewer.hs
@@ -0,0 +1,107 @@
+{-# 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
@@ -10,26 +10,26 @@
 -- PVP:  +-+------- breaking API changes
 --       | | +----- non-breaking API additions
 --       | | | +--- code changes with no API change
-version: 0.3.0.20211007
+version: 0.4.0.20211106
 stability: experimental
 category: Data Structures
-synopsis: Basic symantics combinators for Embedded Domain-Specific Languages (EDSL)
+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.Class@
+  * @Symantic.Classes@
     gathers commonly used tagless-final combinators
     (the syntax part of symantics).
-  * @Symantic.Data@ is an interpreter enabling to pattern-match on combinators,
-    while keeping their extensibility.
+  * @Symantic.Data@ interprets combinators as data constructors
+    enabling to pattern-match on combinators while keeping their extensibility.
   * @Symantic.Derive@
-    enables to give a default value to combinators which avoids boilerplate code
+     to give a default value to combinators which avoids boilerplate code
     when implementing combinators for an interpreter is factorizable.
-  * @Symantic.ObserveSharing@
-    enables to observe Haskell @let@ definitions,
-    turning infinite values into finite ones,
-    which is useful to inspect and optimize recursive grammars for example.
+  * @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@
@@ -38,14 +38,14 @@
     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.View@
-    is an interpreter enabling to turn combinators into a human-readable string.
+  * @Symantic.Viewer@
+    interprets combinators as human-readable text.
   * @Symantic.ADT@
     enables to derive reciprocal functions between
-    data-constructors and @Either@s of tuples.
+    algebraic data type constructors and @Either@s of tuples.
   * @Symantic.CurryN@
     gathers utilities for currying or uncurrying tuples
-    of size greater or equal to 2.
+    of size greater or equal to two.
   * @Symantic.Fixity@
     gathers utilities for parsing or viewing
     infix, prefix and postfix combinators.
@@ -55,7 +55,6 @@
   ChangeLog.md
 extra-source-files:
   cabal.project
-  default.nix
   .envrc
   flake.lock
   flake.nix
@@ -71,15 +70,15 @@
   exposed-modules:
     Symantic
     Symantic.ADT
-    Symantic.Class
+    Symantic.Classes
     Symantic.CurryN
     Symantic.Data
     Symantic.Derive
     Symantic.Fixity
-    Symantic.ObserveSharing
     Symantic.Optimize
     Symantic.Reify
-    Symantic.View
+    Symantic.SharingObserver
+    Symantic.Viewer
   default-language: Haskell2010
   default-extensions:
     DefaultSignatures