Using it as a basis for other tooling sounds really cool. :) :)
Conversation
> 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!
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 😭
hey, it's better than us - we never managed to put together a good easily-browseable version of the spec that doesn't need to be read in Scrivener. (though you will find HTML exports in that repo)
1
hmmm, so we think it's in a sense a mistake to have struct types as a primitive in the language. you can build them out of product types, so it doesn't make sense to have both. you can have pre-built structs as a library feature rather than a language feature.
2
1
Show replies
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.
1