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.
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.
Replying to
This is partly why I am thinking of creating a graphic medium first whereby, you can create a graph and then do stuff like linear/partial ordering on it and then morph it into distinct shapes and then add labels on them later. A substrate like to think with is direly missing.
1
Yeah, I might end up experimenting with something similar too. Thinking about how I want doc comments to be part of the program graph (ie. referring to identifiers etc.) kind of suggests thinking about the graph might be useful.
2
Show replies