This article really needs an (2013), because of<p>> Both GHC’s core IR, Ur/Web's core and Coq are explicitly typed in this way.<p>This is how GHC used to do, but in 2018 GHC adapted the pattern "trees that grow"<p>The paper <a href="https://www.jucs.org/jucs_23_1/trees_that_grow/jucs_23_01_0042_0062_najd.pdf" rel="nofollow noreferrer">https://www.jucs.org/jucs_23_1/trees_that_grow/jucs_23_01_00...</a> (the paper is actually from 2017)<p>Light GHC docs on it <a href="https://gitlab.haskell.org/ghc/ghc/-/wikis/implementing-trees-that-grow/trees-that-grow-guidance" rel="nofollow noreferrer">https://gitlab.haskell.org/ghc/ghc/-/wikis/implementing-tree...</a> (I recall seeing more through docs somewhere). I will quote<p>> The new HsSyn AST supporting the TTG idiom (from now on referred to as TTG HsSyn) is designed to subsume five different representations of Haskell syntax:<p>> AST GhcPs: the AST used in GHC's parsing phase
> AST GhcRn: the AST used in GHC's renaming phase
> AST GhcTc: the AST used in GHC's typechecking phase
> AST TH: the AST used in Template Haskell
> AST HSE: the AST used in an external tool such as Haskell-Src-Exts<p>This means that you have a single generic tree for all of those passes, but each pass has a different instantiation with has custom data<p>Also, some discussion of applications <a href="https://www.reddit.com/r/haskell/comments/7zo9mb/any_application_of_trees_that_grow/" rel="nofollow noreferrer">https://www.reddit.com/r/haskell/comments/7zo9mb/any_applica...</a> and slides here <a href="http://data.tmorris.net/talks/trees-that-grow/bc4ae902ca1d3bf37af86be8021d64a1de2b5116/trees-that-grow.pdf" rel="nofollow noreferrer">http://data.tmorris.net/talks/trees-that-grow/bc4ae902ca1d3b...</a><p>The thing about this is to observe that, in the blog post in the OP, when you added data to a given type, it was inserted as a concrete type (named Type here), that is, you went from<p><pre><code> data Exp = Num Int
| Bool Bool
| Var Var
| If Exp Exp Exp
| Lambda Var Exp
| App Exp Exp
</code></pre>
to<p><pre><code> type TExp = (TExp', Type)
data TExp' = TNum Int
| TBool Bool
| TVar Var
| TIf TExp TExp TExp
| TLambda Var TExp
| TApp TExp TExp
</code></pre>
But you <i>could</i> have kept it a generic type (here called a, rather than Type). This is a common pattern in both Haskell and Rust (and maybe other languages), and isn't the Trees That Grow pattern just yet, but it's like this:<p><pre><code> type GenericTExp a = (GenericTExp' a, a)
data GenericTExp' a = TNum Int
| TBool Bool
| TVar Var
| TIf TExp (GenericTExp a) (GenericTExp a)
| TLambda Var (GenericTExp a)
| TApp TExp (GenericTExp a)
</code></pre>
Now you can recover the original TExpr with<p><pre><code> type TExpr = GenericTExpr Type
</code></pre>
And you can recover the bare Expr with no added data type by putting () (called unit type) there<p><pre><code> type Expr = GenericTExpr ()
</code></pre>
Now, the paper also deals with the problem of, how to add new variants to a data type (it has a | Something that is open ended; this is called "extension constructor" in the ghc wiki, and denoted by XExpr), and how to add different data types to different nodes (you need to, instead of directly adding Type to the generic parameter, add a marker and use type-level functions - called type families in Haskell - to select the data type you're adding). When you figure out all those complexities, you end up with a type-level machinery that will inevitably be similar to the TTG idiom