Lambda the Ultimate

To me, the awkwardness of monads appears to be a special case of the awkwardness that arises from all static type systems because they force the programmer to deal with the computer's way of doing things

How do monads in particular (and I guess static type systems in general) force programmers to deal with "the computer's way of doing things" and what does that mean exactly?

Consulting my Intel manuals, I haven't found any reference to monads. Other than some very simple primitive types (e.g. 32-bit unsigned ints), I don't see anything like the type systems I'm familiar with mandated by hardware.

Abstractions are great, but eventually things need to connect whether they're bits of ethereal logic, gears and timing belts, molecules at a cell membrane, etc.

Not knowing an ideal way to articulate this, I'll start in and we'll see how it goes.

I've been very interested in what makes sapient minds (that would be us) different from non-sapient decision devices (formal systems, technological artifacts). It's struck me that we have, really, no standardized test for sapience (the Turing test is... I'm tempted to glibly say bunk, but perhaps we needn't go further than naive). It's in the nature of sapience, and of technology, that in the long run there should be no standardized test on which technology cannot outperform sapience, for the simple reason that well-defined problem domains are exactly where technological arficacts excel. Sapience is needed when the problem isn't well-defined; it judges whether a formal set of rules is solving the problem, when to step outside the rules, what to do once outside them. (In my blog post on the difference between sapience and non-sapience, I discuss indirect evidence that there is such a thing as sapience; that's a bit much for here, though.) One of my theses is that none of our technological artifacts even remotely approach sapience; yes, I include machine learning in that judgement. It seems pretty straightforward to me that one oughtn't expect sapience to be formally more powerful than formal logic, but that's formal logic's home turf; sapience should only be practically more powerful (the difference between theory and practice being, as the saying goes, small in theory but large in practice).

In exploring why mathematics is so much more facile than our programming languages at building abstractions, I've arrived at the assessment it's because mathematics is a conversation between sapient minds, whereas programming is a sapient mind trying to explain something to a computer that, being non-sapient, can't ever understand anything. (Cf. Philip Guo' post on The Two Cultures of Computing.) Basically, we try to play the computer's game by the computer's rules, and give up our advantages in the process. One might hope to import the flexibility of mathematics into programming by creating a programming language where programs are pure math (<cough>Haskell</cough>), but the attempt fails because (to borrow a choice phrase from the blog post I linked earlier), the extreme rigidity of programming doesn't come from the character of what we're saying — it comes from the character of what we're saying it to.

An alternative strategy is to design a programming language to minimize conversation with the computer, so that programming is expansion on a few simple rules from which unconstrained possibilities blossom; rather like the way an alphabet can give rise to literature. Vast open domains like that are where sapience flourishes. This is what Lisp does, in its essence. I'd been perplexed for some time because, although I felt the simple Lisp evaluator was key to Lisp's longevity, and I felt other key features like garbage collection and bignums felt right in the design, I couldn't explain why they should belong in the same language design with that evaluator. Until I realized the simple evaluator, garbage collection, bignums, they're all about minimizing the conversation with the computer.

Big complicated static type systems seem to me to be a prime example of forcing the computer's perspective onto the sapient programmer.

I see this the same way, but come to almost the opposite conclusion. Mathematics has a big problem with inaccuracy, lazyness and assumptions. For me the attempts to give mathematics a formal grounding like type theory are welcome. Finally we can have computers check proofs, so we do not have to rely on hand-wavy appeals to the reader to fill in the gaps.

Recently I moved from JavaScript to TypeScript for web development, and it is so much better I won't be going back. The type system really helps write reliable code with meaningful and consistent interfaces.

Then again I have never liked Lisp, so perhaps this is to be expected :-)

My conclusion is that there is not one kind of programming mind, that different programmers prefer different ways of working. Sapience is not one dimensional, and for some of us type systems are perfectly sapient, infact we prefer them to languages that lack types.

Oh, sapience definitely isn't one-dimensional; I'm familiar with three dimensions that have, in combination, huge impact on thinking style (none of which is "intelligence"; I'm not a fan of intelligence tests).

To be clear, when I say mathematics is a conversation between sapient minds, I'm not talking about inaccuracy, laziness, or assumptions.

I do feel there's something, in need of further elaboration, to the point I'm making about the difference between sapience and non-sapience, that isn't just a matter of style. Granting, there's a profound difference between cognitive styles (when studying this stuff in the old days, I didn't fully appreciate why the Gordon-Morse material called it cognitive "style" rather than cognitive "type", but I'm getting that now: it may be a consequence of underlying properties of the mind, but what really matters about it is the consequent pattern of behavior, which is quite complex compared to the underlying properties). One thing that had occurred to me some time ago was that different cognitive styles are likely best served by different kinds of programming languages. I don't think one can get away from the fundamental difference between people and computers; the specific sort of relation between the two that fits particular cognitive styles seems a more complex thing. The particular technique through which I approached the matter was, after all, abstraction, which is itself something not all cognitive types(!) are well suited for.

design a programming language to minimize conversation with the computer

As far as I can tell, describing a concept with a minimal conversation requires exactly one condition: a common foundation. In humans, this foundation is our domain knowledge. In computers, this foundation takes the form of libraries. Either way, to describe a sophisticated concept or application with a few sentences requires both parties share a foundation. Even humans cannot learn something until they already almost know it.

We can easily design languages where "programming is expansion on a few simple rules from which unconstrained possibilities blossom". But a few simple rules will never give us a foundation of domain knowledge. We need a full ecosystem for that!

If we're to discuss human-oriented vs. computer-oriented conversations, I think the greater issue is that programmers are speaking in terms of the computer's foundation, by directly invoking those APIs. How can we let humans program in human terms?

DSLs can help, enabling humans to use familiar domain-knowledge terminology. Generally, support for ambiguity and deferred resolution thereof can help because humans like to say ambiguous things.

Those features do seem an awkward fit for common type systems. But it isn't clear whether the better answer is to abandon type systems or develop one that fits. I know your choice, but I suspect you're generalizing too much without a proper discussion of alternative type systems (#notalltypesystems).

Er. When I said minimize conversation with the computer, I didn't mean compress the communication with the computer as much as possible, I meant arrange, as much as possible, to converse with other people rather than with the computer. However, I see you've arrived at an interesting thought...

a few simple rules will never give us a foundation of domain knowledge. We need a full ecosystem for that!

Absolutely. Yes! In relation thereto, the phrase programming idioms comes to mind. (Not where I was trying to go with the metaphor, but an interesting place to go with it nonetheless.)

A worthy body of literature is the product of a flourishing culture.

Those features do seem an awkward fit for common type systems. But it isn't clear whether the better answer is to abandon type systems or develop one that fits. I know your choice, but I suspect you're generalizing too much without a proper discussion of alternative type systems (#notalltypesystems).

I was a believer in type systems for a long time, always hoping for great things from the type-system innovation around the next corner. After enough disappointments, I came to expect new and different problems around each corner, losing faith in the whole strategy. At that point I wondered if there was some radically different strategy one might try; after all, there are languages that don't have complicated static type systems at all and get along inexplicably well; they have yet a different set of problems with their strategy, and I noticed that the experience of doing serious mathematical research is something different again, not really like either the "static typing" or "dynamic typing" experience. So now I'm trying to find a new way. Some days it seems more hopeful than others.

I was a believer in type systems for a long time, always hoping for great things from the type-system innovation around the next corner. After enough disappointments, I came to expect new and different problems around each corner, losing faith in the whole strategy.

This same description applies to mathematics as a whole, and yet mathematics has somehow escaped being equally disappointing as static typing in your mind (how many proofs were ultimately flawed, how many conjectures have withstood analysis for centuries, etc.).

Perhaps you just face static typing more frequently and so familiarity breeds contempt, rather than mathematical progress being somehow "better" than progress in typing?

Some scattered thoughts on that.

• My general attitude to these sorts of explorations is to broaden the range of options we're exploring, rather than to cut off anyone else's vein of exploration in favor of my own. At a preliminary stage, anyway. I tend to explore admittedly oddball ideas, and those who explore oddball ideas tend to favor letting others pursue ideas incompatible with their own.
• 'Twas more a summary description of my experience than a robust defense of the conclusion. My reaction to my experiences is an intuition based on rich context, surely including stuff too subtle to describe or even consciously identify.
• Mathematics is, to my mind, a far more general thing than static type systems. Moving past that to embrace the analogy, mathematics has overall produced tremendous and spectacular successes, which is not my own experience of static typing; it seems to me the further into the static-typing strategy one gets, the worse the red-tape problem gets, which might recommend a reconsideration of doubling-down on something that isn't working well.

Moving past that to embrace the analogy, mathematics has overall produced tremendous and spectacular successes, which is not my own experience of static typing

I'm not sure comparing a field that's literally taken millennia to achieve its tremendous and spectacular successes can be used to fairly evaluate a field that's had maybe 60 years of development.

Nevertheless, type systems have also achieved some pretty impressive results in that short time frame all the same, such as algebraic types and pattern matching, parametric polymorphism, effect typing, dependent types, and type inference.

which might recommend a reconsideration of doubling-down on something that isn't working well.

"Isn't working well" seems like a rather subjective judgment. It seems to work quite well for many people, and where it doesn't, it seems to reflect the inherent difficulty of the goals being pursued. Maybe there's something better to use at those fringes, but I'm not sure fringe cases can justify the claim that typing isn't working well overall.

+1

A few remarks.

I'm not sure comparing a field that's literally taken millennia to achieve its tremendous and spectacular successes can be used to fairly evaluate a field that's had maybe 60 years of development.

Just to remind, I'm not the one who recommended an analogy with mathematics. I think comparing static typing with mathematics is like comparing a canal with an ocean (the former is artificial, highly specialized in its purpose and uses, and vastly smaller). I did want to point out, while we were on that analogy, though, that it seemed to me there was a much clearer case for mathematics than for static typing. (Note, however, that early on it was quite possible for intelligent folk to doubt mathematics; Aristotle, as I recall, was not much of a fan, which kind of skewed the track in Europe for some time.)

type systems have also achieved some pretty impressive results in that short time frame all the same, such as algebraic types and pattern matching, parametric polymorphism, effect typing, dependent types, and type inference.

A fair list, if one is making the case in favor. I'm a skeptic; I'm ambivalent about a lot that's on that list. I might allow polymorphism, although it seems to me to have gotten overly baroque.

"Isn't working well" seems like a rather subjective judgment.

Whether one thinks it's working tends to vary from person to person. Perhaps you mean that whether it is working can vary from person to person. I take you to be suggesting that for some people it mostly works; yet, I could wonder whether even some of that is partly illusory; could it produce satisfaction in those using it while also creating some limits on what they do that they may be unaware of? At any rate, note also my first point above, that I generally advocate exploring more different options rather than exploring one to the exclusion of another.

the awkwardness of monads appears to be a special case of the awkwardness that arises from all static type systems because they force the programmer to deal with the computer's way of doing things

In my experience, the awkwardness of static type is essentially this: our type systems cannot perform the same inferences or reasoning a programmer can. Outside of simple tree data structures, it's difficult for types to describe our intentions or verify our assumptions.

OTOH, static analysis can guard against other forms of awkwardness, such as missing silly mistakes, protecting performance assumptions, or writing tons of tests. I prefer the awkwardness of static types. But if we can develop alternative, accessible forms of static analysis that are adequate and better align with my reasoning, I'm very willing to try them. Perhaps something similar to SHErrLoc.

It seems like an AI-complete problem to provide a general proof-reader. But perhaps we'll get there in the next few decades.

the awkwardness of static type is essentially this: our type systems cannot perform the same inferences or reasoning a programmer can.

I've a feeling there's some shortfall in that account. The limitations of static typing seem to me to be inherent in the overall structure of the system, so that more sophisticated types, or inferences on them, wouldn't actually help, and would likely make things worse. That overall structure is itself ponderous; it feels like bureaucratic red tape. Mathematical reasoning is much more fluid. So when one says "our type systems cannot perform the same inferences or reasoning a programmer can"... just changing the types, or the inferences, isn't going to do it. The whole way it engages the program has to change. And I don't think an artificial intelligence would be an improvement; on the contrary, I would expect it to make things much worse. I reckon so-called AI does not resemble sapience whatsoever. I don't think we're even trying to make our technology sapient, because I think we're clueless about what that even means. However, I do think it's becoming alarmingly common now for technologists to mistake what they're creating for sapience; I think we're much less likely to build sapience than we are to destroy ourselves by giving up our own sapience for the sake of our technology.

If we ever did build a sapient programming interface, programming would be a matter of negotiation with the system, and then the system would be... a programmer, with the same problems we're having now. (I may have mentioned before, somewhere on ltu, the incident about three decades ago when someone told me there was no point in designing programming languages because in a few years all computers would be self-programming, and I told them if computers wrote programs they'd want a really good programming language.)

Mathematical reasoning is not more fluid on the basis of being untyped. Matrices, graphs, groups, sets, many sorts and types are involved. However, in math we aren't as attentive to types because we aren't paying for them. We can use any existing lemma in our proofs without worrying about the costs of converting types through isomorphisms.

In programming, disabling static safety allows us to write programs that couldn't be understood by the existing static analysis. However, humans think in predictable patterns (many flawed), so we'll only correctly use a limited volume of this extra freedom. Insofar as humans have freedom to express those programs while still supporting static analysis, most won't feel it's red tape, just part of explaining the program to a computer or other humans.

Aside: The "static" stage of a software computation is simply whenever a programmer edits code. For live coding or interactive programming, this stage never really ends - even end-user input or bot contributions to a blackboard might be modeled as editing code. There's much benefit to designing a language that is robust, resilient, and efficient even without static analysis, i.e. where static analysis is an auxiliary feature so we can recognize and correct a flawed or fragile software system, and protect performance assumptions in isolated modules, rather than an entangled requirement to even begin evaluation.

Matrices, graphs, groups, sets, many sorts and types are involved.

That depends on what you mean by "involved". Hence my remark about how the types are engaged. Similarly with the first statement, where the tricky bit is what exactly one means by "being untyped"; again, the substantive issue underneath is how the types are engaged.

humans think in predictable patterns (many flawed) [...]

One could pick on that word "predictable", but I'm more interested in the bit about flaws.

Sapiences make mistakes. So do computers; but computer mistakes and sapient mistakes have profoundly different characters. The nature of computer mistakes is shaped by the fact that for computers, nothing has any meaning (so, amongst other things, it takes sapience to judge whether something is a mistake). Human-bashing has gotten fashionable, ultimately driven by economic forces; we judge ourselves by the standards of what we find admirable about machines —which we find admirable partly because those features are things we don't share— and of course we find ourselves wanting; given a human and a machine, which would one expect to exhibit more machine-like precision?

My scientific background didn't prepare me very well to expound the virtues of humanity; I suppose one might consult Shakespeare, or perhaps Gilbert and Sullivan. Here's some food for thought, though. Genetic evolution, which is based on an essentially digital medium, has been underway on Earth for three or four billion years, and reached a tipping point where it kicked into high gear about 600 million years ago with the Cambrian explosion. By my reckoning, memetic evolution, based on a sapient medium, has been underway here for about three million years, and reached its tipping point where it kicked into high gear about 40 thousand years ago with the Upper Paleolithic onset (blossoming of art and technology). Suggesting memetic evolution is about three orders of magnitude faster than genetic evolution.

the substantive issue underneath is how the types are engaged

I argue that static typing and mathematical reasoning engage types in essentially the same manner. The substantive difference is the cost of engagement, and consequently our relative reluctance to manipulate types in programming.

In mathematical reasoning, converting a graph to a matrix based on a previous proof is a O(1) step. In computation, it's at least O(N). In mathematical reasoning, a Cartesian product of sets is a O(1) step. In computation, it's O(M*N). Computation is mechanical, subject to physical constraints.

You say mathematical reasoning is more facile. I agree. But I don't agree with the reason you've given, that this is a consequence of static typing.

the tricky bit is what exactly one means by "being untyped"

No. My argument doesn't hinge on a precise definition of 'untyped'. After all, I am arguing that typing is NOT the substantive difference.

But I am willing to clarify: by my understanding, a 'type' (noun) can feasibly be any compositional property. By compositional, I mean that we have a function that computes the property of a composite in terms of same property for each component - e.g. P(X*Y)=F(P(X),P(Y)). A property is 'typed' (adjective) if it's a type and it's checked. A property is 'checked' if computed and verified to be within expected constraints (whether by man or machine). An untyped property, then, is simply any property that is not typed (that is, not compositional or not checked).

Compositionality is what allows types to work at interfaces and module boundaries, hiding implementation details. It's a convenient property for humans, who have a limited working memory, and for human communities, since it enables a division of labor. It's arguably a very "human-oriented" property, considerably less relevant to a machine that can unerringly process many gigabytes of code or proofs in less than a day.

In mathematics, our ability to reuse proofs as lemmas in later proofs is only possible insofar as the proven properties are compositional. Hence, there is tight correspondence between non-trivial mathematical proofs by humans and type-checked programs. ... Modulo performance and some non-computable axioms (like axiom of choice).

The nature of computer mistakes is shaped by the fact that for computers, nothing has any meaning

In computation, names or numbers have meaning insofar as we associate them with other values in the context. I would reword your statement to say instead that the 'context' accessible to a computation is usually a lot more restrictive than the 'context' accessible to a sapient. And 'accessible' here should be understood in a practical sense: even if a computation downloads pages from Wikipedia or peeks through a camera, the information within might be inaccessible, opaque.

But even if we integrate our human context with a computation, including visual recognition and pop culture and kitchem sinks, I think the difference in biases and motives would still result in behavior and flaws that diverge from what a human would do. Even if the machine were 'sapient' by some metric, it'd still be an 'alien' sapient. Human players who lost to Alpha Go came called it "alien" to the press. And that context is a tiny 19x19 canvas. If it were a broader context like mathematical proofs or city layout, it should be even more alien to us. Would humans really understand these proofs or cities without learning to think like the alien sapient machine that produced them?

So to get the rest of the way, we need to encode our human biases and motives into the machine, e.g. using a weighted logic where weights are based on our preferences or biases. This is something I was describing in my earlier 'human-oriented vs computer-oriented' post.

Suggesting memetic evolution is about three orders of magnitude faster than genetic evolution.

I imagine this has a lot to do with the medium. Virtual life models can evolve a lot faster than human ideas or designs. Horizontal gene transfer (HGT) has evolutionary characteristics similar to memetic transfer.

I've read a fictions involving a massive industrial accident with tons of a CRISPR-like molecule in New Zealand, causing 'evolution' (with HGT) on a widespread scale. I've read fictions involving near-immortal authoritarians gaining power then holding it for millions of years, resulting in cultural stasis. Clearly, we can imagine scenarios where genetic evolution speeds up or memetic evolution slows down.

We're evidently not finding common referent concepts to match up. I talk about meanings, your talk about definitions, and that seems to be at the heart of the difficulty. Tellingly, when I say "for computers, nothing has any meaning", you respond by talking about associating names and values, which is mechanical association and doesn't involve meaning in the sense I... meant.

AFAICT, meaning is by nature associative. Definitions, connotations, the 'meaning' I give to life. Meaning isn't something intrinsic to a sound, word, event, condition, or object. Meaning only 'exists' insofar as an observer will grant/assign it. If the observer is a computation, then it's naturally the computation that gets to grant a meaning.

I'm now curious what meaning you give to 'meaning'. Maybe something closer to an intrinsic "form determines function" or "the purpose of a system is what it does"? Something way different, or just subtly different?

I distinguish sapient minds from non-sapient devices. Formalisms are on the non-sapient side. Meaning is the province of sapience, and accordingly any attempt to treat meaning formally is doomed to fail. So I'm not going to try for that. But I'll try to talk around it, and perhaps I'll find my way to something useful.

The difference between the sapient and formal sides of this distinction, btw, is not something I expect to be able to define formally. I tend, actually, toward reductionism: I don't claim there's anything "mystical" about the human mind that doesn't, in theory, arise from the basic physical constituents of the human nervous system. But (as I remarked in a blog post about this, earlier this year), in practice sapience is a profoundly different thing; the difference between theory and practice being, as the saying goes, small in theory but large in practice.

In the early twentieth century, with a crisis in the foundations of mathematics, Hilbert proposed [using] a metamathematical technique that (as I understand it) allowed formal techniques to be applied to studying the problem without making prior assumptions about the nature of informal mathematics. We start with informal mathematics that we want to study; the substance of that is thought, on the sapient side of the divide, and in a foundational crisis we have to assume we haven't got a clue what that is. We'd really like to use mathematics to study the problem, but mathematics only studies formal systems — not on the sapient side of the divide, and seemingly the foundations of mathematics had gotten into the fix they were in by incautiously assuming informal mathematics could safely be treated as if it were formal. So we make the minimal assumption necessary to bring mathematics to bear: we assume that we've established a connection between the informal mathematics we want to learn about, and a formal system we've defined, such that provable statements in the formal system correspond to true statements in the informal math. The formal system, unlike the informal mathematics, can be directly studied by means of mathematics. And we actually still don't have a clue what stuff the informal mathematics is, but we've made apparently the least assumption that would allow us to use mathematics to study it. I've seen people try to get meaning out of this approach ("model theory"), and that's an example of what I think is doomed to fail: the whole point of the exercise, for me, is that meaning can only exist on the sapient side, in the informal mathematics but never the formal system.

I observe that automatic translation is similarly doomed to fail, because automatic translators treat texts ultimately as strings of symbols. A string of symbols is devoid of meaning; it's just data. It's not possible, in general, to translate a text from one natural language to another without understanding what it means. (Some time back I had occasion to study a news story about some international conference, and the delegate from some eastern-Mediterranean country didn't attend; an automatic translation of a source article explained the delegate had been decapitated. Which didn't seem likely... but, that part of the world being what it is, there was just this slight awful doubt. After a great deal of hunting and study, I worked out that the delegate had apparently not attended because he had a terrible head cold — my best guess is that the source passage autotranslated as decapitation was using an idiom similar to English "sneezing his head off".)

When I say that "for computers, nothing has any meaning", I mean that computers just push bits around, rather than thinking about them.

Model theory isn't about assigning philosophical meaning. It's been quite successful so I don't know why you'd consider it doomed to failure.

As a branch of mathematics, I've got nothing against it. Afaics, it plays with the same sort of approach as Hilbert was doing, in a more high-powered way, which is all very well except that there's this tendency nowadays to imagine, just because the formal half of the correspondence has now been made quite elaborate (via model theory), that meaning resides there rather than remaining forever out of reach of formalism on the sapient side of the correspondence. That is, people really do suppose that in model theory they're actually working with meaning, rather than its mere formal shadow.

Unless we believe in transcendental signifiers, all meaning reduces to simple correlation at some level of abstraction. Wittgenstein's language games assign meaning as simple labels for objects or actions, nothing more and nothing less. Where people get confused I think is that sometimes the same label gets used in multiple language games, and somehow we come to believe there is some greater significance to this, although there is not. We can see the beginnings of this with homophones, however different spelling preserves the different meaning. If we consider collapsing a homophone, for example 'knot' and 'not' we might get some idea of how expectations of deeper "meaning" are created, however this is just an illusion, our pattern matching capabilities seeing dragons and castles in the clouds.

I imagine, as Keean suggests, that the main difference between sapient and formal systems is just the way they are manipulated, with sapient side allowing fuzzier inferences that come optimized for the types of scenarios people have historically found themselves reasoning about.

I once thought that way. My current position emerged from familiarity with it. Where I am now, I see these as common ways to mistake sapience for something trivial. I blogged on this a while back, "The biggest systemic threat atm to the future of civilization [...] is that we will design out of it the most important information-processing asset we have: ourselves"; I meant (in part), if we become so distracted by our technology that we judge ourselves by what our technology can do (rather than what we can do), we'll fail to recognize the value of sapience — and lose that value. I really could see this being the answer to the Fermi paradox.

Fuzzy formalism is still formal. '[Reducing] to simple correlation at some level of abstraction' happens only on the formal side of the divide.

I think you probably made a mistake years ago and moved on to grander errors :). But I'm happy to be wrong and maybe we don't want to get into it here! I think the answer to the Fermi paradox is probably going to be the one listed as the first criticism -- the odds of intelligent life emerging can be so small that it dwarfs the size of space and time.

Yeah, our mutual goal is presumably to help each other, and others following this, to understand better where we're coming from, and thereby understand the underlying issues better.

Re the Fermi paradox, of all the factors in the Drake equation I think the three most likely to seriously curtail the product are the fraction of planets capable of supporting life that actually develop it, the fraction of planets with life that develop intelligence (I'd call it sapience), and lifetime of high-tech civilizations. I'd hesitantly entertain either of the first two, but the only instance we know about in detail is already past those. I'm concerned that once sapience develops something like the internet, it collapses into non-sapience; that is, that the internet catalyzes a process that causes the entire civilization collectively to cease to think.

Re formalism versus sapience, well, I do have one additional angle on that to offer (with some pieces to it). Over the years I've become something of a specialist in (amongst other things) recognizing and avoiding conceptual traps.

• I have long been, and am, a disbeliever in what one might call mystical thought — or perhaps anti-reductionism— the notion that thought is fundamentally beyond logic/formalism. This school of thought seems motivated by a perception that there is something ignoble about sapience that emerges from "mere" mechanical/non-sapient interactions. (Misplaced perception, I think, because it seems to me just as legitimate to view the mystical route to sapience as essentially pnambic —pay no attention to the man behind the curtain— and thereby ignoble, while perceiving the vision of sapience emerging from non-sapience as downright breathtaking.) The current fashion in mystical thought, in the past half century or so, is to claim that the mystical element somehow comes in through quantum mechanics, a notion I associate with David Bohm (although I see the Wikipedia article about it doesn't even mention him). The mystical-thought approach seems to me to violate Occam's razor, introducing new elements as a basis for sapience when ordinary elementary physics ought to suffice per reductionism.
• However, I also see a conceptual trap in what one might call anti-sapience, a belief that sapient thought is an irrelevant illusion. This school of thought seems motivated by a self-loathing trend in popular culture, a desire to believe that human beings are ignoble (ironic, since the anti-reductionism trend was motivated by desire to believe the opposite); it has roots in both radical environmentalism and technology-worship, and has a strong economic incentive behind it (which suggests to me a fundamental flaw in our economic system). From a conceptual perspective, its fundamental flaw is insisting on addition of an unnecessary assumption that sapience must be trivial; or, worse, hiding that assumption by adopting it implicitly.
• A basic technique, for thinking one's way out of conceptual traps, is replacing an implicit assumption by an unknown conceptual factor, so that one's thinking isn't restricted in any particular direction by it. I realized, recently, that Hilbert's approach to meta-mathematics, in its pure form, does just this, studying mathematics by formal means without making any unnecessary prior assumption, one way or another, about the nature of informal mathematics. Another key insight here is that reductionism is not an obstacle to nontrivial sapience; there are a couple of ways to view this. One is the observation, which I mentioned earlier, that the difference between theory and practice, while small in theory, is large in practice; a popular term for this nowadays is "emergence". Another is that if the informal (sapient) approach offers anything that the formal does not, one should fully expect that this additional offering would not be formally demonstrable. This fits very well, I've noted, with the familiar limits on computational and logical power. The Church-Turing thesis, limiting computational power, is an inherently informal thesis. And while Gödel's Theorem (yeah, I'm treating it as if it were singular) is a formal result about the limits of formal systems, if sapience were effectively (that is, in practice) more powerful than any formal system, one would fully expect to be unable to prove that formally. (When blogging about that, I was reminded of the vignette from Revenge of the Sith where Anakin asks Palpatine "Is it possible to learn this power?" and is told succinctly, "Not from a Jedi.")

I'd hesitantly entertain either of the first two, but the only instance we know about in detail is already past those.

This sounds like "intelligent life already happened so its probability can't be too low" which seems wrong to me. We're here observing it only because it happened, so the probability could be arbitrarily low.

Your characterization of anti-sapience seems to miss the middle ground, of the mind as an amazing computer which we haven't yet figured out how to emulate.

I'm not sure that I follow your last bullet. I know that some (https://www.iep.utm.edu/lp-argue/) have interpreted Godel as implying that the human mind can't be emulated by a Turing machine, but I (and I think most mathematicians) view this as a flawed interpretation. And Penrose going on to speculate about microfibers in neurons somehow being quantum antennae that give humans super Turing abilites definitely has that mystical feel you mentioned. I think the situation is fairly straightforward: a human mind cannot understand the correctness of human reasoning in its most general form (at least at a fixed level of credence). So if you provided a mathematician with a Turing machine producing all of the true statements he could himself produce, he would not be able to judge it to produce only true statements. You might imagine that someday we could understand the human mind well enough to model it a Turing machine, and this doesn't lead to any contradiction. The statement of its consistency would be a new, unprovable proposition. Trying to incorporate this reflection mechanism into a system that knows it's consistent leads to contradiction.

This sounds like "intelligent life already happened so its probability can't be too low"

No, what I said doesn't sound like that. I observed that, because we have only one example and it's already past the point of influence of those factors, we have no evidence that the factors are especially small. That we also have no evidence they aren't small is irrelevant, obvious, and old hat. Don't be so eager to ascribe naive mistakes to me.

By the time you observe, in your third paragraph, that you're unsure of my last bullet, that's already been made clear by your second paragraph. By my standards, "an amazing computer that we haven't yet figured out how to emulate" isn't a middle ground, it's just the second option ("anti-sapience", or if you prefer "trivial sapience") said with conviction. Apparently your thinking has this dichotomy built into it, that reductionism must be either decisively embraced or decisively rejected; but I've got a stable approach that does neither. A stable approach that does neither: it is entirely content without having to "settle" the question in either of those ways.

I would assume the odds of intelligent life spontaneously emerging from an ocean are quite low, to the point that I dislike the term paradox being applied. But I'm not really sure why we're on to this topic.

I think your second bullet had too much spin on it. I'm open to the possibility that a mind might not be emulable, even in principle, but I don't see any evidence for that position nor any benefit from speculating about it. We got here from a discussion of type systems. Why would a discussion of types need to land us in a discussion about sapience? Surely a discussion of HMI aspects is enough as a practical matter. This jump to sapience has the same mystical feel to me as explaining consciousness through quantum mechanics.

We got here from a discussion of type systems. Why would a discussion of types need to land us in a discussion about sapience?

Fwiw, a bit of a recap: I suggested that programming is much weaker than mathematics because programming is dragged down by languages that force the programmer to negotiate with the computer, which lacks sapience, whereas a mathematician negotiates with other sapient mathematicians. Subsequent misunderstandings and explanations were apparently failing to reach any sort of elucidation, and I concluded the back-and-forth was not being useful because those involved were using incompatible conceptual frameworks, notably breaking down over the concept of meaning. Dmbarbour expressed curiosity as to what I did mean by meaning. I took the question in good kind and meant to get back to it when I had enough time to give it a serious try. When I did get back to it, further discussion has led us to where we are now.

Re my premise: Lisp in its pure/simple form (ala Scheme), I note, uses the sort of approach I'm describing; it simplifies the language model that the programmer deals with, in ways that avoid negotiation with the computer, instead providing a simple unconstrained framework that can be used as a matrix by sapient minds; in rather the same way, it seems to me, that an alphabet can provide a matrix in which for sapient minds to develop literature. Haskell was created, afaics, by folks familiar with the power of mathematics who were hoping to bring that power to programming by limiting the language to traditional mathematical structures — but, as I see it, they imported traditional mathematical structure into a traditional computer-oriented programming milieu, and the problem was the traditional programming milieu that they kept, not the absence of the traditional mathematical structures they imported into it. Another way of viewing the divergence of these PL design philosophies is that most "modern" languages try to achieve extensibility by adding constraints, whereas Lisp achieves its extensibility by removing them.

I'm concerned that once sapience develops something like the internet, it collapses into non-sapience; that is, that the internet catalyzes a process that causes the entire civilization collectively to cease to think.

Perhaps their thoughts become consumed by so many hedonistic temptations that biology shaped by competition and scarcity are poorly suited to resist them. That certainly seems like a powerful driver in numerous behaviours we see today.

The current fashion in mystical thought, in the past half century or so, is to claim that the mystical element somehow comes in through quantum mechanics

Interesting! I had never heard that Bohm had collaborated on theories of mind before. The description of holographic-like memory is interesting. There doesn't seem to be anything magical or pseudo-scientific about his approach to consciousness though, and he doesn't seem to assert any need for quantum effects in consciousness, although his holistic approach seems fairly comprehensive so it's probably hard to so trivially summarize. Thanks for the new info though!

if sapience were effectively (that is, in practice) more powerful than any formal system, one would fully expect to be unable to prove that formally.

Indeed, but then we should expect to find some conclusive evidence of this, so we should remain skeptical.

we should expect to find some conclusive evidence of this

Perhaps, given we're talking about something inherently non-formal, we should rather expect to find some inconclusive evidence. Or something persuasive but not cut-and-dried enough to call evidence.

I mentioned some time back in this thread, something I find rather persuasive in this regard (though dmbarbour, judging by their response, was spectacularly unimpressed). Memetic evolution differs from genetic evolution in, I submit, three notable ways (amongst others). First, the replicative medium for genetic evolution is chemical, while for memetic evolution it's a population of sapient minds. Second, the observable copying of basic information for genetic evolution is of incredibly high-fidelity, whereas for memetic evolution it's —observably— of quite low fidelity (the classic game of "telephone" demonstrates). I suspect that high/low-fidelity difference was what prompted Richard Dawkins to assume, when first describing memes, that they were "still drifting about clumsily in their primeval soup". I think he was not just wrong about that, but hugely wrong and got the whole field of memetics started off on a wrong foot from which it still hasn't recovered. It's an understandable mistake; the appearance of low fidelity follows from the nature of the sapient medium: any information that a sapient mind directly apprehends will be thought about, because, well, sapience, causing a high rate of mutation. Evolution admittedly requires high-fidelity replication but doesn't require observers to be able to readily pin down what is being high-fidelity-replicated. And it seems that something about sapience enables memetic evolution to function in a different and profoundly more powerful mode, producing the sort of super-high-fidelity fixpoints needed for evolution without the fussy brittle sort of high-fidelity base-level copying used in genetic evolution, thus saving vast amounts of time. Because memetic evolution isn't in anything like its primeval soup stage; rather, for many thousands of years we've had highly sophisticated memetic organisms, with differentiated organs and advanced reproductive processes. There's even a very famous book that's all about the reproductive process of a species of memetic organisms: Thomas Kuhn's The Structure of Scientific Revolutions. As I've explored the early development of human thought, I've concluded —and this is the third "notable difference" I have in mind— that memetic evolution isn't just modestly faster than genetic evolution, it's about three orders of magnitude faster — genetic evolution has been underway on our planet for maybe three billion years, and kicked into high gear (as evolution tends to do after a while) about 600 million years ago, whereas memetic evolution has been underway for maybe three million years (or less), and kicked into high gear about 40 thousand years ago.

I'm thinking, with such a profound difference in evolutionary properties between a non-sapient medium and a sapient medium, it suggests a profound qualitative difference between sapience and non-sapience.

It's an understandable mistake; the appearance of low fidelity follows from the nature of the sapient medium: any information that a sapient mind directly apprehends will be thought about, because, well, sapience, causing a high rate of mutation.

Definitely some interesting connections, but I would attribute the low fidelity to the low stakes. If the stakes were high, as they are with gene copying in a multicellular organism, then high fidelity will emerge because it's adaptive, and low fidelity processes will simply die off.

The fine details of most memes simply aren't important, as long as the core principles are preserved. You could argue that differentiating the core principles from the irrelevant details thus requires sapience, but it seems equally plausible that inferring the incorrect core principles from a meme would lead to untimely demise. Thus, only memes whose core principles are largely intact persevere (as will those who can do so correctly).

Edit: this possibility might seem to contradict the "low-stakes/low-fidelity" classification, but if we accept that every meme has adaptive and non-adaptive qualities, then low fidelity on the non-adaptive qualities, which probably outnumber the adaptive ones, would make mutation mostly harmless, and thus low fidelity is allowable. Only when the smaller set of adaptive qualities changes is there danger.

I'm thinking, with such a profound difference in evolutionary properties between a non-sapient medium and a sapient medium, it suggests a profound qualitative difference between sapience and non-sapience.

I agree there is a large qualitative difference: the energy required for replication and the largely low stakes of mutation. This probably permits mutations to continue to diverge and potentially find new maxima or mimima that would require considerable (and uncommon) environmental upheaval to see the same in genetics.

You seem to be using "adaptive" to refer to how much the meme benefits people rather than how much the meme benefits itself.

I studied linguistics because memetics wasn't offered as a course of study. What I found out is that one of the fastest ways for a meme to spread is if it is used to distinguish OUR kind of people from the other kind. (This is why products sell better when they are sold in men's and women's versions) Or as sign that you're part of a particularly privileged group. In this niche what looks like a high rate of mutation is probably a low rate of mutation combined with a selection pressure for distinctness.

Memes also spread much faster when they deputize a person to go out and correct a widespread erroneous co-meme. (grammar pedantry, anti grammar pedantry, etc). I don't know why this is so effective but I get very antsy and compelled to spread a meme when I know that there is someone WRONG on the internet.

You seem to be using "adaptive" to refer to how much the meme benefits people rather than how much the meme benefits itself.

Yes, I was taking a longer view since we were discussing the evolution-level timescales. A meme that benefits itself at the expense of people that spread it would quickly die out because the people would die out. You raise some good examples of faster how memes spread faster though. I've definitely noticed them myself.

There are no low stakes involved. Nor is replication ever low-fidelity. Evolution doesn't happen unless replication is very high fidelity; you need high-fidelity replication, competition for resources, and a source of mutation. What isn't necessary is that (1) the mechanical copying process, out where we can see it, be high-fidelity, nor that (2) we be able to identify just what it is that is being copied with high fidelity. The principle of evolution is essentially mathematical; if the conditions for it arise, evolution is the name for what happens. Our understanding is not needed in order for it to happen, and the high-fidelity doesn't have to be at the level where mechanical copying is happening, either. In fact, in memetics, anything that's obvious to us would necessarily not be the replicator, because if it's obvious to us, we would think about it, which is in the nature of sapient minds, and that means we would alter it. The actual replicators, the things copied with high fidelity, have to be there because if they weren't there would be no evolution happening, but they have to be some sort of unobvious fixpoints. And it seems they exploit properties of sapience, too.

But I am willing to clarify: by my understanding, a 'type' (noun) can feasibly be any compositional property. By compositional, I mean that we have a function that computes the property of a composite in terms of same property for each component - e.g. P(X*Y)=F(P(X),P(Y)). A property is 'typed' (adjective) if it's a type and it's checked. A property is 'checked' if computed and verified to be within expected constraints (whether by man or machine). An untyped property, then, is simply any property that is not typed (that is, not compositional or not checked).

I don't think this generalizes how most people are using `type`. I would say a type is a piece of data mechanically propagated according to some type rules. The property you're talking about is something like the denotation of the type, and thus a type system can be sound or unsound.

I use 'type descriptor' for an expression that describes a type. I've encountered difficulties in the past with conflating types and type descriptors. It's awkward to say the type IS the descriptor without assuming a 'principal' type and assuming only one type system is applied, as opposed to pluggable type systems.

My definition is from contemplating the limits of type systems under an assumption of modular development of software (which seems fundamental per Conway's law). I'm pretty happy with it, even if it requires some explanation.

Can you explain more why it would be awkward to use `type` to refer to the descriptor without principal types or with multiple type systems? Your concepts seem good. I'm just suggesting tweaking the terminology to be more in harmony with existing terminology. For example, phantom types wouldn't seem to be types under your definition.

A type descriptor is an expression to describe a type. The idea of "principal type" suggests existence of some normal form for this expression. But not all systems of expression are normalizing. And if not normalizing, without a principal type, we may have many distinct descriptions for some types. Further, type descriptors tend to be specific to a type *analysis*. In conventional typed languages, we only have one analysis model so this isn't a useful distinction. But if we admit multiple or alternative analyses, like pluggable type systems, then any given type can have many descriptors.

Phantom types don't directly fit. But I've found many such features can be modeled indirectly as phantom cryptographic signatures or encryption. Basically, we need to move the concept out of the type system and into the program, while keeping it logical (so it's a NOP at runtime). Phantom variables become abstract keys. Then we can model type descriptors that track logical cryptographic status in a compositional manner.

"The limitations of static typing seem to me to be inherent in the overall structure of the system, so that more sophisticated types, or inferences on them, wouldn't actually help, and would likely make things worse. That overall structure is itself ponderous; it feels like bureaucratic red tape."

I've written decades worth of code in both strongly statically typed and completely untyped languages. Once I settle in to using a language, it feels natural enough, and it's at least momentarily jarring to switch to another language with a significantly different type system. I do find it far more straight-forward (predictable) to reason about large systems when there is static typing, but I have successfully worked on giant code bases with no types whatsoever, so it simply a matter of degrees.

That said, I've been working the last few years in a statically typed system with much stronger type guarantees than are commonly available, and I find the static nature of the type system to be quite helpful, even without any IDE support (which is one of the greatest benefits of statically typed languages).

You say that "more sophisticated types, or inferences on them, wouldn't actually help", which I can actually imagine with many existing statically typed languages, because the recursion of the type systems is often limited in arbitrary ways (to simplify the compilers) or ephemeral in nature (to simplify the compilers). What that means is that higher and higher investments of time on the part of the programmer have smaller and smaller (perhaps negative) returns in usability and even readability. (As I wrote that, I was thinking about templates in C++, or generics in C# or Java.)

Type inference is a far different beast than a traditional leaf-to-root type flow. Without type inference, each AST node knows (determines) its own type, without any hints from the outside world, and percolates that information up the node tree. If that type isn't the desired or necessary one, then the parent node either performs an implicit conversion, or there's an error. (I know this model well from experience; 20+ years ago I wrote a Java compiler using this model, and it worked well -- and it's still getting used today.)

Type inference, on the other hand, requires a well-choreographed dance (recursive in nature) across subtrees within the AST. For example, a node may be asked a question like: "If I didn't give you any hints, could you figure out what your type would be? And if so, what type would that be?" Or another question, such as: "If I told you that I needed you to be type T, could you figure out if that is even a possibility, and what hoops you'd have to jump through to make that happen?" And only after a series of back-and-forth "negotiating" at various recursive stages in the hierarchy does the node learn what type it actually is expected (required) to be, at which point it (recursively) organizes itself to be able to provide that type. Since the negotiation is recursive, it allows the tree to "reshape" itself (speaking primarily of types, and not suggesting reorganizing the tree structure itself, although that is a possibility) into the desired result, which is (conveniently enough) the only shape that naturally (or least expensively) achieves the desired result. (Any other condition turns out to be a compiler error.)

it feels like bureaucratic red tape

Having now seen type inference done well (hopefully, done right), I can assert that type inference with a static type system is the opposite of "bureaucratic red tape" from the programmer's point-of-view. It's more like lines on a road (helping achieve order, safety, and efficiency), and guardrails on the sides (preventing the catastrophic).

What is somewhat ironic is how obvious static type inference is in retrospect, yet simultaneously how challenging it is to pick even a single example that illustrates its presence, because it literally disappears (becomes invisible) as a language feature -- that is its very purpose. But if you know languages and compilers, you will understand this question: "What is the type of 0?" It turns out that type inference answers that simple question (perhaps the simplest question of all) in a completely different way than a traditional compiler, and the way that it answers it allows a language to do things you've never imagined before.

I am fond of multi-stage programming, modeling components that adapt to each other through a soft constraint system. This is close in nature to a human conversation, where both parties cooperate to find a sensible shared meaning in the presence of ambiguity. Expression and resolution of ambiguity, together with iterative refinement, seems to be very human-oriented.

Yet, I feel it's awkward to entangle this computation with static type inference. The design principle of separation of concerns would suggest that types and metaprogramming should not be combined into one mechanism. By separating type inference and metaprogramming, we have much greater freedom to extend the set of patterns our users model independently of our static analysis tooling.

Unfortunately, it takes a very sophisticated analysis to grok an ad-hoc user-implemented type negotiation. Fortunately, we can get very far with a simple annotation to defer static safety analysis until after a static computation (template programming, type providers, static assertions, etc.). Such an annotation is convenient for software expressions and assumptions that are valid only in a subset of cases, or which we don't know how to analyze, or where we do know but the analysis tooling hasn't caught up.

I'm not sure how to interpret your comments. I can only assume that you are working from a set of experiences that are sufficiently dissimilar from my own.

One way to picture the type of recursive system that I was describing is to imagine that, for any type Tc, there exist any number of methods by a given name, each of which accepts a sequence of m parameters of type TP1..TPm and emits a sequence of return values of type TR1..TRn, where the choice of m, n, TPi and TRi for each method is independent of every other method, subject to obvious rules of disambiguation.

Given an invocation denoted in the source code with a name and a sequence of arguments, the compiler must determine the type of the target (the object reference whose type implies the set of methods), and so on. With a relatively simple language (C++/C#/Java), the rules for determining the method are relatively straight-forward (for the most part), because each argument evaluates to a type, and thus the set of methods can relatively easily be whittled down to a single choice, or in some cases, an unambiguously "best fit" choice.

In the case of type inference, there is also type information (perhaps a set of possibilities) that may be known at any node within the AST that can impact the type resolution of the deeper nodes. That type information must be pushed down to those nodes, in order to reduce an uncountable set of possibilities into a bounded (though potentially exponential) set of possibilities. In the example above, this is easy to imagine because each argument for the example could be a return from another invocation, whose type is likewise variable, and so on recursively.

Conceptually, information can be flowing down the AST node tree, up the AST node tree, or it may go back and forth as a reducing sub-portion of the tree settles on a "best fit" solution.

A quick (semi-related) example that I've used before:

enum Ordered(String symbol) { Lesser("<"), Equal("="), Greater(">") }

List sort(Comparator? comparator = null)
    {
    Int extent = size;
    if (extent < 2)
        {
        return this;
        }

    function Ordered (ElementType, ElementType) compare;

    if (comparator == null)
        {
        assert ElementType instanceof Type;
        compare = (v1, v2) -> v1 <=> v2;
        }
    else
        {
        compare = comparator.compareForOrder;
        }

    do
        {
        Boolean     sorted = true;
        ElementType bubble = this[0];
        for (Int i = 1; i < extent; ++i)
            {
            ElementType next = this[i];
            if (compare(bubble, next) == Greater)
                {
                this[i-1] = next;
                this[i]   = bubble;
                sorted    = false;
                }
            else
                {
                bubble = next;
                }
            }
        --extent;
        }
    while (!sorted);

    return this;
    }

With each line of code, and each AST node, it adapts its knowledge. So after the “if” statement, in the “then” branch, it knows that the comparator is a “Comparator” (i.e. not nullable) and not a “Comparator?” (i.e. nullable), and then after the assert, it knows that the “List<ElementType>” is actually a “List”. That in turn allows the lambda to infer from the “ElementType” of the the parameter of the function type of the “compare” variable that its parameters are Orderable, and hence it can use a <=> “star trek” / “space ship” comparison operator.

You could generalize your description as: we have unknown types, we have some multiple-choice options that might fit, and we want to make a good choice.

This can be well understood as an implicit soft constraint system: unknown types become constraint variables, available choices provide a search space with alternative constraint-sets, and our heuristics for 'good' choice are encoded as some form of 'soft' prioritized choice (as opposed to 'hard' accept-reject constraints). Then we only need to satisfy our constraints and pick the best answer.

Such systems are familiar to me. But they entangle type negotiation with type inference, which I consider unwise from perspective of SoC and language extensibility.

I'd prefer to hand-implement a monad or DSL for constructing soft constraint models, with ad-hoc constraint variables and weighted alternatives. I can use this to compute the runtime program - a form of multi-stage programming. If it's inconvenient to typecheck the constraint model, I can defer type inference until the later stage.

I think we may not be referring to the same aspect of inference.

A lot of people refer to the ability to omit types altogether (e.g. parameter and return types) as type inference; that is not the aspect of inference that I was referring to, and as a result, I probably confused the conversation.

I'm referring specifically to the ability of an AST node to infer its type both by what its parent node communicates, and also (inter-related with the communications from its parent) the responses to questions that it receives from its own child nodes, combined with a dynamic context that reflects the various aspects of type assertions (implicit or explicit) that have occurred in order for a node to be reached.

Some of the concepts that I am describing are present here: http://wiki.c2.com/?TypeInference

I am not fond of Multi-Stage programming. My opinion is that generics can provide equivalent conciseness bit with much better readability, and understandability. An algorithm that outputs another algorithm is very hard to debug, because you cannot see the generated algorithm easily, and it's hard comprehend all the possible generated algorithms to reason about their correctness. If instead of abstracting over algorithms, we abstract over datatype, we can stick to simply expressing the desired algorithm (sort, rotate, partition, filter, group etc) and abstracting over the type of data.

Another point is I think what makes monads hard is the fact that they don't compose, nothing to do with static types. A single row-polymorphic monad seems a much more usable option. The problem is you cannot stop people declaring their own monads, which makes me think a slightly different approach is needed.

Edit: To expand on the monad point, the problem is that 'wrapping order' matters. We end up with layers which then require monad transformers. We could see the problem originating with re-entrance and recursion. What if instead of a stack model, we have an environment (dictionary) model, so variables get added to a dictionary instead of pushed onto a stack. Now something like a monad will compose (providing they use unique names, so we can path qualify variable names to avoid collisions). The drawback is that we have to manually manage the stack, which might turn out to be a problem, but I think language like this might be worth playing with. In other words it may not be Monads that are the problem, but the underlying calculus.

hard to debug, because you cannot see the generated algorithm easily

I chose to fix this issue via rewriting semantics. But I grant it's a problem for conventional languages.

it's hard comprehend all the possible generated algorithms to reason about their correctness.

If it's static, this isn't an issue. It is sufficient to reason about specific algorithms, so we can simply defer analysis. For runtime staging, we would need more sophisticated types to reason about correctness: GADTs or full dependent types.

generics can provide equivalent conciseness bit with much better readability, and understandability ... instead of abstracting over algorithms, we abstract over datatype, we can stick to simply expressing the desired algorithm (sort, rotate, partition, filter, group etc) and abstracting over the type of data.

Simpler is indeed better, assuming it covers your use case. I also favor simpler models for data generics.

what makes monads hard is the fact that they don't compose, nothing to do with static type"

Right. Monads are awkward to compose even if dynamically typed.

If it's static, this isn't an issue. It is sufficient to reason about specific algorithms, so we can simply defer analysis.

But you still have to write the algorithm generator. Debugging that code case by case seems problematic even if it’s easy to debug each case in isolation.

Most compilers, even for strongly typed languages, have a similar issue: we don't have a strong guarantee that the AST or intermediate code preserves type or behavior. If we have a program generator that produces programs that can be analyzed, we're already much better off.

A generator algorithm or compiler function can still operate on a simple AST and perform its own ad-hoc static analyses without integrating the host type system. But if you feel the need, GADTs can model a typed AST.

You have in mind tools that manipulate intermediate representations rather than meta-programming of the sort that Keean had in mind.

Your description of a good type system vanishing into the woodwork seems to be much like what I observe in mathematics — what works with what is always there but just comes naturally, rarely making itself the center of attention.

Within the type-system milieu, it's bothered me about the principle of type inference that it seems incompatible with a programmer being responsible for the correctness of their code. If I write some code and make sure it works right for a certain range of things, there might be a more general range of things for which the type system can successfully type the expressions, and so the type system may allow what I've written on a range of things that I never intended it to work on, and for which I do not mean to certify that it's correct.

I think what you are saying is (if I may condense it): Ambiguous bad, deterministic good. I tend to employ that law quite widely :-)

Indeed. Also bad, things that can easily be misunderstood. (There's a potential for that, when a facility is meant to avoid saying things explicitly.)

Regarding "human oriented vs computer oriented" codebases, I feel you're not giving those Unison developers sufficient credit.

We can think about software artifacts and environments using a metaphor of physical artifacts and environments. This is a useful human-oriented metaphor insofar as it aligns with human intuitions regarding distribution, installation, and modification of artifacts. Software artifacts are only cheaper to replicate and inspect. Unison favors this metaphor. Each software artifact internally complete, and modification involves opening up the artifact and performing surgery - which only affects that one copy.

Creating a human-friendly 'environment' is left as an exercise to the user. Well, the developers are also working on it. But the language is essentially just a medium for this environment - the atoms and molecules and laws, following our physical metaphor. Rather than "computer oriented", I'm inclined to say Unison is "differently human-oriented", having a different vision and different priorities.

My Awelon project prioritizes user control over the computation environment. I would discourage use of external databases and services, which are difficult for users to inspect, replay, curate, secure, and extend. OTOH, I would encourage our ability to safely and easily share data with another user or a community environment. Different priorities lead me to a different "human-oriented" design - immutable codebase for control and curation, represented as an LSM-trie for lazy, incremental, prefix-aligned synchronization and sharing. Prefixes then correspond to conventional packages or modules, and also to filesystems, forums, or databases.

Of course, that's all low level foundation.

I've given much thought to higher levels of interaction between humans and computers.

Naively, any command shell or console app can be modeled as a simple chat-room shared by a human and a bot. The human can make requests or queries, the bot can respond, automate tasks, perhaps ask some questions of its own. Unfortunately, this model requires humans and bots to each speak the other's language, and it's difficult for humans to observe or control the context or bot.

A vastly superior option is a simple blackboard system. The shared conversational context becomes a first-class value. Users and bots interact only with this shared value rather than directly with each other, and thus may each use their own abstractions. Users can leverage projectional editors over the shared context - widgets to view and edit the context, forms to manipulate it functionally. Bots can simply operate on the resulting structured data. We can extend this for CSCW with multiple bots and humans.

Rather than contemplating 'sapience', the question I've asked is "how do we make this conversational context even more human-oriented?"

When humans converse with humans, there is a great deal of ambiguity that are resolved heuristically through implicitly shared domain or world knowledge or future statements and experiences. If given opportunity, we can note a relevant ambiguity and query. Some ambiguities are never resolved, if they are judged to not make a huge difference. It seems technically feasible to me to explicitly represent the shared world knowledge, ambiguity, and resolution thereof as part of our conversational context, separate from the bot or human. I will need to represent the 'context' as some variant of soft constraint logic environment. Well, a variant where we can collapse trivial ambiguities and focus user or bot attention on the more important queries. I'm still thinking about the details.

Intriguingly, if we build a context this way, we can render multiple 'interpretations' to help a user observe and resolve ambiguities in the context. Like a multiple-choice answer, or a more-like-this. If we leverage an ambiguous context for multi-stage programming, we should support rapid application development with iterative refinement. This is a direction I intend to pursue after I've a sufficient foundation.

In any case, I would tend to frame the question of human-oriented HCI in terms of adequately dealing with ambiguity and unknowns, and sharing partial knowledge, rather than building sapient software. I don't imagine sapience would be necessary or even desirable for most machines.