3 ms·
I suppose you could add a few to this list: Koka has formalised side-effects, and thanks to that can do in-place mutation after static analysis, similar to HVM.
by alexisread 4y ago
I suppose you could add a few to this list:
Koka has formalised side-effects, and thanks to that can do in-place mutation after static analysis, similar to HVM. It also uses static analysis to manage memory with elided reference counting.
Lastly, koka has managed to utilise static typing with dynamic binding, contrast with cell-lang which avoids dynamic binding (which has it's use cases).
https://koka-lang.github.io/koka/doc/book.html#sec-effect-types https://koka-lang.github.io/koka/doc/book.html#sec-effect-ty...
Flix does something similar to cell, though the typing is worked out better as lattice types ensure that there is an unambiguous top and bottom type. Addditionally where cell cannot compute dependent values, Flix can as it uses constraint modelling rather than reactive computation ie. the algo computing the rules is formally worked out to cover the edge cases.
https://flix.dev/principles/ https://flix.dev/principles/
Maude handles subtyping and typechecking of said subtypes through equational and rewrite logic. It has the concept of purely functional modules as well as impure (system) modules, but adds to that the math theories that represent the modules, so you get a lot of formal verification techniques at your disposal while programming.
http://maude.cs.illinois.edu/w/index.php/Maude_Overview http://maude.cs.illinois.edu/w/index.php/Maude_Overview
Composita covers the idea of removing pointers, and restricting components so you can use concurrency in anger (and managed memory without GC at the component level)
https://concurrency.ch/Content/publications/Blaeser_Component_Operating_System_PLOS_2007.pdf https://concurrency.ch/Content/publications/Blaeser_Componen...
Kali makes a good job of migrating processes - where cell restricts the ability to do closures due to the extended value set, kali can walk the call tree to migrate all linked state.
http://community.schemewiki.org/?Kali-Scheme-Revival http://community.schemewiki.org/?Kali-Scheme-Revival
I think cell looks interesting, but there seem to be restrictions here to simplify/avoid some of the harder problems. That in itself is not a bad thing, but it's worth noting given that some of these problems have been tackled individually above.
I'm not quite ready with a blend of these techniques, but it looks as though they are compatible with each other.
- verdagon 4y agoWow, I've never heard of most of these languages, and I consider myself a language expert! How did you learn of these?
- alexisread 4y agoMainly reading threads here :) I make a stab at looking at the top headlines. There's a pattern in a headline eg. Mentions of GC, datalog and so on which I flag. The exceptions are Composita and Maude. Composita is off the back of Oberon, which is one of the smaller language-based OSes. Maude I found on a keyword search around formal verification- I'm looking to build a new language so interesting stuff keeps coming up when you go down the rabbit holes ;)