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
Replying to
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.
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.
1
Show replies
Replying to
Have you been watching what is being built here? twitter.com/DionSystems/st
The idea of having a structure for text like that helps with various morphisms which I think could be leveraged for docs too.
Quote Tweet
1
2
Yeah this stuff is super neat!
1
1
Show replies