Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
telling you what bytes to expect where
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
Boarders#4085
@_discord_535117309732323328:t2bot.io
[m]
Ah ok, I see
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
and this stuff can get pretty complicated
Boarders#4085
@_discord_535117309732323328:t2bot.io
[m]
That is very cool stuff
Sounds like it should connect up with works on fuzzers quite nicely
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
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
Boarders#4085
@_discord_535117309732323328:t2bot.io
[m]
Though I guess if you have a type checker for meeting the binary specification then a fuzzer would need a type unchecker
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
hehe
so yeah, Fathom is like a dependently typed language with a built-in universe of format descriptions
Boarders#4085
@_discord_535117309732323328:t2bot.io
[m]
Amazing, I love to hear these kind of usages
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
and it compiles those format descriptions to parsers and pretty printers
at least, it should do, once I figure out all the stuff 😔
Boarders#4085
@_discord_535117309732323328:t2bot.io
[m]
ah yeah, great stuff
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
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
Labbekak#0369
@_discord_84011264606502912:t2bot.io
[m]
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
Labbekak#0369
@_discord_84011264606502912:t2bot.io
[m]
An implementation of cubical type theory by the author of that blog post is here: https://git.abby.how/abby/cubical
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
Yeah, Abby does really cool work
uber
@uber:kde.org
[m]
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
brendanzab
@brendanzab:matrix.org
[m]
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
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]

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.

Boarders#4085
@_discord_535117309732323328:t2bot.io
[m]
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.
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
Oh interesting Boarders! not sure if I've come across "intensional polymorphism" before?
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?
Boarders#4085
@_discord_535117309732323328:t2bot.io
[m]
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.
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
oh interesting
yeah I like the idea of typecase
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
I think typecase might have weird implications though - but not sure
brendanzab
@brendanzab:matrix.org
[m]
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
brendanzab
@brendanzab:matrix.org
[m]
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
        }
    }
Boarders#4085
@_discord_535117309732323328:t2bot.io
[m]
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?
_discord_280132690059984897
@_discord_280132690059984897:t2bot.io
[m]
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#6008
@_discord_280132690059984897:t2bot.io
[m]
Boarders#4085
@_discord_535117309732323328:t2bot.io
[m]
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.
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
theory in terms of usability?
like, design principles?
Boarders#4085
@_discord_535117309732323328:t2bot.io
[m]
I suppose just anything that is beyond engineering yeah, that might be design principles though, I'm not sure
RazzBerry#6167
@_discord_165599453716283392:t2bot.io
[m]
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