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
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
At the moment I've been more focused on keeping closer to the more traditional dependent type theory stuff, but I might have to switch it up at some point.
1
Like, eventually I want to merge records and functions into some sort of 'graph thingy' with missing fields being the parameters. But I'm kind of inching towards that.
Replying to
Surely, graph would need to have some kind of ordering in certain parts and not in others I guess? Like when there is a subset relation on types, you would need to introduce partial order, no?
1
Yeah, I'm not sure how to impose restrictions on the graph. I was planning on enforce a DAG, then figuring out how to allow more expressiveness later.
1
Show replies