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…
Conversation
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.
1
1
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).
when you say phase problems, what do you mean exactly?
1
Ie. how to deal with the interpretation of 'formats descriptions' into the host language. Eg. do you mean a U32Be or an { x : Int | x in 0..u32_max }? It shows up where you have dependent types though. Gotta head off for a bit, but I can try to explain later!
2
1
Show replies