<p>Your suggestion does not quite work, but <strong>polymorphic higher-order abstract syntax</strong> does:</p>
<pre><code>data Prog name = Var name
               | App (Prog name) (Prog name)
               | Abs (name -&gt; Prog name)
</code></pre>
<p>See the paper <a href="http://adam.chlipala.net/papers/PhoasICFP08/PhoasICFP08.pdf" rel="nofollow noreferrer">Parametric Higher-Order Abstract Syntax for Mechanized Semantics</a> by Adam Chlipala.</p>

CC BY-SA 4.0
2022-02-15T16:27:04.740Z
2022-02-15T16:27:04.740Z
Andrej Bauer
<p>Suppose we have an algebraic datatype parameterised by a type variable <code>name</code>, e.g.</p>
<pre><code>data Prog name = Var name
               | App (Prog name) (Prog name)
               | Abs name (Prog name)
               deriving (Show, Eq)
</code></pre>
<p>What is the most straightforward and intuitive way to handle bindings and substitutions? Specifically, I am hoping for something that only relies on the type parameter (<code>name</code>) so that the underlying algebraic datatype doesn't need to be altered (unlike, for example, De Bruijn index). Thanks.</p>

<pl.programming-languages><lambda-calculus><functional-programming>
Intuitive way to handle variable binding
A confused dove
# Intuitive way to handle variable binding

(Asked by: username_0 on 2022-02-14)

Suppose we have an algebraic datatype parameterised by a type variable name, e.g.
data Prog name = Var name
               | App (Prog name) (Prog name)
               | Abs name (Prog name)
               deriving (Show, Eq)

What is the most straightforward and intuitive way to handle bindings and substitutions? Specifically, I am hoping for something that only relies on the type parameter (name) so that the underlying algebraic datatype doesn't need to be altered (unlike, for example, De Bruijn index). Thanks.

**Tags:** pl.programming-languages, lambda-calculus, functional-programming

---

## 1 answers

### Answer by username_1 on 2022-02-15. Score: 2 | Accepted answer

Your suggestion does not quite work, but polymorphic higher-order abstract syntax does:
data Prog name = Var name
               | App (Prog name) (Prog name)
               | Abs (name -> Prog name)

See the paper Parametric Higher-Order Abstract Syntax for Mechanized Semantics by Adam Chlipala.


---

