A friendly little systems language with first-class types. https://github.com/pikelet-lang
brendanzab Well Dominic Orchard pinged Ben Moon on the slack
brendanzab Also says "we will have the implementation Gerty online in a month or so I think! that might make playing easier"
atennapel Alright cool
brendanzab 😆
atennapel 🤫
brendanzab Ooo, this is fun: https://journal.infinitenegativeutility.com/blocks-courtesy-of-konrad-zuse
brendanzab https://www.youtube.com/watch?v=OJGnpmnXR5w
suhr: how did it go with your LALRPOP SQL parser?
I have to write my own parser generator first though, because LALRPOP just dies.
my experience with LALRPOP is that it's fast when you got no errors, but once you have an ambiguity all hell breaks loose
I started using
sqlparser, it's not exactly optimal in terms of implementation but it seems quite complete
brendanzab: found this document by Conor McBride which also talks about manifest fields: http://staff.mmcs.sfedu.ru/~ulysses/Edu/SSGEP/conor/repo/notes.pdf
Chapter 6.1.1
references pollack's stuff
these notes look rather neat!
1 reply
no, I've seen them before though
I just end up using lalrpop usually 🙃
@gabriel: I've used grmtools, and really like it/have thought about integrating the nimbleparse tool into vscode, but the plain old nimbleparse gives a fast enough turn around time that I haven't really gotten around to it, anyhow if you're doing a lot of futzing around with grammars and like plain old yacc I think its great
e.g. the
$ nimbleparse java7.l java7.y Hello.java example from https://softdevteam.github.io/grmtools/master/book/nimbleparse.html
would be cool to have some sort of modular attribute grammary generator thing for rust
IELR gives LR(1) parsers with precedences and without mysterious conflicts.
Also, I want some nice things like poset precedences instead of linear one and grammar holes.
So I can write
Foo = ? and the parser generator checks the grammar like there's an unique token in the place of ?.
After reading more about cubical agda, I wonder if we can have cubical types everywhere.
how so?
or 'cubical is the default mode for agda'
It feels like a huge step forward. More flexible equality and quotient types out of the box via higher inductive types.
yeah it seems nifty - I think there are still some issues to sort through in some of the details though?
not super clear on all that though, but it definitely does seem exciting
I guess I would also hope to see people continue researching alternative approaches
It definitely influences alternative approaches.
This also looks interesting btw, “Internalizing Representation Independence with Univalence” https://www.youtube.com/watch?v=e3wGUuAxfG8