A friendly little systems language with first-class types. https://github.com/pikelet-lang
so you might read a number, than that's assumed ahead of time to tell you the number of items to expect next
so based on that data you then know format of upcoming data
so you have some sort of data dependency there
Sounds like it should connect up with works on fuzzers quite nicely
so you want to make sure you're taking into account integer bounds etc. in you specification and saying what people should do in those cases
Though I guess if you have a type checker for meeting the binary specification then a fuzzer would need a type unchecker
so yeah, Fathom is like a dependently typed language with a built-in universe of format descriptions
Amazing, I love to hear these kind of usages
and it compiles those format descriptions to parsers and pretty printers
at least, it should do, once I figure out all the stuff 😔
like ideally Fathom is something that could just be embedded in a dependently typed language
but most dependently typed languages are really bad for compiling to native code, caring about memory layout, staging, etc.
unless you do the translation manually and do all the proofs
plus the toolchains and UX of using provers is a pain - I want something that can plug into a tool like cargo pretty nicely
Not sure if anybody linked it before, but this is a great blog post about Cubical Type Theory: https://abby.how/posts/cubical-type-theory.html
An implementation of cubical type theory by the author of that blog post is here: https://git.abby.how/abby/cubical
so strange to hear about abby like this, i used to hang out in some of the same spaces as her when we were very young so it's weird seeing her show up all over the place again
For those using Element to chat, and who are trying out the new 'spaces' beta, I've made a Pikelet space here, collecting together some relevant rooms: https://app.element.io/#/room/!WdJMYJDqGePIkLOwbP:matrix.org
Posted a bit of a thread on twitter talking about a quote from Don Syme about designing APIs that use ML-style modules: https://twitter.com/brendanzab/status/1399717007948357633
…when you have a component you don't know how many things to parameterise it by. Do you want to parameterise it by the type of strings, or date-times? You could do that! But by doing that you make the component more complex, and you've got to make all the choices up-front.
brendanzab Do you think any form of type level dispatch (I have in mind intensional polymorphism) would be helpful here. I have had the same thought about typeclasses in Haskell either being inefficient or being completely unwieldy.
And yeah I also find this with Rust's traits too 😦
I think I had a tweet in that thread talking about it
type classes and traits are also really annoying if you want to generalise/split stuff up retroactively - I think modules might be a bit more forgiving in that respect?
Intensional polymorphism was about having typecase whilst still maintaining a phase distinction. That allows precisely the sort of type based dispatch whereby a hashmap could be specialized on a given type for example. I think Sixten was inspired by that work.
yeah I like the idea of typecase
I think typecase might have weird implications though - but not sure
marwes:
IntoIterator for arrays makes pretty a bit nicer to use! https://github.com/yeslogic/fathom/pull/296/commits/9c98c6e5de5f9dfc04601dd1bc04a148a05e4c57
Is
append the main reason for returning DocBuilder from the allocator methods?
Just wonder if it would ever be possible to simplify the API a bit, eg. removing
DocBuilder
lol, I be doing bad things:
impl<'doc, D> std::ops::Deref for Context<'doc, D> {
type Target = &'doc D;
// FIXME: `&&'doc D` is a bit ick... egh
fn deref(&self) -> &&'doc D {
&self.alloc
}
}
Does anyone here know a nice story for how to structure error reporting or a "theory" of error reporting in a compiler with interesting types?
What kind of issues are you thinking of?
I made this thread on twitter which might be of interest: https://twitter.com/brendanzab/status/1381508264110682114
brendanzab I had in mind more like the mechanics of reporting the errors in a nice way ala rust or elm.
I haven't seen much in the way of theory for that though I know a number of ideas from those languages. I suppose it might just be more a matter of engineering than theory.
like, design principles?
I suppose just anything that is beyond engineering yeah, that might be design principles though, I'm not sure
Sounds like you are interested in usability? I've seen two camps for this, the elm way which is to provide very detailed/long errors https://elm-lang.org/news/compiler-errors-for-humans and the opposite opinion which is that errors should be short https://calebmer.com/2019/07/01/writing-good-compiler-error-messages.html