Conversation
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.
2
1
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
Yeah, it is! It's here - still in a state of being rebuilt though so it's not super useful yet: github.com/yeslogic/ddl - planning to get back to it this week. Lots and lots of disclaimers yadayada…
1
1
I'm also making a dependently typed lang as a side project too - hopefully with structured editing at some stage too: github.com/pikelet-lang/p
1
1
exciting! most of what's written for ours is the specification, and some C code that handles the "parsing".
3
1
if we went back to it we would definitely move to Rust.
1
2
Cool! I'll have a look and see if there's anything interesting I can learn!
mind if we leave our thoughts on your thing as we read through the spec?
1
Sadly I let the spec get out of date 😭
2
Show replies