> 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.
Conversation
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!
1
1
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
Need to get back to fixing that up. The main inspiration is PADS/DDC (the data description calculus), but turning it into a full dependent type system. Turns out that this leads to weird phase issues that I'm currently trying to figure out.