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
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
Definitely think that structured editing doesn't need to be all node-based programming. Excited to see more people playing around with this stuff.
Replying to
Yeah, I like how they retained text and still got the juice out of structured editing by creating a kind of invisible semantic layer. That sort of thing is a major missing point for transitioning into better tooling.
1
Thanks, we think it has a lot of potential! One of the, maybe more esoteric, goals is that Dion improve iteration speed on language design. We want Dion to be a tool for "code modeling" that spans many language types. Also, references in comments are part of the plan!
2
2
Show replies