Ken,
Thanks for the references! Have two-level types been applied to parser
generation?
Best wishes,
--greg
Greg Meredith
in gmane.comp.lang.haskell.cafe: Here is an idea so obvious that someone else must have already thought of it and worked it all out. Consider the following grammar.
Hello!
If I understand your basic idea correctly, it is to split a recursive data type into two parts, a non-recursive type constructor and a knot-tying recursive type. This idea has been christened "two-level types" by
Tim Sheard and Emir Pasalic. 2004. Two-level types and parameterized modules. Journal of Functional Programming 14(5):547-587.
The idea dates earlier, to initial-algebra semantics and "functional programming with bananas and lenses":
Mark P. Jones. 1995. Functional programming with overloading and higher-order polymorphism. In Advanced functional programming: 1st international spring school on advanced functional programming techniques, ed. Johan Jeuring and Erik Meijer, 97-136. Lecture Notes in Computer Science 925. http://web.cecs.pdx.edu/~mpj/pubs/springschool.htmlhttp://web.cecs.pdx.edu/%7Empj/pubs/springschool.html
Erik Meijer, Maarten Fokkinga, and Ross Paterson. 1991. Functional programming with bananas, lenses, envelopes and barbed wire. In Functional programming languages and computer architecture: 5th conference, ed. John Hughes, 124-144. Lecture Notes in Computer Science 523. http://research.microsoft.com/~emeijer/Papers/fpca91.pdfhttp://research.microsoft.com/%7Eemeijer/Papers/fpca91.pdf
Cheers, Ken
Best wishes, --greg -- L.G. Meredith Managing Partner Biosimilarity LLC 505 N 72nd St Seattle, WA 98103 +1 206.650.3740 http://biosimilarity.blogspot.com
Greg Meredith
Thanks for the references! Have two-level types been applied to parser generation?
Hrm, I'm not sure what kind of application you have in mind, so I suppose the answer is that I'm not aware of any application. (: I suppose that the parser for the type-level fixpoint of a type constructor is the term-level fixpoint of a parser constructor. Unfortunately "data Fix f = Fix (f (Fix f)) deriving Read" doesn't work in Haskell, because there's no way to express the constraint that the type "f a" is an instance of Read whenever the type "a" is. However, see Valery Trifonov. 2003. Simulating quantified class constraints. In Haskell workshop, 98-102. http://flint.cs.yale.edu/trifonov/papers/sqcc.pdf http://flint.cs.yale.edu/trifonov/papers/sqcc.ps.gz This discussion also reminds me of Ralf Hinze. 2000. A new approach to generic functional programming. In POPL, 119-132. http://www.informatik.uni-bonn.de/~ralf/publications.html Cheers, Ken -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig Nevertheless, most cosmologists, including Dr. Guth and Dr. Linde, agree that the universe ultimately must come from somewhere, and that nothing is the leading candidate. Dennis Overbye, New York Times, May 22, 2001.
participants (2)
-
Chung-chieh Shan -
Greg Meredith