Video on Unison/comparison to Haskell/Monads/distributed computing

https://youtu.be/rp_Eild1aq8

Monads are passé, apparently.

Previously mentioned on ltu rather a long time ago http://lambda-the-ultimate.org/node/5151

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Human/computer strategy

      Links: Unison video; previous LtU post.

Indeed, he's quite matter-of-fact in saying monads are awkward so Unison by preference does something else instead.

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; I'd prefer a programming language that avoids computer-oriented structure in favor of human-oriented structure — a very simple formal model that empowers a profoundly open realm of creativity in much the way an alphabet empowers literature (which I touched on in a recent blog post). Lisp is for me far-and-away the extant exemplar of a human-oriented programming language — though of course it is very much the sort of single-thread language mentioned early in the Unison talk. I'm rather ambivalent about the concept of Unison, as they seem to recognize aspects of the problem —they're trying to simplify dealing with the computer— but they're trying to do it by retreating into the computer's world, adopting a blatantly computer-oriented primary form of the codebase (and even allowing some errors to be fixed by the computer without human intervention, which strikes me as a catastrophically bad idea).

Though their remedy for the single-thread problem is, as I understand it, to adopt a God's-eye view, which seems potentially separable from the computer-oriented aspects that bother me.

How so?

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.

People-oriented programming

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.

Mathematics

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.

Style and substance

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.

re: minimize conversation with a computer

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).

It takes an ecosystem :-)

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

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?

fwiw

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

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.

Well said.

+1

continued

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.

re awkwardness of static types

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

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

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,

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.

re types and flaws and change

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

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.

re meaning

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?

Definition of `type`

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.

Re def of type

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

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.

Type descriptors

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.

It's whatever you're used to

"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.

type inference and metaprogramming

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.

Not sure ...

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.

re type constraint systems

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.

Clarifying

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

Multi-Stage Programming

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

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.

Program generation

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.

re program generation

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.

I'm with you now

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

Type inference

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.

ambiguous

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

misreadable

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.)

re human-oriented vs computer-oriented

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.