content: {-# LANGUAGE DataKinds, GADTs, KindSignatures, EmptyDataDecls, TypeFamilies,
      PolyKinds, TypeOperators, PatternSynonyms #-}
  
  module NormTree where
  
  import Data.Traversable
  import Data.Foldable
  import Data.List
  
  -- Natural numbers
  data Nat = Z | S Nat
  
  -- Singletons for natural numbers
  data Natty :: Nat -> * where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)
  
  -- Vectors
  data Vec :: Nat -> * -> * where
    Nil  :: Vec Z x
    (:.) :: x -> Vec n x -> Vec (S n) x
  infixr 5 :.
  
  -- The following definition is a Haskellization of the
  -- "fixpoint of normal functors"
  -- from https://github.com/pigworker/MetaprogAgda/raw/master/notes.pdf
  -- section 1.9
  
  -- General Single Sorted Trees Containing x things
  data NormTree (sh :: Nat -> * -> *)(x :: *) :: * where
    (:-) :: sh n x -> Vec n (NormTree sh x) -> NormTree sh x
    -- the sh parameter determines the possible shapes of nodes
    -- for each arity; we expect it to be a GADT or a data family
  infix 4 :-
  
  -- Here's how to say "the usual shapes, or some extra shapes,
  --   but nobody else handles variables"
  data ExpPlush (sh :: Nat -> *) :: Nat -> * -> * where
    Var :: x -> ExpPlush sh Z x
    Abs :: x -> ExpPlush sh (S Z) x
    App :: ExpPlush sh (S (S Z)) x
    Tup :: Natty n -> ExpPlush sh n x
    Plus :: sh n -> ExpPlush sh n x  -- see? no x in the shapes
  
  -- You can say "no extra shapes"
  data NoExt :: Nat -> * where
  
  -- So, just the usual shapes, with strings for variables.
  type Basic = NormTree (ExpPlush NoExt) String
  
  -- The Church numeral for 2 looks like this.
  church2 :: Basic
  church2 = Abs "f" :- (Abs "x" :-
              (App :-
                (Var "f" :- Nil) :.
                (App :- (Var "f" :- Nil) :. (Var "x" :- Nil) :. Nil) :.
                Nil) :.
              Nil) :. Nil
  -- That's easy to clean with pattern synonyms.
  
  -- Generic calculation, e.g. of free variables, is cheap.
  freeVars :: Eq x => NormTree (ExpPlush sh) x -> [x]
  freeVars (Var x :- Nil) = [x]
  freeVars (Abs x :- t :. Nil) = delete x (freeVars t)
  freeVars (_ :- ts) = foldr (union . freeVars) [] ts
  
  
  -- But what if we're multisorted?
  
  -- The above notes generalize normal functors to containers (chapter 3)
  --   (by the way, you can sort of do containers in Haskell
  --    https://pigworker.wordpress.com/2015/06/06/hasochistic-containers-a-first-attempt/
  --    but I digress)
  -- then to indexed (i.e., multisorted) containers (chapter 4)
  -- which are closed under fixpoints (section 4.5)
  
  -- The theory of containers (and indexed containers) is a depth well plumbed
  -- by Neil Ghani and his friends (e.g. Michael Abbott, Thorsten Altenkirch,
  -- me, Peter Morris, Peter Hancock). The papers tend to be quite categorical,
  -- which is tricky if you don't have the relevant Babelfish in your ear.
  -- DBLP Neil Ghani and search for "container" for the back issues of the
  -- series.
  -- This paper http://www.cs.nott.ac.uk/~psztxa/publ/jpartial.pdf
  -- is about differentiability of containers, but has some *pictures*
  -- which might help make sense of the categorical mumbo jumbo.
  
  -- It's a big brain upload, but it has that "threshold concept" aspect
  -- of changing the way you perceive what is common to inductive data
  -- structures, and to systems of interactive programming (which is
  -- Hancock's key insight). Almost like you *can* see the wood for the trees.
  -- The "Cambridge notes" I linked to, above, give a more
  -- (Agda-)programming-oriented presentation.
  -- Brain-mangling homework exercises are available on request.
  
  -- My plan here is to drag the indexed container fixpoint construction back
  -- to the finitary case. We get multisorted normal functors.
  -- A *number* of recursive position becomes
  --   a *list of sorts* of recursive (and nonrecursive) positions,
  
  -- So...
  
  -- Sorts are either terminal (Left) or nonterminal (Right).
  type family Case (f :: x -> *) (g :: y -> *) (z :: Either x y) :: * where
    Case f g (Left x)  = f x
    Case f g (Right y) = g y
  
  -- If we know how to build both, we can interpret a list of sorts.
  data Kids (f :: x -> *)(g :: y -> *)(zs :: [Either x y]) :: * where
    KNil :: Kids f g '[]
    (:&) :: Case f g z -> Kids f g zs -> Kids f g (z ': zs)
  infixr 5 :&
  
  -- Now a shape is indexed by its own nonterminal sort and its kids' sorts.
  data MutTree (sh :: y -> [Either x y] -> *)(v :: x -> *)(i :: y) where
    (:=) :: sh i zs -> Kids v (MutTree sh v) zs -> MutTree sh v i
  infixr 4 :=
  
  -- Let's go wild!
  data Side = Pat | Exp
  data Sort = Tm Side | Def | List Sort
  -- Sorts are closed under list formation, term sorts and definition sorts.
  -- Term sorts are either pattern or expression.
  
  -- Now we say what the syntax trees are by describing the shapes for
  -- each sort. We have only one nonterminal sort -- identifiers.
  --
  -- But, by way of going wild, I've added
  --   "mode" whose job is to specify labelling disciplines
  --      (and I'm not fussy what kind mode is)
  --   "more" whose job is to specify syntax extensions
  -- I'm choosing only to label variable references, but ymmv.
  -- Crucially, this labelling and extensibility discipline has
  -- nothing to do with the idea of how to make trees.
  -- Helpfully, "more" also takes "Mode", so extensions are free
  --   to negotiate their own relationships with labelling disciplines.
  data Syntax :: (mode -> Sort -> [Either () Sort] -> *) ->
                  mode -> Sort -> [Either () Sort] -> * where
    SNil   :: Syntax more mode (List s) '[]
    SCons  :: Syntax more mode (List s) '[Right s, Right (List s)]
    SVar   :: LabelVar mode -> Syntax more mode (Tm e)   '[Left '()]
    SCon   :: Syntax more mode (Tm e)   '[Left '(), Right (List (Tm e))]
    SAbs   :: Syntax more mode (Tm Exp) '[Left '(), Right (Tm Exp)]
    SApp   :: Syntax more mode (Tm Exp) '[Right (Tm Exp), Right (Tm Exp)]
    SLet   :: Syntax more mode (Tm Exp) '[Right (List Def), Right (Tm Exp)]
    SEqn   :: Syntax more mode Def
                        '[Left '(), Right (List (Tm Pat)), Right (Tm Exp)]
    SMore  :: more mode y zs -> Syntax more mode y zs
  
  -- The empty extension.
  data NoMore :: mode -> Sort -> [Either () Sort] -> * where
  
  -- Two labelling disciplines.
  data Mode = Plain | Fancy  -- actually, Mode should be extensible
  type family LabelVar (m :: mode) :: * where
    LabelVar Plain = ()
    LabelVar Fancy = Int
  
  -- We need to interpret the nonterminal sort somehow.
  data N (i :: ()) = N String
  
  -- Here's an example with expressions, patterns and definitions
  church4 :: MutTree (Syntax NoMore Fancy) N (Tm Exp)
  church4 =
    SLet := (SCons := (SEqn := N "church2"
                            :& (SCons := (SVar 1 := N "f" :& KNil)
                                      :& (SCons := (SVar 2 := N "x" :& KNil)
                                                :& (SNil := KNil)
                                                :& KNil)
                                      :& KNil)
                            :& (SApp := (SVar 1 := N "f" :& KNil)
                                     :& (SApp := (SVar 1 := N "f" :& KNil)
                                              :& (SVar 2 := N "x" :& KNil)
                                              :& KNil)
                                     :& KNil)
                            :& KNil)
                   :& (SNil := KNil)
                   :& KNil)
         :& (SApp := (SVar 0 := N "church2" :& KNil)
                  :& (SVar 0 := N "church2" :& KNil)
                  :& KNil)
         :& KNil
  
  -- Now let me hide some cruft.
  
  pattern PNil = SNil := KNil
  pattern x :+ xs = SCons := x :& xs :& KNil
  infixr 6 :+
  pattern f :$ a = SApp := f :& a :& KNil
  infixl 7 :$
  pattern PV :: LabelVar mode -> String -> MutTree (Syntax NoMore mode) N (Tm e)
  pattern PV i x = SVar i := N x :& KNil
  
  church4' :: MutTree (Syntax NoMore Fancy) N (Tm Exp)
  church4' =
    SLet := ((SEqn := N "church2"
                   :& PV 1 "f" :+ PV 2 "x" :+ PNil
                   :& PV 1 "f" :$ (PV 1 "f" :$ PV 2 "x")
                   :& KNil)
             :+ PNil)
         :& PV 0 "church2" :$ PV 0 "church2"
         :& KNil
  
  
  -- Dull stuff
  
  instance Traversable (Vec n) where
    traverse f Nil = pure Nil
    traverse f (x :. xs) = pure (:.) <*> f x <*> traverse f xs
  
  instance Functor (Vec n) where
    fmap = fmapDefault
  
  instance Foldable (Vec n) where
    foldMap = foldMapDefault
  