is your thing going to be open source?
Conversation
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
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
The issue is that these are 'dependent struct types', so they are more 'dependent sums' than 'product types'. I'm still on the fence as to if I want them to be nominal definitions though.
I'm also thinking I might want to separate out 'dependent sequence formats' from 'dependent structs' - this might help me with some of the phase problems I was having (mentioned in another tweet).
1
1
when you say phase problems, what do you mean exactly?
1
Show replies