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.
Conversation
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.
1
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
There is something called Relation Algebra: en.wikipedia.org/wiki/Relation_
It is a bit niche at the moment, but I think if you can turn those equational laws into combinators, arbitrary orderings and restrictions could be brought in on substructures of the graph.
2
Oh yeah I've been thinking about looking at something like that. Kind of funny that you say it is niche, when it was a big inspiration for relational databases! 😆
1
Oh wait, I am confusing it with the other relational algebra? There are two? 😳
Replying to
The confusion is quite likely and they share fused roots.
Peirce → Arthur Burks → E. F. Codd → Relational Algebra
Peirce → Tarksi, Givant → Relation Algebra
Also, if you look closely, you can see the relational algebra operators having morphisms with relation algebra ones.
2