[trurl]

Uh, there are many papers and examples of using HOAS in statically typed settings, such as ML, Haskell, Twelf, Coq, etc. There is still the issue of exotic terms, but there are known type system tricks for helping with that as well. And the exotic term problem would be even worse in Scheme.

[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

  }