Trying to avoid having top level commands in my dependently typed language. It's frustrating that you can't give a type to a signature easily! You need manifest fields or singletons or identity type trickery to make certain definitions public, or else you limit expressiveness. 🤔
Conversation
I wonder if you keep a journal of your general thoughts on the tradeoffs incurred in making a language dependently typed? With how the language is evolving and your vision, what do you think of bringing dependent typing onboard?
1
Sadly most of this is scattered around, eg:
- github.com/pikelet-lang/p
- app.element.io/#/group/+pikel
- gist.github.com/brendanzab/eba
- reddit.com/r/ProgrammingL
I was playing with Roam, but I'm now having a go at using Neuron for my personal note, which I hope will be more future proof?
1
1
I'm like dependent types - the implications of having them are just a bit tricky! I really like the idea of having first-class specifications. It's just there are many challenges with going down this route that seem like that don't have clear solutions yet.
2
1
I do wish that I was able to work with these programs more like annotated graphs - a lot of the current languages are very positionally dependent. I also want to be able to layer on more metadata in order to control compilation, like staging annotations for example.
2
2
But yeah that reflects lots of my frustration with existing programming tools right now - not just dependently typed languages. It's just that the solutions to any of this stuff is super unclear.