Quelklef

milk consumer

girly but not a girl

name-color: #C09


at this point there are well-established methods for tracking types in programming languages. (monads, algebraic effects, etc)

one area of research which afaik is still under development is tracking partiality. i believe idris has a feature that lets you mark a function as total or partial and it will ensure that all functions which are supposed to be total actually are (unless you use an escape hatch)

one question regarding totality checking is, "what about games and webservers, which WANT their event loops to diverge?". a proposal I've heard for this is that you write your program to make a "single step in computation", such as, say, performing a single game tick or responding to a single request. then it's the runtime's job to put this "step" function into a loop. this way you can still have partiality where appropriate, BUT that partiality is pushed allllll the way to the top of the program. (same with how Monads push effects to the top of the program)

this is, like, cutting edge stuff. i personally don't know of any language, or even library, which implements this. EXCEPT CSS!

see, CSS has very low computational power, but in fact you can use it to simulate a single step of rule 110. Rule 110 is turing-complete. in other words ... CSS is a total programming language which, if attached to a looping runtime, would become turing complete. in effect CSS accidentally implements the aforementioned architecture

take that, idris!


You must log in to comment.

in reply to @Quelklef's post: