[colanderman]

OK, thanks for pointing those out to me. Google leads me here: http://adam.chlipala.net/cpdt/html/Hoas.html which discusses the typing issues.

But what of actually parsing a program in HOAS? The idea of HOAS is to translate the text "\x -> x + 5" into the expression Lam (\x -> Op("+", Var x, Const 5)). But how does one translate the string "x" into the variable name x short of data-as-code (or a similar meta-facility)?

The best Google turns up for this problem is here: http://books.google.com/books?id=OxeBw-sH4SUC&lpg=PA50&#... which seems to address the problem using a meta-facility of lambda-Prolog.

[trurl]

The best example I have handy is some Scala code a student I worked with wrote in Scala. I'm not sure if this is necessarily compatible with the latest version of their parser combinator library, but is hopefully suggestive:

  import scala.util.parsing.combinator.syntactical.StandardTokenParsers
  import scala.util.parsing.input._
  import scala.util.parsing.syntax._


  object HoasTest extends StandardTokenParsers {
    lexical.delimiters ++= List("(", ")", "\\", ".", ":", "=", "->", "+", "{", "}", ",", "*")
    lexical.reserved   ++= List("Bool", "Nat", "true", "false", "if", "then", "else", "succ",
                              "pred", "iszero", "let", "in", "fst", "snd")

    import lexical.NumericLit
    import lexical.Identifier

    def Term(base: Parser[Term]): Parser[Term] = positioned(
        SimpleTerm(base) ~ SimpleTerm(base) ^^ { case fun~arg => Apply(fun,arg) } // should be left-assoc
      | SimpleTerm(base) ~ ("+" ~> SimpleTerm(base)) ^^ { case a~b => Plus(a,b) } // should be left-assoc
      | SimpleTerm(base)
      | failure("illegal start of term"))

    def SimpleTerm(base: Parser[Term]): Parser[Term] = positioned(
        (("\\" ~> ident <~ ".") into (x => Parser { in =>

          def body(arg: Term): ParseResult[Term] = Term(Identifier(x) ^^^ arg | base)(in)
        
          body(new Term {}) match {
            case Success(_,rest) => Success(Lambda(x, (arg) => body(arg).get), rest)
           case f => f
          }
        }))
      | "(" ~> Term(base) <~ ")"
      | base
      | failure("illegal start of simple term"))

    def BaseTerm: Parser[Term] = positioned(
        numericLit ^^ { case n => Num(n.toInt) }
      | failure("unrecognized base term"))

    abstract class Term extends Positional

    case class Num(n: Int) extends Term

    case class Plus(a: Term, b: Term) extends Term

    case class Lambda(x: String, body: Term=>Term) extends Term {
      override def toString = "\\"+x+".("+body(new Term { override def toString = x }).toString+")"
    }

    case class Apply(fun: Term, arg: Term) extends Term

  }