we decided that self-describing data is the wrong problem. or at least, it's a thing people need but not by itself a hard thing to make. the reason we're never satisfied with the ones we have is *schemas*.
Conversation
so we came up with a schema format for dependently-typed object graphs. it's a compact binary format, mostly to help people resist the temptation to edit it directly as text and then be upset that its text representation doesn't meet their standards of beauty.
2
1
6
we got bogged down in the type checker.
1
2
notionally this could subsume any existing data format, whether self-describing or not. and then you could have a whole tool stack built on top of it - equivalents of diff, version control, grep, structure editors... but the tools would work on any data you had a schema for.
1
3
you could also implement programming languages on top of it, and stop using text files altogether. that's further out though.
1
1
anyway it's a lot of work and, while it would benefit the world, we think we can do more to help the world in the political domain rather than by spending our time building things.
1
1
thank you for asking.
2
3
1
1
Oh neat! I'm currently making a dependently typed data description language at - the intension is to describe existing binary data formats, but that is a big challenge, hehe. Trying to chip away at it. I really like the sound of this!
1
5
Using it as a basis for other tooling sounds really cool. :) :)
1
1
> we got bogged down in the type checker.
haaaa! The struggle! I'm implementing it directly in Rust, but it often feels cumbersome and slow. I do wonder if I would have been better served making more prototypes.
yeah the challenge is basically that most of the people who understand dependent type checkers are mathematicians rather than programmers. so all the explanations of it are, um, abstract.
3
4
is your thing going to be open source?
1
Show replies
Maybe I've mentioned this, but I think using Rust for elaboration isn't a good idea. You either have to write your own GC and RTS (as Lean devs did, working in C++), or else your implementation is guaranteed to not scale.
3
2
Yeah I don't think you've mentioned this, but it's a good thing to bring up. I do think it's better framed as, "Using Rust will mean that you need to build your own GC and RTS if you want it to scale", which I think is a really good thing to point out.