1
$\begingroup$

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.

$\endgroup$

1 Answer 1

1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.