4 ms·
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 ter
by trurl 15y ago
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 15y agoOK, thanks for pointing those out to me. Google leads me here: http://adam.chlipala.net/cpdt/html/Hoas.html 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&ots=LLvKioXSKc&dq=hoas%20parser&pg=PA52#v=onepage&q=hoas%20parser&f=false http://books.google.com/books?id=OxeBw-sH4SUC&lpg=PA50&#... which seems to address the problem using a meta-facility of lambda-Prolog.
- trurl 15y agoThe 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 }