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
Is that because there hasn’t been enough languages that embody the theory or because theory itself hasn’t been developed sufficiently to address the corner cases?
1
Theory hasn't been developed enough I think. Lots of potential for people to fill in the gaps, but this takes time, investment, and motivation. Then you need to figure out which ideas are actually useful in practice.
1
1
Also sometimes the motivation is there, but it's blocked on some other load bearing thing. Not all the pieces are ready yet. Progress is being made though, which is encouraging! Does take longer than I would hope for, but it's really hard to rush this stuff.
Replying to
Yeah, I understand. Any worthwhile thing that has long term life is built one step at a time. I think the key point here is to be consistent and not let things wither away for a long time.
1
1
I am gonna give those links you shared a closer look and see how things evolved. Will respond back once I have a better picture.
1