search

gallais / idris-tparsec

TParsec - Total Parser Combinators in Idris
https://gallais.github.io/idris-tparsec/
GNU General Public License v3.0
93 stars 10 forks source link

Add docs to SLTC example a la Arithmetic example #4

Closed Kazark closed 6 years ago

Kazark commented 6 years ago

Background

I am very excited about this library. A couple years ago I was all into parser combinators and tried using Lightyear. It made all my functions partial and my program crashed and I had no idea why. I searched around until I found the Agda paper (which I guess you wrote) but was out of energy and gave up. It was beyond me at the time; I was only beginning to put effort toward reading papers. I developed a style for writing total parsers in Idris without combinators. It was heavy on boilerplate but I was that committed to totality. I would write that way even in F#. In many ways I would say the purpose of dependent types is to enable totality.

So I was very excited to see that you had ported your stuff to Idris. I read your Arithmetic example and it was very helpful. I am going to try to read the paper now.

Request

If you wouldn't mind, I would love to see the STLC example documented in the style of the Arithmetic example docs. I would really like to grok and internalize what you've done here but my CS degree didn't prepare me at all for understanding academic computer science so I've been working to understand it on my own time because I have a great hunger for it.

Thank you for making this library.

Kazark commented 6 years ago

Much appreciated! Thanks so much! I've been working my way through the paper but my Agda is very weak so the more I can dig in on the Idris side the better.

gallais commented 6 years ago

If you have specific questions or an example of a (simple) grammar you'd like to implement but don't know where to start, don't hesitate to open an issue and I'll try to find the time to see what I can do.

Kazark commented 6 years ago

Thank you very much. I'm likely to take you up on that.

Kazark commented 5 years ago

I got pulled away from the project I was going to use this on, but am now getting back to a different project, with some simpler parsing requirements, and I think it's going to be a great one for diving in here. Since I first made a pass at this, I have gained a much better grasp of how to use Idris' WellFounded module, and have dabbled a bit more in Agda, and I have worked on correlating the Idris code to the Agda code in the paper, and all these things (as well as the repetition) have allowed me to make progress in grasping the paper: I've made it through the definition of fix and up to that point (but not quite including that yet---having to quit for the night) everything is making sense. I also think that that the latter bit, about the parser combinators, will come rather easily. I worked on digesting the invertible syntax descriptions paper since last making a pass at this, and understood that; which was rather mind-expanding in terms of parser combinators. Also I have an implementation right now for parsing the form of S-expressions I am seeking to parse, which has been instructive to construct. It is not recognized as total by Idris, but carries along a proof of diminution that has me convinced: (x : List Char) -> Either Error (y : List Char ** Smaller y x). It has given me some valuable prep, I can say, after glancing over the types in that section. However, I have realized that in its current form, I am not going to be able to use the utilities of the WellFounded module to get Idris to recognize my diminution proofs as giving rise to sound recursion: my types are the wrong shape when fitting into sizedRec, and so on. Which has nicely brought me back to this library, and I'm intending to grasp it this time!!

If I can get my "binary S-expressions" parser working with tparsec, I intend to parse something more complex with it. I'm excited.

Mostly just talking to myself here I guess. But again thanks for the paper and the library: I'm enthusiastic about it.