Intuitive way to handle variable binding

Question

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.

Answer 1

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.