This article ends in such a funny way, as if the people making dependently typed languages haven’t thought about equality. The issue of equality in dependent types has been such a focus for these folx that it literally gave rise to a branch of mathematics called Homotopy Type Theory, lol. There are huge numbers of papers and people working on variations of equality, and these issues have been a major core focus of dependent type theory research for literally decades. I just don’t get this post at all, it feels detached from the world of dependent types.
But there are other languages and type theories that exist. Languages like those are very much more friendly towards programmers, but equality in the world of research is a very rich and complex topic, and there’s more perspectives on it than there are widely usable languages.
I’m a broken record on this topic, but there’s a ton of non-Unix prior art to learn from. Many minicomputer systems had a separation from programs and commands, with the former being not directly invoked latter being what the user called. For example, with i, programs have typed arguments with validation (including marking secrets which aren’t visible on recall), and you can call up a form (F4 key anywhere) for all the valid arguments and their types. It then assembles the the command arguments for you, then calling that builds arguments for the program (which themselves are typed - you can pass pointers on argv). There’s other good human factors features to take too, such as context-sensitive help everywhere, even for exceptions and errors.
I would love to learn more about non-Unix UI from back in the day. Do you have any good references or links for this? The best thing I can find is a modern video that demos the Symbolics Lisp Machine command line.
Sounds vaguely similar to Nushell. External binaries can be imported as commands, but by default they have to be explicitly run. This frees up some syntax for doing more explicit things with values/variables and makes the completions / help a first class thing.
There is a “GOTO” keyword, but instead of something as prosaic as affecting the internal control flow of the program, its argument is in fact an IP address, and denotes that execution of the program immediately moves from the current machine to the indicated machine.
This of course is mirrored by its sister keyword COMEFROM which, thanks to the distributed nature of GOTO, can redirect any currently executing code on a remote server to be halted and resumed locally.
One of the things mentioned here is Russell’s Paradox and it frustrates me that it’s stated the way it is – by reference to a set of all sets – which is a common way to bring it up. The paradox has nothing to do with a set of all sets, but it persists as a very popular thing to mention. :\
This is a standard practice in Haskell land where they’re called smart constructors: https://wiki.haskell.org/Smart_constructors
This article ends in such a funny way, as if the people making dependently typed languages haven’t thought about equality. The issue of equality in dependent types has been such a focus for these folx that it literally gave rise to a branch of mathematics called Homotopy Type Theory, lol. There are huge numbers of papers and people working on variations of equality, and these issues have been a major core focus of dependent type theory research for literally decades. I just don’t get this post at all, it feels detached from the world of dependent types.
The dependently typed programming languages that I know of today of are:
Do all of those have the same notion of equality?
I strongly doubt it!
But there are other languages and type theories that exist. Languages like those are very much more friendly towards programmers, but equality in the world of research is a very rich and complex topic, and there’s more perspectives on it than there are widely usable languages.
A baffling inability to recognize the consequences of capitalism, instead displacing it onto the tools.
I’m a broken record on this topic, but there’s a ton of non-Unix prior art to learn from. Many minicomputer systems had a separation from programs and commands, with the former being not directly invoked latter being what the user called. For example, with i, programs have typed arguments with validation (including marking secrets which aren’t visible on recall), and you can call up a form (F4 key anywhere) for all the valid arguments and their types. It then assembles the the command arguments for you, then calling that builds arguments for the program (which themselves are typed - you can pass pointers on argv). There’s other good human factors features to take too, such as context-sensitive help everywhere, even for exceptions and errors.
There are a lot of modern “prototypes” too on Unix/Windows
https://github.com/oilshell/oil/wiki/Interactive-Shell
e.g. 2014 article with nice screenshots
http://waywardmonkeys.org/2014/10/10/rich-command-shells
This one seemed cool
https://xiki.org/
I would love to learn more about non-Unix UI from back in the day. Do you have any good references or links for this? The best thing I can find is a modern video that demos the Symbolics Lisp Machine command line.
Sounds vaguely similar to Nushell. External binaries can be imported as commands, but by default they have to be explicitly run. This frees up some syntax for doing more explicit things with values/variables and makes the completions / help a first class thing.
There is a “GOTO” keyword, but instead of something as prosaic as affecting the internal control flow of the program, its argument is in fact an IP address, and denotes that execution of the program immediately moves from the current machine to the indicated machine.
This of course is mirrored by its sister keyword
COMEFROMwhich, thanks to the distributed nature ofGOTO, can redirect any currently executing code on a remote server to be halted and resumed locally.Ah, this is a feature in General Magic’s programming language Telescript.
One of the things mentioned here is Russell’s Paradox and it frustrates me that it’s stated the way it is – by reference to a set of all sets – which is a common way to bring it up. The paradox has nothing to do with a set of all sets, but it persists as a very popular thing to mention. :\