Lambda the Ultimate

I would like Java typing system at the speed of C. Of course, some runtime error reporting compromise should take a stand, but I'm willing to bear it.

Languages, and certainly compilers, are about a lot more than syntax and typing. To be honest, those are important, but also very superficial features. I sometimes can't spin my head around what a weird baroque construction C/C++ is, but it all works out neatly. Like forward declarations, or the module system design. All very old design decisions nobody would take these days but still important if you want to be able to compile 100MLoc projects fast.

But I don't really understand it. I wish one day one person would come around and list all decisions what makes C/C++ such a good language (Instead of bad. Enough bashing this ancient language everywhere.)

are fine, to the extent I'm perceiving. For that, I have to pay a tribute to good old C/C++. I like objects, code blocks, ability to cope with recursive functions. Now it all seems so natural and god given, but back in old days, function stack, objects, and replacement for gotos were all a hell of inventions. I can't describe a relief after leaving Commodore 64 BASIC rudimental constructions behind myself.

But now, after all of the history of a diversity of programming languages experiments, I'd like C/C++ to be wrapped inside a new, less redundant syntax envelope. I don't say it is a bad language. It's just that, seeing other experiments, it can be even better.

Yeah, but again semantics.. Who cares? One of the things of C/C++ is that compilers always have been uncompromising towards performance. Most C compilers parse while they lex and type check while they parse, and then the result is efficient code. Even the syntax is aimed at producing efficient assembly. There won't be a lot of people who'll be able to pull off anything anywhere as efficient from scratch. Certainly not with some academic principled approach which (only) starts off with superficial observations on syntax and semantics, I think.

(Though I gather templates were a design mistake from a performance perspective. Or it was just a trade-off. I don't know.)

I can also put it a bit more academic. C compilers have "Near linear behavior where even constants matter." Who designs that way these days?

Maybe it either looks good, either performs fast. I guess we can't have it all.

One of the things of C/C++ is that compilers always have been uncompromising towards performance

This is an artifact of pure-brute-force and a lot of resources. Pascal compilers are way more faster, but obviously lack the huge amount of time polished them to generate faster code.

But this is more about the compiler output, and I wonder what could be a modernized design of the language, what else could be added/removed with the knowledge of today.

For example, RUST provide lifetimes and some guarantees that keep the code GC-free and provide more safety. This is part of what I'm thinking.

---
The thing is that probably the only action in today imperative languages was adding OO and the slow addition of functional stuff, without much thinking in a well integrated experience (maybe, with the exception of LINQ).

But I don't really understand it. I wish one day one person would come around and list all decisions what makes C/C++ such a good language...

Judgments of goodness are relative, requiring some baseline context for comparison, such as competing alternatives at a particular point in time. In the 80's C was compared with very few mainstream alternatives, mainly Pascal; for example, see C vs Pascal access to Inside Macintosh calls in Apple docs. (I can tell you why I liked C more than Pascal then.) You would also have to compare with Objective C, and indirectly with Smalltalk since Obj-C is a roughly speaking a Smalltalk clone. I've been teaching my (college age) sons some C lately, making me think about it some.

C and C++ should be treated as two different languages, where C++ originally is judged against C as the baseline for comparison: what makes it better or worse than C, depending on your objectives. Stroustrup talked about it a lot. Perhaps a handful of issues mattered much to developers by the early 90's. (I first ran into C++ via paper in a periodical by Stroustrup, then later I found his one and only book, the first about C++ on bookshelves). Today "modern" C++ is different enough to consider it a separate language, compared to the version from 1990, especially given a quite altered standard library.

It was fairly easy to learn C by yourself, if you were up for pointers and manual memory management. It was not taught in classes, where I hung out; you were expected to teach yourself. It has few semantic constructs and not many keywords to learn. The model exposed was a graph in memory comprising code and data, and most semantic actions did something to that graph, referred to parts of it, or executed relative to it. Using C well required learning what storage classes meant, and where values were located. (Newbies would always concatenate strings in a local buffer, then return it as a value, not realizing return means scope exit and thus termination of local lifetime.) I liked that C was expression oriented, with values you could compose rationally. Some constructs in Pascal declared magical effects whose semantics could not be approached as values, so they involved more narrative.

Strengths and weaknesses in C involved being able to make whatever graphs you wanted, even if this meant shooting off your foot, provided you didn't use the same symbols someone else was already using, which would cause a link error. Nothing stopped you from doing anything dangerous beyond common sense, discipline, and convention. Slight mismatches in meaning could be catastrophic, and those become more likely at scale when using more code from different people. But if you didn't like being told what to do, freedom in C was nice.

Part of the original appeal of C++ was namespaces, in the "a class is a namespace" sense, carving the symbol world into parts with less conflict. By partitioning responsibilities among different types, there was also default incentive to avoid ball-of-mud architecture design, unless you didn't care. More structure meant less chaos. Eventually more structure also means less freedom, which happens after you pile on lots of new stuff with required conventions. But at first there was a slight increase of freedom under C++, since you did not need to avoid using the same names in different scopes, so interference was reduced. Any refreshing smell was due to that. Closing down access via member privacy was also nice, as a means of enforcing intention some things be hidden, so code clients could not depend on them. In other words, specific features prevented headaches.

The C model of memory graph you an arrange any way you like was still mostly present in C++, so everything was very concrete and easy to understand. At Apple for example, all early 90's debugging was done in 68K assembler, without any symbolic C++ source debugging, but you could see where you were anyway, since it was obvious how C++ and assembler related. Both were operations on the graph of code and data you had in mind. In that way, what was nice about C was still present in C++ at that time.

Designed to be that.

The implied premise that "natural" thinking is "good" should be scrutinized. Natural thinking is full of cognitive biases and fallacies and misconceptions. Natural thinking is almost never valid thinking.

Further, "imperative is a natural way of thinking" should be scrutinized. We might construct some relatively imperative plans (like, given a grocery list, we might form a plan that directs us to each item). But the bulk of the "thinking" was how we formed that plan in the first place, and how we later adjust plans based on observations or changing goals, neither of which is easy to think about or express imperatively.

I don't think one should infer a natural-thinking-is-good premise. I do think that when someone who thinks carefully finds a certain mode of thought natural, one ought to give consideration to its possible merits. The idea that "natural thinking is almost never valid thinking" is one that obviously depends heavily on one's choice of how to construe the adjective "natural" in context. I remember in my first year of graduate school, in an AI class, we were asked to participate in a study to do with people's understanding of probability. The person running the study started out by telling us a story that was supposed to illustrate how ordinary people misunderstand probabilities, and it struck me at the time that the moral they were trying to draw from the story was itself based on an ungrounded assumption about what reasoning was being used by the ordinary person in the story. I did fill out the questionnaire for the study, partly I suppose because it was evidently meant to help some other students with the study they were doing (I suppose our professor allowed that study to take up time from our class for much the same reason), but after we'd turned in the questionnaire we were given some further information about how the results were to be interpreted that was obviously based on a patently false assumption about what my thinking had been, and I felt utterly betrayed and dirty. I don't recall having participated in a single survey in the twenty eight years since then. A blanket statement like "natural thinking is almost never valid thinking" reminds me strongly of the faulty thinking in that study, and seems likely to stem from similar self-justification (choosing an interpretation of data to fit one's conclusion).

Note that the claim "imperative is a natural way of thinking" uses an indefinite article; I do not see why such a claim should be interpreted to having any bearing on any exclusively imperative mode of thought (whatever that would even mean).

Rather than "natural" I would propose designers aim instead for an "ergonomic" language. There is nothing natural about driving a car, for example, but the act becomes comfortable and second nature with proficiency. A car is a technology that covers a variety of human weaknesses, such as our inability to move swiftly and for long durations, to move bulky or heavy things, or to feel comfortable in hot or cold weather. I want something similar for programming languages - a technology that is unnatural but comfortable, and that covers my many human weaknesses.

the claim "imperative is a natural way of thinking" uses an indefinite article

Meh. If that's how you interpret it, you could just as easily argue "functional is a natural way of thinking" because we occasionally have thoughts of general form "I can combine X and Y via F to get a Z". But in context, I think it clear enough that someone who says "imperative is a natural way of thinking" is suggesting it is significantly more so than other ways of thinking such as "functional".

"natural thinking is almost never valid thinking" is one that obviously depends heavily on one's choice of how to construe the adjective "natural" in context

If you have a definition for "natural" that most people would accept and for which the statement does not hold, I'd like to see it. AFAICT, I could truncate the phrase to "thinking is almost never valid thinking" and it would still hold. I need only to look at human history or politics or psychology to see how ridiculous human thinking tends to be.

The relatively few forms of 'valid' thinking we know (such as formal logic, symbolic math, scientific method, Bayesian probability and statistics) tend to be very difficult for humans to perform consistently. Even a typical professional scientist who knows about confirmation bias and who knows the scientific method insists we aim to disprove our hypotheses will think frequently in terms of proving the hypothesis.

when someone who thinks carefully finds a certain mode of thought natural, one ought to give consideration to its possible merits

The word "natural" is vague. If someone thinks carefully and comes to such a vague conclusion, both the quality and care of said thinking should be questioned. Consider instead someone who thinks carefully and writes out a rubric of how a language performs with respect to various cognitive qualities such as:

• comprehensibility - a human fluent in the notation can keep a large model in his head, interpret it correctly.
• continuity - small changes in goals or scale leads to small changes in expression. This helps avoid rewrite-from-scratch and results in a smoother learning curve.
• compositionality - we can combine ideas with a predictable effect, and conversely we can easily extract, reuse, and share useful components of a larger idea. This is essential to support a community.
• clarity - when we express an idea, we can avoid accidentally mixing in other extraneous or irrelevant ideas
• concision - ideas can be efficiently represented, taking little time or space
• familiarity - because path dependence is a thing, affects economics and adoption

It's still a qualitative judgement, but less vague and more useful. We might try to examine what seems "natural" or "ergonomic" in terms of qualities that align nicely with the human individual or community (comprehension, familiarity, compositionality). And we can seek to combine those nice properties with other qualities that cover various weaknesses. One could certainly add more qualities to the rubric.

you could just as easily argue "functional is a natural way of thinking"

Yes. Yes you could. One could imagine such a remark, juxtaposed with the other, leading to an interesting continuation of the discussion; perhaps.

in context, I think it clear enough that someone who says "imperative is a natural way of thinking" is suggesting it is significantly more so than other ways of thinking such as "functional".

That's not clear to me. You may — and I really do have sympathy with this — be a bit hypersensitive to anything that smacks of criticizing the functional model. I think it's very easy to get into that frame of mind when defending something over time; long-running discussions may tend to polarize even when everyone involved is trying to avoid it.

I don't think what I'm talking about is ergonomics in the general sense; that term is likely to put emphasis on aspects of casual useability that are much less deep than what I'm after. There is a large class of concepts that are difficult to put into words; generally, a person talks around them and some people, who think similarly and share the concept, recognize what the person is referring to even though they didn't put it very well, while other people don't recognize what they're getting at and things start sliding to multiple, mutually unintelligible schools of thought. What I'm after is a sort of deep naturalness arising in the dynamics of ideas in the Platonic realm; I see its tracks in the history of category theory. I think category theory raised the exciting prospect — for people who recognized this sort fo naturalness — of perhaps acquiring a formal tool for studying it. When I first encountered the term "natural transformation" I was dubious, feeling that it was a rather restricted case to give such a grandiose name to; but lately I see it as a symptom of the thinking that gave rise to it (rather like the use of the term "spin" in quantum physics).

Re the six "various cognitive qualities" you mention. My thought, fwiw. Those aren't bad things... and yet, I feel they're missing something of the whole phenomenon. Sometimes analysis makes the big picture harder to capture.

What do you mean that the military uses an imperative command structure? I think elaborate type systems are hard to use because they're forcing you to prove things and that's hard. Formal reasoning about imperative programs is even harder.

There are some opportunities for doubt about the proof aspect of this. To start with, it's not altogether obvious that one should be forced to prove things when what one wants to do is specify what is to be done. It is of course important that programs be right, which would seem to be where proof comes into it, but with a programming language there are two kinds of proof involved: proofs about the language as a whole, which are done by the language designer before the programmer comes into the picture, and proofs by the programmer at programming time. Presumably the way the language is designed will have a profound impact on the distribution of proof tasks between designer and programmer. Some kinds of languages might put the hard proofs on the designer and leave the programmer relatively unencumbered; at programming time the act of proving things correct might blend seamlessly with conceptualizing the program. Other kinds of languages might cause the programmer's conceptualization and proof tasks to separate out from each other like immiscible fluids, with the proof task becoming a major burden that drags down the conceptualization. My own work for decades has centrally involved the premise that "programming is language design", so that indeed the programmer is partly responsible for preparing things for later programming; but the entire language framework is still set up ahead of time, and the programmer's proof-for-later-use might also be subject to smooth integration of proof with conceptualization.

The difficulty of formal reasoning about imperative programs is not an illusion. It's worth noting, though, that the difficulty may be due either to not yet knowing how we ought to be organizing imperative programs, or not yet knowing how we ought to be reasoning about them; it's a common observation, in discussions of this point, that mathematics has concentrated through most of its history on reasoning about declarative constructs, so our clumsiness in reasoning about imperative constructs may just be because we haven't yet put enough thought into figuring it out.

None of this translates into an immediately-available solution, though. Even if we suspect we just don't know something yet, that doesn't in itself change the fact that we don't yet know it.

That we shouldn't be forced to prove things is exactly my problem with strongly typed languages.

Some kinds of languages might put the hard proofs on the designer

I think you must be in some kind of DSL if the designer of the language can solve all of the hard problems in advance.

My intuition is that we'll never make imperative reasoning easier than functional reasoning because imperative programs tend to bring extraneous ordering and environment dependence into the problem and I can't see that being simplifying in general. But who knows?

It seems imperative programs can be represented functionally with an operator like "snd x y = y" providing we force strict left to right evaluation of arguments (this is done in 'Frank'). Is this functional, or is this imperative? Does it matter when the semantics are the same? What about a monad written with 'do' notation? Functional or imperative? What if we type an a 'C' program in the IO monad (so language syntax remains the same, but we change the type system). Is it functional or imperative now? It seems the semantics of ordering side effects can be expressed functionally so the difference is only syntax, and people can use whatever syntax they feel is more readable?

Facile language is a subtle thing; I think we still don't have a handle on it. The most rudimentary measure of the "power" of a programming language is what can be computed with it, and there is an interesting result there (the Church-Turing thesis), but blatantly, if that really made languages equivalent to each other, we could all just specify programs as Turing machines and be done with it. Just because two languages are equal in computational power doesn't mean they're interchangeable. There are more discerning formal comparisons between languages; there's Felleisen's expressiveness, and I took another step beyond that to a formal measure of abstractiveness, but that doesn't capture the full notion of "power" either. As I said, I think we still don't have a handle on it, as a whole.

Long ago, early in graduate school, I took a math class on the study of structural rigidity via matroids. (Fascinating experience; there were, as I recall, five math majors taking it, and they were all waiting to see whether the CS major who'd surprisingly signed up would really show, because the class would only run if six people took it; but I digress.) Matroids are one of those abstract structures, like groups/rings/etc., defined in terms of some things and some operations on them and some properties that have to hold, and there are like nine or so different definitions of matroid, all equivalent to each other, and there are pairwise directed proofs between these definitions showing that anything satisfying definition X also satisfies definition Y. One of these definitions, however, really appeared to be the most basic, and in a conversation one day the professor suggested to me that one might do a complete set of pairwise proofs from each definition to each of the others in order to demonstrate that that one definition was the most natural one in terms of which to understand all the others.

Nevertheless, some things were vastly easier to prove using some one of the other definitions of matroid.

Sure, it may be possible to describe imperativity in a functional framework using monads, but in practice that might just conceptually limit imperative programming by requiring it to fit into the straightjacket imposed by the typing infrastructure of functional programming. Unlike matroids, where we had a slew of different definitions and we understood all of them and could move between them more-or-less at will, in programming we don't yet nearly have a handle even on what the options are let alone what the native form of each is nor how to move readily between them. So I figure we're nowhere near knowing enough to judge between them.

A simple imperative language with garbage collection can certainly be expressed in the IO monad, with no additional restrictions over normal strong typing.

expressed in the IO monad, with no additional restrictions over normal strong typing.

Exactly my point. The very straightjacket I was referring to.

I don't mean to trivialize the alternative to my own view on this. Some people perceive "express[ing] in the IO monad, with [...] normal strong typing" as a simple and elegant framework. The point on which I wish to be clear, however, is that I do not see this approach as simple and elegant; rather I see it as cumbersome, essentially red tape dragging down the language. It appears to me such an elaborate type system is already suffering an impedance mismatch with the functional language paradigm — the typing is a second language, so that instead of writing a program in one language the programmer is obliged to write in two languages at once while keeping them synched with each other — and further shifting one of those to an imperative language only further increases the mismatch between the primary language of programming and the secondary language of typing. I do appreciate that some people find that approach acceptable, and I wish them well without irony; but I do not share their view of the matter.

I somewhat agree with your point about type systems, but don't think Monadic encoding of IO is part of that problem. Nor do I think modeling change functionally increases the mismatch. It seems to me that modeling change has to be the first step in reasoning about it. It's hard to reason about change using variables that themselves are changing.

If you accept the same programs as normal 'C' which is already typed, why is it a straight jacket? Especially if all the types can be inferred from the existing 'C' code. What I am saying is you can take a pre-existing 'C' program, and type check it in the IO monad, if it passes type checking you can compile it with a pre-existing C compiler (GCC for example). The whole point is the syntax is normal 'C', there is no second language the programmer needs to learn, the type system us used in the compiler for analysis, or this is a thought experiment to show the equivalence of two systems.

it may be possible to describe imperativity in a functional framework using monads, but in practice that might just conceptually limit imperative programming by requiring it to fit into the straightjacket imposed by the typing infrastructure of functional programming

In my experience, imperative programming isn't any more limited by monadic representation than it is by representation in C or Pascal or Basic or other conventional imperative languages. If anything, monads are the more flexible.

All of those representations do a horrible job with concurrency and composition. We can seek improvements, a model of "imperativity" that more cleanly accounts for multiple agents, physical communication, and open systems rather than leaving it to ad-hoc threads and side-effects. I am exploring a model of process networks using open channels to integrate external effects. There are various other models that receive relatively little attention, like the Kell calculus.

But I don't see any "straighjacket imposed by the typing infrastructure of functional programming" that would not also apply to statically typed imperative programming. I grant type systems may be a limiting factor in a more general sense, but I don't understand why you single out functional programming.

Some people perceive "express[ing] in the IO monad, with [...] normal strong typing" as a simple and elegant framework

Monads are simple, trivial, but they aren't elegant. Monads are a big hammer to which most problems are nails. Monads work just fine for representing inelegant models of imperative programming.

One of the reasons type systems are a constraint is that all programming is dynamic and typed at run time to some extent. Variant types for example use dynamic dispatch in pattern matches.

The problem with static typing is that you have to *split* your design into a statically typed part and a dynamically typed part, and that's extra work and it makes your code fragile.

The tradeoffs are well known to anyone who has written a compiler: a huge amount of what a compiler does is dynamic checking. If you over-abstract your design and use some static typing it is much harder to modify. But if you don't, you lose the ability to reason about the compiler almost entirely.

I have some experience with "fine-tuning" options here. For example I used Ocaml polymorphic variants which in theory are much better than ordinary variants in a compiler doing term reductions. In the end, to make that viable open recursion is needed doubling the amount of code per term type (exponential in number of term types), losing the assurance of type inference, horrible error messages .. and in the end I gave up and switched back to fixed variants with wildcard matches throwing "this is not supposed to happen" exceptions.

I agree with the issues you mention for static types, especially regarding the "statically typed part and a dynamically typed part" program division. Such issues apply to both imperative and functional styles.

Actually I would more or less claim that every "fault" of imperative programming has a dual "fault" in functional programming. I did say "more or less" so this is only a vague thing.

A good example is imperative mutation spaghetti. Since any procedure which can see a variable can modify it or use it, procedures which do so are fragile because a change to an apparently unrelated procedure can cause an impact. At least part of the problem is the lack of type information which might describe the mutation, in the absence of which you are forced to examine the actual implementation of procedures, so that they cannot actually be abstract.

But functional programming has the dual problem: any function can depend on any visible variable. Its spaghetti too! And in case you're about to say that this is not so bad because variables are immutable .. you'd be WRONG. Because of recursion, there can be many copies of a variable, one for each closure of the function, and you have the spaghetti problem that you don't know which one another closure binds to .. because it depends on when the closure was created. Which is exactly as if the variable was mutable if you say it "we don't know the value of the variable because we don't know what time you are asking about".

In this case the duality is not complete because procedures should be given control types where functions have return types, so in ordinary imperative languages procedures really are worse than functions.

In my opinion the real problem here is that FPL advocates have to agree the purely functional is a good analysis tool but a real programming language *should* be able to mix functional/declarative and imperative code in a clean, symmetric, manner so you can choose which idiom to use for any subpart of a problem solution. But we can't, we don't know how to do this. Monads show one integration method, but it really is not a good one. A good one would allow half your code to be functional and half imperative. It is well known for example that you can write imperative code inside a function without destroying transparency provided none of the effects escape. It is well known you can splice lists together if the head is never used again. It isn't just faster, its easier to write. In FP type systems this is linear typing, but C++ has a form of it too with rvalue binders!

My claim is that properly constructed functional/imperative symmetric language would retain the desirable properties of pure FPLs .. and enjoy some of the advantages of imperative code too. And the key to that I believe is understanding the concept of action, which requires a model of the software environment which provides a space/time continuum. Functional programming, being declarative, is a spatial system and that simply cannot work in pure form because there's no action. Implicit action from dependencies simply isn't reliable: it doesn't actually tell you much unless you specify implementation details like whether your FPL is eager or lazy. Being able to specify control flow explicitly *part of the time* when required is highly desirable. Having to do so all the time is clearly not. Even imperative languages have functional subsystems!

The most important thing about a purely functional language is that researchers push the boundaries of what you can express easily with one, and then, to construct a real language we just need the sum of the FPL and its dual. I have no idea how to do that of course. Maybe duality is the wrong symmetry.

I disagree with your characterization of functional vs. imperative here. Some general counter points:

• Imperative code also depends on variables in scope, so clearly this isn't a duality.
• Stateful aliasing, not in-place mutation, is the real issue for referential transparency. There are functional languages like Clean, Mercury, DDC Haskell where in-place mutation is possible when we know we have a unique reference due to uniqueness tracking in the type system.
• While instancing variables using the same human-meaningful symbol for recursive closure construction might be confusing, it is not equivalent to mutating a variable that is aliased between closures. It's closer to instancing many points, each having an `x` and `y` field. To know the value of `x`, you must know which point you're asking about, but you don't need to know when you're asking.
• Variables are optional in both styles, cf. Forth and Joy. We should avoid characterizing imperative or functional in terms of variable use, and instead seek more fundamental distinctions.

Regarding monads, a lot of FP programs are "half" imperative or more if you count number of lines in the IO monad or wrappers like the Warp web server. And there are monads such as State and ST that permit locally imperative expression of program behavior without risk of effects escaping.

I'm not fond of ST or IO. I've observed that any model using `new X` (no matter the type of X) proves semantically problematic in context of serialization, persistence, parallelism, concurrency, distribution, incremental computing, efficient garbage collection, entanglement with the interpreter environment, and replication (as might be used for checkpointing, mirroring, branching, backtracking). But I do make use of State when it is convenient, IO as needed, and my interest in Kahn process networks and variants is closely related, providing a clean basis for interaction, state, concurrency, etc. without `new`.

In any case, I don't see FP as being weak at imperative expression. I've seen Haskell called the best imperative language. While tongue in cheek, and perhaps a bit dated (given development of Nim, Rust, etc.), there is some merit to it - I can certainly express myself imperatively using monads, and Haskell offers convenient freedom to introduce new imperative layers or abstractions compared to conventional imperative languages.

Ok, I take your points. I think I have a mental model of timeless space here, in which objects exist, always existed, and keep existing. This spatial picture corresponds in my mind to set theoretic mathematics. One uses logic says things like "for all X, there exists a Y such that the union of X and U minus Z is Y" or some such, and i view these are assertions about space: definitions are purely declarative, there is no action. There is no construction either. You do not construct Y, it simply exists, a constructor for Y is not a constructor, but a locator.

I equated this spatial world with functional programming. I would say it is indeed the basis of functional programming. But real FPLs of course have more.

So I want to add time as a dimension to programming. Underneath, energy fires off events in transistors in space and time: the core concept is action.

So again, imperative is not really the same as temporal, any more than functional is the same as spatial.

However my point remains we need symmetry. FPL's have types which are exclusively spatial and that's a disaster. Even if you can model temporal concepts like mutation with monads, the types do not properly reflect the temporal properties.

Frankly, the monadic model doesn't even work. You're relying on dependency chains to define time. EG if you have f: S * A -> S * B, then the notion comes from the idea you need the data in the domain first, to compute the codomain value. But this is not in the foundations. And if you are evil and actually hook I/O up to the state changes you may be in for a nasty surprise when the purely functional compiler optimises away some operations, or changes the order, because it assumed no side effects.

Time has to be a core concept, and we have to have temporal types to provide enough abstraction to reason about time.

Bad example: you have to open a file *before* you can read data from it, and you can't open it again until it is closed. And you CANNOT model this in an FPL with spatial types. Even if you provide a function that maps a "not yet open file" to an "open file" and only allow reads on an open file, you have left the "not yet open file" value lying around. Here persistence is an enemy. Linear typing would help here but I'm not sure it's enough to model all protocols.

Coroutines can enforce this easily at run time. Any fibre that tries to open an "already open file" will starve. You may want to ensure this can't happen statically with type information, I don't know how to do that but would like to. Note, there's no error code for breaking protocol, so there's no need to analyse it.

Your system with networks will be the same. You can do it too.

Set theory works just fine for modelling time. You model things as functions of time (cf all of physics). Similarly, FPL work just fine for modeling opening and reading files. As programmers, we're writing code now that will handle cases that arise in the future. Being able to reference now actions that exist at various times in the future and reason that we can't combine them in a certain order because the types will be wrong makes perfect sense to me. Why are you assuming that all values are spatial?

the monadic model doesn't even work. You're relying on dependency chains to define time. EG if you have f: S * A -> S * B, then the notion comes from the idea you need the data in the domain first, to compute the codomain value. But this is not in the foundations. And if you are evil and actually hook I/O up to the state changes you may be in for a nasty surprise

Your argument here can be rephrased as "monads don't work because I cannot add effects to the State monad" (a monad best characterized by `runState : State s a -> s -> (a,s)`). It is true that you cannot add effects to the State monad which is defined to use a specific, purely functional embedding. But this limitation cannot be generalized to "the monadic model".

We can start instead with a more general model of MonadState, perhaps a 'free' state monad where `Get` and `Put` requests are represented as values. We can hook up IO effects to state in either of these cases, e.g. modeling an inbox and outbox for messaging, managing publish-subscribe state, updating keyboard states, rendering buffer states, and so on.

In the general case for monadic state a contextual computation has opportunity to observe or interfere with the state before continuing. Such interaction is essential to having an effect in general, not just time. The State monad elides such interactions and thus does not have an effect.

if you provide a function that maps a "not yet open file" to an "open file" and only allow reads on an open file, you have left the "not yet open file" value lying around

As you mention, linear types could work. But more relevant to the current discussion, you could simply track 'open files' in the environment embedding a monad, and allow a request to open a file to fail or block (whichever is most appropriate for your model).

When you run a program and look for errors, it becomes increasingly difficult to test all the branches and functionality.

What if instead the aim is to look at a program itself as data, and make the strongest guarantees about the programs runtime behaviour as we can without running it.

Types are useful precisely because they are static. Dynamic languages like python and JavaScript do have types, but they are no use in checking correctness or improving program reliability. In fact they tend to make programs less reliable, as passing a string to a function expecting a number can have unpredictable consequences, and nothing stops you doing it.

So my summary is that it is precisely the split between static (can be proved without running the code) and dynamic (need to run and debug the program) that makes types useful. With better type systems we may be able to statically prove code like sort functions always correctly sort their input, without having to run the code.

A valid criticism of this is that you may be writing the same program twice, once declaratively at a proof level, and once at the operational level, but of course the types do not guarantee total correctness, they only guarantee certain properties. The key question then becomes, are the properties of a program that are provable using types useful in understanding program correctness?

The properties of imperative programming you describe may well be the case for existing languages. However functional programming is very hard to reason about too and has the dual problems. Reliably, it is just as bad because of the duality principle.

For example a procedure in say C++ can modify any variable in scope, which is really horrible, right?

Dually, a nested function can depend on any variable in scope. Its the dual problem. And don't say the variables are immutable because that is quite wrong: functions can recurse so the problem is a nightmare because you don't know which instance of the variable you're referring to, which is equivalent to asking at what time you refer to a mutable store.

The only reason functional is better is because it is more deeply studied. After all FPL's are all based on set theory which has been around rather a while. And it is known to be a disastrous and without proper foundation. [Sorry but Curry/Howard is just a proof that neither logic nor set theory can exist without the other, yet both are founded ON each other: the correspondence is not a theorem, its true by construction]

If you actually looked at how coroutines worked you'd change your tune. Since they're dual to functions in some sense, they have the the same properties (dualised), including for example purity, abstraction, etc. Furthermore FP is unable to handle half the things you think it can handle, such as partial functions, streams, sum types, and more generally coinduction. You can model all these things but the models introduce an extra level of complexity that soon gets out of hand.

The same thing happens in C with imperative code. Move to C++ and its better: now you have more powerful functional stuff. Move to say Ocaml and you get even more functional power on top of your imperative base.

The moral is, you can't write code without both imperative and functional components. All high level imperative languages have expressions which is a weak form of functional programming. And of course Haskell tries to get imperative with monads (which is a very weak and bad way to do it).

The ONLY kind of language that makes sense is one with both products and sums, one with both functional and imperative code. Everyone knows that. The problem is just how to integrate them. We live in a Newton world, with space (functional) and time (imperative) but we need Einstein: a space/time continuum.

This all seems like it ought to hook up, somehow or other, with my wranglings with the notion of co-hygiene, though the conceptual frameworks seem rather different (I struck on the idea in exploring connections between term-rewriting and basic physics; blog post). A nuance I've been considering is whether there are generic classes of side-effects, that might allow useful analogy between different kinds of computational side-effects and different kinds of non-gravitational forces in nature. I suspect the two basic classes of side-effects are visible in Felleisen's calculi (and therefore in my vau-calculi since they share objectives from Felleisen's work); essentially the two classes correspond to the highly universal complementary pairing between time/space, verb/noun, energy/matter, control/data, etc.

If you look at research on "naive programming", the most natural way is an event-based style, with tiny imperative and algebraic bits glued onto the side (i.e., a collection of rules of the form "when X happens, the player loses a life" and "the score is the number of circles Pacman has eaten"). (Eg, see A Programming System for Children that is Designed for Usability.)

However, event-based programming is incredibly fallible, because these programs are chock full of race conditions. This isn't normally a problem when giving instructions to humans, because (as you say) with sufficient experience a human can usually figure out an appropriate ordering of events.

The "with experience" qualifier is extremely important: eg, a recipe written for a professional chef will be much terser and seemingly-ambiguous than one written for an amateur, because the professional can look at the list of needed activities, and then work out the dependencies and schedule their activities on their own. (In fact, the pro will usually be frustrated by the level of detail in a recipe written for an amateur, because the explicit schedule given won't be optimized for their particular kitchen.)

Without experience you're just hosed, because it's very unnatural to think about every possible schedule/interleaving and verify that it always gives you a correct answer. Even people who know how to do it don't enjoy it: pretty much every expert on concurrency theory works really hard to use it as little as possible in their own programs.

Pure imperative programming removes races from algorithms by making the program strictly sequential. Pure functional programming eliminates races from algorithms by making races harmless. Both of these are unnatural, because they are extremist positions relative to the naive way we think. But going to extremes is also effective -- optima are often corner solutions!

Mixed programming models (as you find in Haskell, ML, Scheme, Java, Python, C and every other practical programming language) reintroduces logical data races, and makes program reasoning hard again. Basically, a call to an unknown function that modifies data behaves effectively like a scheduler preemption. Unfortunately, many of our best-performing algorithms rely critically on aliasing to function -- somebody had to consider every possible trace, and concluded that the logical races in this case were harmless.

TL;DR: programming is hard.

This is a nice explanation, and I think it would make an excellent blog post.

well reasoning is hard so of course encoding reasons is even harder, you not only have to think, you have to model your thinking as well

[nevermind]

The military example is interesting. Although an army is a massively distributed system, everybody within it is organised in a strict hierarchy. The imperative orders are executed in a system where instructions flow downwards, information flows upwards and the division of responsibility (ownership) is aligned with the control-flow. This is a particularly clean kind of distributed system. It is a well-nested collection of embarrassingly parallel sub-problems. In programming terms it is probably closed to writing branch-and-bound programs? i.e do X until Y happens is split into tell C1 to do X1 until they see Y1, C2 to do X2 ... and report when you see some f(Y1, ...Yn).

Militaries are famous for hierarchy, aren't they. Not quite so simple, though; there may be multiple branches of service, each with its own internal hierarchy, and even if they are in theory all under a single commander-in-chief, much of the time they'll interact only at lower levels so you have again multiple independent hierarchies. Not to mention that not all such hierarchies will have a common commander or even necessarily a common cause; there's a whole spectrum, out to the extremal case of enemy forces. There are, I think, remarks floating around that it takes a high degree of cooperation for two forces to meet in battle; complementary, perhaps, to remarks about the chaotic nature of the resulting battle (eg, no plan survives first contact with the enemy).

I wouldn't dispute that the military has a nice clean model that works on paper. I wouldn't dispute that in the real-world it is a lot messier. But, does the real-world version work well as a distributed system or not? When units without a clear chain of command have to cooperate - the result does not look like a good model for how to organise a distributed system. In programming it is rare to find an organisation / coordination problem that can be mitigated with an increase in firepower. Brute force does not scale well in exercises in distributed programming.

seems nice in theory but the *real* military rarely works that way.. there are competing interests, contractors, multiple funding sources, multiple communication networks and we can sum it up by the term SNAFU. Situation Normal, All Fucked Up.

Functional programming may have some advantages over imperative but it is incomplete and lacks symmetry.

Functional is a misnomer, the correct word is spatial. In the spatial world, constructors are a misnomer too, you do not construct values, you locate them. This gives rise to a proper interpretation of the idea of persistence and immutability: inductive datatypes, which inhabit the spatial world are finite and terminated. The abstract world is modelled on sets and elements (types and values). It is intrinsically declarative. It has products, which implies unordered access to components have invariant results.

Functions are harder, but live in the mathematical world of sets.

But the spatial world is not enough. It cannot handle partial functions. Division, for example, has no representative here. You can model it, restrict the domain or extend the codomain to get a function, but that's a model, it has the wrong type. Similarly functional programming quite obviously cannot process streams. How could it, if the stream does not end? More generally you can't handle sum types or indeed any coinductive type in a functional system.

The imperative, or temporal, world has no problem with coinduction, but it can't handle products! This is a well known problem: variables change so invariance of projections is lost.

But traditional imperative programming system has a major drawback. Whereas a function has a domain and codomain, allowing its semantics to be encapsulated in an approximation with a type system, which simplifies reasoning, procedures just return control, and no value.

The solution to this problem is to add the missing codomain type, but you must understand this is a *control* or *temporal* type not a spatial one. A control types is the set of all possible events in which a procedure can engage. The idea is not mine, it is present at least in Hoare's model of CSP.

Object orientation also attempts to make reasoning easier by partitioning the state space and restricting access to classes of the partition to a small set of methods, making reasoning easier. By itself this idea is known to fail due to the covariance problem.

But it only fails because people are trying to use a subroutine based model for the world, and spatial types where temporal ones should be used. The dual construction of an spatial object is a multichannel coroutine.

Coroutines do not return control. In theory, the not only never end, they also never started. Just like persistent spatial data types, they are forever, and they were always, and they're active imperative entities that do I/O on communication channels. The sequence of possible I/O operations is the coroutine's control type.

Coroutines can handle streams, partial functions, and sums correctly which functions simply cannot. So any programming language MUST have both kinds of spaces: spatial and temporal. Without both there is no action, and computing is all about action.

Here is division: read x, read y, if y!=0 write x/y. The control type is RRW?, meaning two reads and maybe a write.

Streams are easy: read x, write (f x), repeat. You simply cannot do that in an FPL. You may wonder why. The answer is that a stream is NOT an infinite list, its an unbounded sequence. It can still be finite. Functions cannot handle the lack of a terminal because without a terminating condition that cannot return. But coroutines don't return anyhow. So if you send a finite sequence down a channel a looping transducer just stalls waiting for data that never comes. It's not a problem!

I have an advanced example of how to use coroutines: a parser which can parse from a context free grammar. It works by exploring all alternatives, a coroutine is spawned for each, and if it fails it just fails. Unlike the corresponding functional parser where you have to return a fail code because functions *must* return, coroutine can't return in the first place.

What I do NOT have is a good way to calculate or use control types. I can reason about them on a case by case bases but I don't know how to teach the compiler to help.

This vaguely reminds me of Wadler's Paper on call-by-name being dual to call-by-value. You've written about this point of view a few times, but I haven't been able to quite follow it. Have you written about it in more detail somewhere else? If not, I need a bit more intuition. For example, why isn't a disjunction spatial?

Yes, call by name and value, and perhaps eager and lazy evaluation, products and sums, functions and continuations .. we have many dual concepts but no coherent way to organise all together.

There is a modelling language, namely category theory, with the power to build these models in a precise way, but my understanding is too basic to really understand the relationships .. it feels a bit like the notion of an adjuction.

Products are characterised by projections. The are spatial entities because they always existed (no, constructors do not make them .. making things implies TIME .. products are not constructed, they are located). Products are persistent and immutable, projections always return the same value no matter what order you apply them. This time invariance is what makes them spatial.

Now look at a simple variant such as Left of int or Right of float. We know the encoding is a tag, say 0 for Left and 1 for Right, followed by store for an int or float, depending on the tag.

But which one is there? The int or the float? We know how pattern matches works, we check the tag AT RUN TIME and jump to code that assumes the value is an int if the tag is 0, or a float if the tag is 1. So the actual type is dependent on the tag and requires a test which requires control flow. That is, it requires temporal sequencing. You test first, the branch to the appropriate handler.

However that's only a typical FPL model of a variant. Consider a compiler generating code that runs a C function, which has two blocks in sequence, the first with a local variable of type int, the second with a float. The data type to represent this is a *C* union! There's no tag. The reason is that control flow is the discriminant: in the first block, the local variable on the stack is an int, in the second a float. Which variable is active is time dependent, the program counter acts as the discriminant.

Oh, wait! That's EXACTLY what happens in the FPL model in a pattern match, we just convert the stored tag into an address which is put into the program counter (i.e. we DO a branch). The handler is intrinsically lazily evaluated, if we do not run it AFTER checking the discriminant the type system would be unsound.

But that means the type system depends on the imperative concept of control flow. in other words sum types are intrinsically control, or temporal types.

The piece data (tag, value) is NOT a value of a sum type: that's a spatial type, and sums are temporal. It's a model, and its a model you cannot have in a purely spatial system (that is, a purely functional language), because the model just delegates to lower level control flow primitives.

If you want to see a REAL sum type here is a coroutine: c = read inp1, if c then write (out0,x) else write (out1,y). The coroutine "black box" writes to one of two channels and it can write values of distinct types too (which you cannot do in a FPL!). What hangs off the other end of these channels, reading the results, are alternate continuations. So the coroutine, by writing to one channel or the other selects the continuation which executes the rest of the program.

The control type is that we "write on out1 or on out2" and THAT is a sum type. Its a disjunction, which chooses between continuations.

Yes, my implementation uses a traditional if/then/else internally. C++ didn't come with coroutine primitives natively :)

By the way, I do NOT understand all this completely. I do not have a precise succinct theoretical model. Filinski has a go at a subset of it in his master thesis (Symmetric Lambda Calculus/Symmetric Categorical Language).

My intuition is that it might be more fruitful to understand this as factoring the usual set of values into spatial/temporal encodings. I'm also not sure that spatial/temporal is even a good way to describe it. I think this is the usual duality between positive/negative, producer/consumer, value/context. The consumer of a conjunction can consume two values. The consumer of a disjunction must supply two contexts. I think Wadler's paper that I linked above (among others) shows how to do this. There was a second paper in that series. You can think of a calculus like this as describing a compilation target. There's nothing wrong with thinking of a disjunction as a value, but when you compile to this particular compilation target, you encode it as "control flow".

Also, I'm skeptical about some of the things you've claimed to be dual, like mutability being dual to shadowing. That doesn't feel right to me. Some of these other dualities can be made precise.

Finally, I think the way that you do asynchronous message passing between co-routines as you've described on here previously is going to be huge semantic can of worms and will be a barrier to any clean duality result you might hope to find. Comments like this are a big red flag to me:

For example given two coroutines which are functional transducers of type (R1 W1)+ and (R2 W2)+ if we connect W1 to R2, the composite is NOT (R1 W2)+ because I specify that on a read/write match up, either the reader or write can go first. So you can get two reads in a row before anything pops out of the W2 channel.

This is very interesting to me, though, so if you do make progress on formalizing some of these ideas, I'd love to hear about!

One interesting way to encode sums that you haven't mentioned is a Church or Scott encoding, essentially: `(a + b) = ∀c.(a -> c) -> (b -> c) -> c`. This makes it rather explicit that you provide two continuations, and the sum selects one of the two. In the Scott encoding, we have `left = λa.λonA.λonB.(onA a)` and `right = λb.λonA.λonB.(onB b)` as our data 'constructors'.

In the past, I've experimented with modeling spatial types explicitly. That is, I would have `type@location` where `location` is a specialized class of types. Locations could be heterogeneous in which features they provide, e.g. which computation primitives and effects. Hence, the type of an "add" function might be `(HasAdder a loc) => a@loc -> a@loc -> a@loc`, which is to say "if we have an Adder for type `a` values at our location, then we can add two `a` values to produce a third `a` value at the same location." Functions existed to represent communication between locations, which was only reliable in cases for locations representing different threads in the same process. I could encode distributed values `(a@A * b@B)`, and distributed control `(a@A + b@B)`. As an interesting variant, I could encode time as part of the location with a monotonic transition, representing latency.

Making spatial distribution explicit in the type system was intended to support compilation of a program into distributed shards or fragments. I still think it's interesting, but I stopped experimentation with it mostly because I needed dependent types and runtime compilation to use them effectively. In almost use all cases, I want to configure distribution based on runtime data and available resources, e.g. to optimize latency or utilization.

Anyhow, whether it's Left vs. Right, or this continuation vs. that one, or a message on channel 0 vs. a message on channel 1, sums always have both a spatial and temporal aspect. Blocks of code are spatially represented in both source and memory. Channels can be represented spatially using separate buffers, or themselves use `(tag, value)` pairs where the tags are channel IDs. The `(tag,value)` encoding will have only one tag at a time, hence a temporal disjunction.

It is not unreasonable to characterize time itself as a function. Time takes a world from one configuration to another. A function takes information from one configuration to another.

Consider a simple cellular automaton. We have a simple step function that takes the system from one state to another, perhaps running Conway's game of life. This is among the most coherent explanations of "time" that I have encountered, albeit greatly simplified. There are reversible cellular automata. Commonly reversal requires information from a broader portion of the system compared to the forward step rule - an asymmetric effort. I find this interesting because most of what we understand in physics can be explained by simple local rules and similarly reversible phenomena. Reversible computing in general has an interesting relationship to physics.

Functional programming can work just fine with streams and coinductive data. Sure, you can't expect to wait for the entire stream before returning a result. But you can take a stream of numbers and compute another stream representing, say, a running sum or a local average.

Functions do get awkward with some things, like if you want to split a stream into eighty child streams based on the values without processing and filtering the stream eighty times. (Filtering streams is problematic even without doing so eighty times.) But we can write a function that evaluates in small steps a process network that observes the stream and pushes to eighty output ports.

It seems to me that the vision of "functional programming" you argue against above is something of a straw man. FP doesn't insist on silly things like infinite processing before returning a result. FP doesn't hesitate to develop and use patterns like monads or arrows or reactive networks that solve real programming problems.

Interestingly, I recognize in this a shift of thinking that's likely part of why some people embrace monadic style while others reject it. When introducing monads, it becomes necessary to step back entirely, and irretrievably, to a meta-level from which one views the program using the monad. There's a price to pay for that. Just as I've described strong typing as a second language that one has to cope with simultaneously with the first language of programming, the introduction of this meta-level further increases the number of different views the programmer has to juggle at once. This seems to be qualitatively different from the sort of "higher-order" programming involved with, say, mapping a function f onto a list, because the mapping has transformed f from a function on elements to a function on lists but any shift-of-level needed to think about it is localized, only needed for thinking about that particular operation; once you grok how the operation on the list is derived from f, you're still on the same level of programming you started at. I recently saw someone claiming that fexprs bring nothing new to Lisp because without them it was already possible to add new special forms by introducing a meta-circular evaluator; which seemed to me somewhat missing the point because fexprs allow you to do such things without introducing a separate level of evaluator.

I don't believe that juggling views or layers is the issue here. People work with those without much difficulty all the time - in the form of software design patterns, DSLs and scripting, frameworks, network services, etc.. Imperative starts with many more views and layers than pure functional because you've got to consider interactions with the OS and network. The important difference is that these views are 'concrete' at every step.

My own hypothesis is that the visceral rejection of 'monads' is more a convergence of factors.

First, monads are presented without a concrete, visualizable structure, something users can hold in their heads and interpret. This could be addressed easily enough, e.g. by using Oleg's freer monad so we can avoid an extra typeclass abstraction and work through many example uses of monads with a single concrete representation.

Second, languages like Haskell have an unfortunate tendency to force users to confront generalized abstraction before working their way up to it through multiple examples. This doesn't work so well for humans because we can't learn something until we almost already know it. Ideally, a PL design should consider learning curves, avoid learning cliffs. I sometimes feel that program documentation should readily support interactive tutorials and puzzles to help a programmer grasp a difficult concept. Program rewrite semantics are also interesting here, since they together with partial evaluation enable us to unravel and dissect abstractions we don't understand when working with foreign code.

Third, many people come into FP with misconceptions. They frame their understanding of FP in terms of what they are familiar with - imperative programming. I certainly was no exception to this. It leads to awkward attempts to distinguish "the model" from "the real thing" with regards to state, identity, effects, and concurrency. This is exacerbated further by an informal understanding of those concepts. Misconceptions are a lot harder to work past when you don't grasp the alternative because points one and two.

I feel we could do a lot better with presenting concepts like monads, keeping things more concrete and grounded in ways programmers are able to grasp.

I don't believe that juggling views or layers is the issue here.

Well... yeah. You don't see the problem. It's not a problem for you. But we knew that. Iirc I also remarked, somewhere around here, on what happens when one person is trying to describe a concept that another person doesn't share, and this seems an instance of that effect. Concepts have no substance; if you don't perceive it yourself, it's easy to suspect it doesn't exist. The problem is compounded when talking about a difficulty with something, because one is tempted to distinguish between difficulties caused by seeing something versus those caused by not seeing something — quite possibly an illusory distinction, and one that can provide <s>hours of fun for the whole family</s> no end of confusion.

Truthfully, the rest of your first paragraph only confirms for me that you're not getting the concept I'm describing; the analogous cases you name don't seem analogous to me, the imperative complications you mention seem superficial to me thus underlining the absence of the deep concept.

My own hypothesis is that the visceral rejection of 'monads' is more a convergence of factors.

Hm. This is consistent with the hypothesis that you're seeing this as less fundamental than I am.

First, monads are presented without a concrete, visualizable structure, something users can hold in their heads and interpret.

(Lol. Sorry, I'm not laughing at you, it's just... are you familiar with the classic criticism of category theory as "generalized abstract nonsense"?)

You mention the "freer monad" thing. I'm skeptical, as always, but that direction does sound more promising than others I've heard of.

languages like Haskell have an unfortunate tendency to force users to confront generalized abstraction before working their way up to it through multiple examples. This doesn't work so well for humans[...]

Mitigating limitations of the human mind is of interest, but when people have a problem with a way of thinking it isn't always just a problem with them. Sometimes there's a flaw in that way of thinking. (Remember Feynman's story about breaking into safes in people's offices at Los Alamos, in brief moments when left alone with them? He saw it as a security problem that the safes were so easily broken into, but the official response to the problem, when he pointed it out, was to issue orders that he was never to be left unattended in those offices.)

Ideally, a PL design should consider learning curves, avoid learning cliffs.

Sounds very plausible, but there's also something to be said for choosing a lower-altitude, and more accessible, destination.

Third, many people come into FP with misconceptions. [...]

Betting on misconceptions is fairly safe. Keep in mind, though, that experts in anything are at risk of underestimating the artificiality of their expertise. I've encountered folks who find W-grammars as natural as breathing, and can't understand why anyone finds them hard to work with.

You don't see the problem. It's not a problem for you.

You mistake my words. I do see the problem. I remember my struggles with monads, and I've walked a few others through theirs. Usually, just pushing to use a few different concrete monads in a few exercises (e.g state, reader, maybe, IO) without thinking about the abstraction is enough to get someone productive with monads. My experience learning and teaching monads is anecdotal, but contributes to the alternative hypothesis I presented above.

Rather, I disagree with your proposed diagnosis, that the problem is somehow related to meta-levels or juggling views. That simply does not fit any of my observations. When I mentioned some cases where a challenge really is "meta levels and multiple views", I intended to communicate that those aren't similar to the problem with monads, therefore your diagnosis is wrong.

something to be said for choosing a lower-altitude, and more accessible, destination.

I agree. I have mentioned process networks are a very promising destination. Concrete, visualizable, accessible. Better supporting logically concurrent input, output, and flexible composition. Yet retaining the essential interaction property that make monads an attractive concept for functional representation of imperative behavior.

Well, it's good that each of us can find something about the other's comments to agree with. When things come down to disagreements about whether people are understanding each other's positions, it all tends to disintegrate into unresolvability. If people outside a subject are bothered by conceptual problems with it that practitioners can learn not to be bothered by, there may be no way to agree on whether the practitioners have learned to understand it better or learned to turn a blind eye to the problem; students of history centuries later may debate it, and perhaps still get it wrong but by then it will at least seem less urgent.

Actually you're dealing with models of streams, etc, not real ones.

To explain, lets first consider partial functions, such as division:

div: int * int -> int

You cannot do division in a functional programming language!

What? That's right. You cannot do it. What do you do if the divisor is 0?
You can build a MODEL:

int * int - {0} -> int
int * int -> 1 + int

but these have the wrong type. These are functions.

You can use monads. Same deal. Its not real. Its a model.

Its the same deal with streams. Coroutines process both partial functions and streams natively without modelling. Filters are no problem: x = read inp; if P(x) write (out, x); repeat. Failing to return a value is natural for coroutines because, in fact, they never return in any cases!

They're not better: coroutines can't do products. Sure, they can build models of products as time series, but that's not a real product because products have invariant projections.

So when you say "FPL doesn't insist on silly things like processing the whole of a stream before returning a value" you're completely missing the point that you CANNOT write a function that processes a stream. Just as you CANNOT processes a partial function either. You can only work with functions and products.

In an FPL, you CANNOT do mutation. But yes, you can use monads to model it. But using monads isn't the same thing at all as actually modifying something: the monad imposes a framework around your imperative code. Of course .. that is precisely the idea, to encapsulate the imperative code and stop the mutations "escaping" to arbitrary variables.

In any practical language of course, it is never going to be purely functional. And that's really the point here. FPL's hide their imperative features, but they're quite clearly there: Ocaml specifies eager evaluation of function arguments AND IT MATTERS. And Haskell says lazy, AND IT MATTERS. Which means neither is purely functional.

It would be better if the purely functional and imperative constructions in a language were balanced and well integrated instead of being hidden inside a myth. See Filiinski for a technical discussion of the myths (lazy FPL's do not have sums, eager ones don't have products). The thing is FPLs do not actually process functions. Functions can't diverge, they always return values (for example). They can't have side effects, so writing to a port, inside an I/O monad or not, is clearly NOT functional programming. Its imperative programming that happens to use the type system of your language and it clearly doesn't work except for special implementation details. Write to a port? Impossible. How do you know the writes are done in the order you think you specified, unless you rely on hidden implementation details? How do you know the compiler didn't optimise these things away?

A nasty example of that: in Felix, functions are not allowed to have side effects, and any function returning unit can be elided and just replaced by a unit value. Unfortunately Felix also has generators which have persistent state and look like functions. The compiler lifts generators out of expressions and replaces them with a variable which the generator assigns to, so the remaining expression is purely functional with no side-effects. Felix also deletes the initialiser of any variable which is not used. But there's a problem: if the generator returns unit, the whole generators is elided, deleting the side effect. In particular coroutine "read" is modelled as a generator, and this means I cannot read a unit, units are really useful (for example to represent clock ticks).

My point is, if you optimise a Haskell program on the assumption there are no side effects and lift some lazy operations to eager on the basis of strictness analysis, you have a serious problem because there's no way to actually model an operation like writing to a port in your functional abstraction as something non-elidable. A write, for example, could just return unit and you could elide functions returning unit. You have to CHEAT to prevent this. So in fact no, you cannot write to ports in a real FPL. The operation is intrinsically imperative and you CANNOT build a model of it. You CAN model mutations to store because they're internal (not externally observable).

I understand where you're coming from with "the model" vs. "the real thing" because I once thought similarly. I came from an imperative paradigm and framed functional everything in imperative terms. These days I find the distinction awkward and of no utility within software. Real things include computation, performance, integration of cyber-physical systems. Within software, we have only models.

Streams model incremental computation as a generally unbounded sequence of values, and any computation that behaves thus can truly be considered as a stream, regardless of how it is encoded. Your coroutine read/write is no truer a 'stream' than is a lazy list or a more explicit codata type.

Re: division - I disagree with your argument in a few different ways. First, types aren't any more essential to FP than they are to imperative (e.g. the original lambda-calculus is not typed). Second, there is nothing inherently wrong or anti-FP with partial functions or use of constrained types (like non-zero integers) to prevent error. Third, division is "modeled" (and so is `int`) regardless of whether you're in imperative or functional or using coroutines or whatever.

Re: "coroutines can't do products" - Sure they can. You've mentioned elsewhere that coroutines essentially encode 'sums' in terms of selecting one coroutine or another to handle a message. The dual to that - the product - would be having two coroutines logically active at the same time, e.g. gathering data from two different sources, or writing fragments of a message to two different ports for separate processing.

Re: "writing to a port (..) is clearly NOT functional programming" - Yet returning a value of the form `(Write(port, value), continuation)` is well within the realm of functional programming. FP is about functional modeling of software systems, and that necessarily includes effectful interactions. It's a useful feature that we can think and express ourselves 'imperatively' within a state or network monad, yet can still treat and abstract and compose monadic expressions and effects as referentially transparent values from an external perspective.

Re: Felix semantics of dubious soundness - clearly your effectful generators shouldn't have the same type as effect-free functions. Instead of returning Unit, perhaps they should have type `IO Unit` or `Generator Unit`. :D

In any case, I don't have more time to spend on this discussion. If you take away only one thing, I hope you'll be a bit more critical of your own concepts, and a tad less dismissive of approaches that don't fit your personal paradigm.

Let me try to make the division point again. Division is a partial function. It has a natural representation with coroutines.

When you build a functional model, the type is wrong. You have built a model of a partial function using a function. There is more than one such model.

The fact the type is wrong perverts your code. If you chose to extend the codomain you have to check the result was not "division by zero error".

We KNOW this is perverse and wrong, and that it is a model IN the language. What makes it a model, distinct from the real thing, is that the representation is plain wrong as evidenced by the incorrect type.

You can use monads to partially hide this, that is, to avoid checking for numerical errors every step of a calculation.

So I am being very specific here explain exactly why you have a model: type is wrong, and you have to actually write code to handle the possible error case.

So I think there really IS a distinction between a language, and a system encoded in this language which could be represented linguistically as a meta-language. There's a distinct level break here.

This is exactly the same as compiler intrinsics such as integer addition, and user defined functions which necessarily depend on these intrinsics. Exactly what is intrinsic can vary. Everything else is a model.

So functions are intrinsic to FPLs, even though what you use them to model is not. Partial functions are not intrinsic although you can model them. [Note: in many languages division really is intrinsic, since a division by zero exception is thrown, but of course not in C, since it has no exceptions]

With coroutines if you have a chain of calculations some of which are partial functions, you may or may not be able to read a result from the output of the end of the chain. If you can, you get an answer, otherwise your program just returns without saying anything.

Functional code is utterly different. It's not possible for a function chain NOT to propagate a result. So you have to invent a fictitious result or you cant get real results when they exist.

This is a model and it is unnatural in well defined sense: you have to say what the fictitious results look like (eg "division by zero" or "overflow"). Another person may invent different names or different result structure. Its an artificial framework, a model for the calculation.

You not have to do that with coroutines, in fact, you may WANT to do it and the problem is precisely the opposite: its hard to bypass the intrinsically correct design and pervert it with error handling. It easy to actually forget or misdesign the error handling for the simple reason that failing to output a result if there isn't one isn't an error.

You may think it should be. But in my parser, attempts to parse a string with productions that don't match simply don't produce a result and that's exactly what you want EXCEPT in one special case: NO result is found. In which case you want not only to know there's a syntax error, but where it is.

I agree all software is modelling but my point is that just because you can model things in an FPL doesn't mean you should: you should have a symmetrical system where you can switch design spaces to simplify your models. IMHO of course!

Your critique of division doesn't make much sense to me. An FPL can diverge and a co-routine can loop. An FPL can return an Either type, a co-routine can return control flow to another port. Either can raise an error. Where's the difference?

Math uses partial functions all the time, division arguably among them. While total functional programming is a thing, most FPLs can express partial functions and divergence. The infamous `(λx.(x x) λx.(x x))` is an example from the popular Lambda calculus underlying many FPLs. There is no need to return a 'fictitious result'. Simply not returning is an option, and seems a reasonable option when modeling partial functions from mathematics.

Types are a separate issue. Types are convenient for use in explanations or understanding code, for resisting errors, for overloading expressions. But we don't need them. If we type division with `Int → NonZeroInt → Int` to guard against divergence, that doesn't affect the model or definition of division. We're limited to the same computable observations as we were for `Int → Int → Int` (because we cannot observe a divergence). The type only affects the burden of proof for static type-safety of the program.

My concern about this approach is it makes performance unpredictable (in the same way that I think lazy evaluation does). For example the generic parser you wrote seems very slow, and I am not sure it is possible to solve this problem because of the way threads are launched to deal with parse options in parallel.

The half-way model of cofunctions retains a single thread of control, giving the programmer explicit control of what gets evaluated in parallel, and would seem to avoid this problem, whilst keeping the ability to model state co-functionally.

I am actually thinking that a further layer of abstraction on top of this will make it easier to use, so that we model objects, where methods are pure functions, that take private object properties as additional arguments, and return the new values for these private object properties. Effectively the object is a state machine. We then have two cofunctional views of the object; The internal one where the object is a recursive tail call of itself as a function that calls 'yield' as a function with the results, and yield returns the next command; and the external one where we call methods.

The thing that concerns me about this whole approach is that functions are no longer referentially transparent. Calling the same function with the same objects can produce different outputs. However I don't see how referential transparency can be maintained without threading the state. Monads, where the state is threaded but hidden, would seem to be the only solution to avoiding explicit threading and maintaining referential transparency?

You are correct about performance but this is not because of the coroutines. An dual parser can be written using purely functional techniques.

The functional version has an advantage and a disadvantage compared to coroutines: the functional version returns a set of all possible parses from each nonterminal so it does the same rescanning exactly as the coroutine model. However the functional version can easily MERGE the results into a set, ensuring there is only one representative of each unique result. The coroutine machinery cannot do that, because identical results can come in at different times.

The disadvantage of the functional method is that collections of results are expensive to represent. If you want a set, you're going to be using some kind of log N based tree. The coroutine system has no such problem, since it only handles one result at a time.

A partial solution is to merge both methods. The idea is similar to a Prolog cut operator. At some point, you gather the time series into a spatial set and swap back to the functional system. So for example, to do a cut, you would have a coroutine which acts as a sink and writes values into a physical set via a pointer to a mutable variable, adding only unique values. Then you drop into the functional model, grab set, and post it back up to the coroutine model.

So the idea there is to leverage the duality and the capability of using BOTH models together. Of course, the result is still not a linear parser but remember we're trying for run time combinatorial parser construction, so the if the user takes care you can write a grammar with good performance otherwise you get bad performance.

[Ref transparency issue another reply]

This sounds a bit like search strategies, where non-directed searches are inefficient. However we often don't want all solutions but a specific subset (or individual result). For example the greedy parser which consumes as much as it can with each rule. In many cases we just want to know if there is any solution, it doesn't matter if there is more than one. We can see this in Prolog's approach to logic problems contrasted with something like Answer Set Programming.

The disadvantage of the functional method is that collections of results are expensive to represent. If you want a set, you're going to be using some kind of log N based tree. The coroutine system has no such problem, since it only handles one result at a time.

The set does not have to be represented explicitly, and you can avoid the membership tests if you avoid calling the rule that would trigger them, i.e. via memoisation. Have you read this:
Frost, Richard A.; Hafiz, Rahmatullah (2006). "A New Top-Down Parsing Algorithm to Accommodate Ambiguity and Left Recursion in Polynomial Time" (PDF). ACM SIGPLAN Notices. 41 (5): 46–54. doi:10.1145/1149982.1149988.

Although it is describing the combinator approach in Parsec, it is written in a language-neutral style. Backtracking + memoisation is used to avoid the set-membership queries. Overall the control-flow is roughly similar to what you've described using coroutines although the memoisation avoids the need to eliminate left-recursion from the grammar first.

Ok, so I believe cofunctions, as a special case of coroutines, can be "pure" in some sense and provide "referential transparency".

First of all, in the abstract, simply swapping control back and forth between calculations so two cofunctions "help" each other clearly allows for pure and transparent operation.

Your problem is that you are NOT actually calling functions but closures which retain state. However the state which necessarily is retained is the "current continuation" of the cofunction so next time you call it you resume where you left off.

Because you are storing the closure in a variable, the exchange of control modifies the variable to hold a different continuation after each invocation so you lose transparency.

The problem is that what you *actually* get back from a co-call is a pair: the current continuation of the cofunction AND a value it yields. So you would just have to accept both to solve the transparency problem. For example like so:

let initcof = cof in 
let nextcof, v1 = initcof x in
let lastcof, v2 = nextcof (v1 + 42) in
v2

here, the cofunction cof is closed into initcof, but a call returns not only the value v1, but also a new continuation. This is nice because the old continuation is reusable, i.e. purely functional.

I think you can already do something like this in Scheme with continuations. This is more complicated than your previous encoding but it avoids losing referential transparency.

The yield would be unchanged, each yield does something different, but yield isn't a function so that may not matter.

I believe this is what we call "threading" the state where you have to keep track of what the latest version of a value is, and thread it through all computations that use or modify it.

What a monad does is different, you are still threading the continuation (so you keep referential transparency) but you hide the threading.

test x = do
   v1 <- cof x
   v2 <- cof (v1 + 42)
   return v2

Where the monad provides the method 'cof', which is updated by the Monads 'bind' function.

So the conclusion for me is you still need a mechanism like a monad to hide the state threading if you want to have referential transparency without explicit threading of state.

I wonder if a monad is the only way to do this? It may well be the simplest based on the types for 'bind' and 'return'.

Control types look as if they will be isomorphic to grammars (reads and writes replacing symbols) - were these the grammars with side-effects mentioned when you were asking about eliminating left-recursion?

If the control types define the I/O behaviours (interface?) of a multichannel coroutine, composition may prove to be difficult without finding an appropriate of restrictions.

Control types can be any sets of event sequences. The concept isn't mine, but appears in Hoare's CSP paper. A convenient way to annotate such sets may not exist in all cases, but for simple coroutines (or threads or processes) in which the only events of interest are basically I/O operations, then regular expressions are convenient if they're applicable. Failing that we have to hope we have a context free language, and use a grammar.

I think the issue is the same for spatial types: rough typing is OK, but if you want to get precise you need a dependent type system. And of course even that is not going to be enough (if it were, it would be unusably complicated).

So really the issue of types is what are reasonable approximations, and we probably need some notion of subtyping.

For example given two coroutines which are functional transducers of type (R1 W1)+ and (R2 W2)+ if we connect W1 to R2, the composite is NOT (R1 W2)+ because I specify that on a read/write match up, either the reader or write can go first. So you can get two reads in a row before anything pops out of the W2 channel.

Never the less the composite type exists and can be calculated mechanically. So you are right I believe, some restrictions are necessary.

But the problem is worse. Suppose I have several coroutines I connect in a network with channels. My question is: exactly what does the type information tell us?

Normally types allow type checking. But it isn't clear to me what that means for coroutines. In particular, coroutines regularly starve, block, and suicide, and none of these things indicates a fault. In fact without one of these things programs couldn't terminate!

I have written a parser as a demo using coroutines. It took a while to get it to work. I can reason about coroutines but it is not easy at the moment. Note that coroutines are strongly related to Hoare's CSP: replace "concurrent" with "indeterminate". Coroutines are simpler and should be understood before venturing into concurrency, if only because all massively concurrent programs will essentially run coroutines in huge numbers inside a small number of actual processes (that's how Go works).

I have an advanced example of how to use coroutines: a parser which can parse from a context free grammar.

Is there a demo to look at, which shows this? I found pars.flx in your github but it had simpler examples in it. It would be interesting to read something that shows parsing from a CFG.

I'm not quite sure what you want to see. There is a working non-trivial parser text case here now:

https://github.com/felix-lang/felix/blob/master/chk2.flx

An example in the CFG DSSL looks like:

    factor = 
      | factor "*" factor { BINOP("Mul")}
      | factor "/" factor { BINOP("Div")}
      | factor "%" factor { BINOP("Mod")}
      | prefix  
    ;

I call this an *action grammar* because it also has actions, like all real world parsers PL parsers do. The action here is BINOP ("Mul") which is an AST constructor for binary operator named MUL. From a grammar viewpoint this is a unit (epsilon). Because the grammar is left recursive the test case has to run the left recursion eliminator function. Critically, this has no impact on the AST generated.

Now, the thing is, none of this shows you anything at all about the parser implementation using coroutines: the grammar terms generated are symbolic initially, which you should read as "lazy". This is so we can actually detect things like left recursion. Once we have a refactored grammar that we're happy with we can render it into an actual parser (using make_parser_from_grammar). The coroutines are hiding inside that.

you are using is ambiguous. Imagine parsing an expression: 1+1+1, it returns at least these: (1+1)+1 and 1+(1+1). Sure you can take only the first parse, but let me propose something like this:

<Start>   ::= <Sum>
<Sum>     ::= <Sum> ('+' | '-') <Fact>
            | <Fact>
<Fact>    ::= <Fact> ('*' | '/') <Exp>
            | <Exp>
<Exp>     ::= '(' <Sum> ')'
            | <Integer>
<Integer> ::= [0-9]+

Why is this better? Firstly, it returns only one tree instead of a forest. And secondly, it handles operator precedence without even one additional line of code. You can even create a right recursive version, just swap the sequence parameters.

If someone is interested in general CFG parsing algorithms that support left recursion (at least for an inspiration), I propose to take a look at CYK parser, Earley parser and GLL parser algorithms. I think CYK should be the slowest one and GLL should be the fastest one of these three, but I didn't test them all, I just saw somewhere that Earley beats CYK. My javascript implementation of Earley takes about two seconds for one thousand lines in a fairly simple grammar, but it chokes cubicly on right recursion.

Yes, that grammar is ambiguous and the parser would return all the parses. The point is to test the behaviour of the coroutine based parser.

The parser is not efficient. The point was to see how coroutines could be used in a real example.

A second point is that what I call action grammars can be refactored without changing the AST they generate.

I think that is what I wanted to look at, I will go and have a read. I was curious what the mapping from grammar to co-routines looked like, and what kind of structure the output machine would possess.

The mapping is roughly one to one. The actual code is in two levels. First I define recognisers, the parsers are layered on top of them. The really interesting file is src/packages/chips which provides a set of core coroutines. This is the key one, which handles alternatives:

chip tryall_list[D,C with Str[D]] (a: list[iochip_t[D,C]]) 
  connector io
    pin inp: %<D
    pin out: %>C
{
  while true do
    var x = read io.inp;
    for h in a do
      var lin,lout = mk_ioschannel_pair[D]();
      spawn_fthread (h (inp=lin, out=io.out));
      write (lout,x);
    done
  done
}

Note this is 100% generic, it has nothing to do with parsing. Same for this one:

chip pipeline_list[T] (a: list[iochip_t[T,T]])
  connector io
    pin inp: %<T
    pin out: %>T
{
  proc aux (lst:list[iochip_t[T,T]]) (inp: %<T) {
    match lst with
    | h1 ! h2 ! tail =>
      var inchan,outchan = mk_ioschannel_pair[T]();
      spawn_fthread$  h1 (inp=inp, out=outchan);
      aux (h2!tail) inchan;
    | h1 ! _ =>
      spawn_fthread$  h1 (inp=inp, out=io.out);
    endmatch;
  }
  aux a io.inp;
}

And I use this which is tricky:

chip deref_first_read[D,C] (p:&iochip_t[D,C]) 
  connector io
    pin inp: %<D
    pin out: %>C
{
  var x = read io.inp;
  var rinp,rout = mk_ioschannel_pair[D]();
  spawn_fthread ((*p) (inp=rinp, out=io.out));
  write (rout,x);
  while true do
    x = read io.inp;
    write (rout,x);
  done
}

What happens is that each "symbol" in a production is created as a closure on the heap and a pointer returned and stored in an array. The above coroutine dereferences the pointer. The reason for doing this is to support forward references and recursion: a level of indirection is required to infinite expansion in the rendering routine which translates the lazy symbol form of the grammar (which uses strings for non-terminals) into an executable network of coroutines.

This function translates a grammar to a recogniser (there's a similar but longer function for parsers):

fun render_prod 
  (lib:gramlib_t,v:varray[ntdef_t]) 
  (p:prod_t) 
: 1 -> recog_t =>
  match p with
  | Terminal (s,r) => { r }
  | Epsilon => { BaseChips::epsilon[Buffer] }
  | Seq ps => { BaseChips::pipeline_list (
      map (fun (p:prod_t) => #(render_prod (lib,v) p)) ps) }
  | Alt ps =>  { BaseChips::tryall_list (
      map (fun (p:prod_t) => #(render_prod (lib,v) p)) ps) }
  | Nonterminal nt => 
     { 
       var idx : size = find v nt;
       var pslot : &ntdef_t = -(v.stl_begin + idx); 
       var pchip : &recog_t = pslot . 1;
       return BaseChips::deref_first_read pchip;
     }
  endmatch
;

So this show how the symbol combinators translate to executable ones.

I'm exploring process networks as a promising basis for imperative effects. A process network value can support background parallel computations and communications, can be composed in flexible ways, and naturally supports multiple inputs and outputs over time and hence can model generators, animations, interrupts, etc.. The network is semantically just a value, so it can also be copied, serialized, returned from a function, passed as an argument or message, etc.. But a language interpreter or compiler can optimize evaluation of these values to leverage physically distributed processes.

but leaves open the question how to specify and use control types (the set of events the processes can engage in).

If the process is an object (modelled as a state machine), the set of events and responses it can engage in are the methods. So the type of a process is effectively a record containing all the method types labelled by the method 'id'.

But that doesn't help with the sequence of the methods: the control type is concerned with the valid sequences of method calls.

Also remember, a process is the control inverse of an OO object. So it is not a passive receiver of method calls, but rather an active entity which calls these methods, that is: the process is calling the methods, whereas with OO the environment calls the methods.

Thus the process enforces protocols by calling methods in proper orders. If it is communicating with another process, then both will call each other with matching method calls. So the question is: will the sequences of method calls made by these two processes actually line up?

This question is much simpler for cofunctions since there is only ONE method (yield) and only ONE pair of types which can be exchanged so the only "variable" is the number of calls. And my problem is: so what if there is a yield for which there is no matching fetch? One side has just terminated the exchange, but that doesn't mean its a bug if the other side is expecting stuff that never comes. In fact .. this would be the norm!

The point I was making is that objects are a special case where the set of accepted events is always the same. If you look at the suggestion of returning the continuation explicitly, you could think of an object method as having the type "Obj.(Int, Int) -> (Obj, Int)" where "Obj" is type nominal type of the object. Now we can see that a protocol can be encoded like this:

Obj1 {
   a : Int -> (Obj1, Int)
   b : Int -> (Obj2, Int)
}

Obj2 {
   c : Int -> (Obj1, Int)
}

Here we have a protocol where if we are in state "Obj1" we accept messages "a" and "b". With "a" it remains in state "Obj1", with "b" it transitions to state "Obj2", where it expects message "c", which transitions it back to state "Obj1".

Edit: I would suggest that there always should be a response, you just return unit when you don't need it. That's because I want a single thread of control, but you could have 'no return' simply by only encoding the state transition as in "d : Int -> Obj3" where Obj3 has no methods if it is a terminal state.

The analog to 'simply typed lambda calculus' would be to assign a message type to each port. That's easy to specify and use. But it isn't very precise or expressive and would not prevent a network datalock. I've been thinking about how to do better.

Some intuitions:

One might attempt to characterize a process network (including subnets and individual processes) in terms of a grammar processor or state machine, where input sentences are transformed to output sentences. An input sentence would prefix each input message with the port identifier, and the 'output sentence' would prefix each output message with the port identifier. If our ports are simply typed, this reduces to a series of port identifiers, which are the basic words of our sentences.

Session types could be adapted. A process network can be treated as a single linear channel or session containing all the input and output messages. We would need some careful attention to how composition of networks impacts the type (hiding internal wiring and events, etc.), but our actual type descriptors could feasibly be based on session types.

We also can characterize a process network as a linear object with methods representing ports (input or output) and each injecting/extracting some data and returning the updated network. By returning a network of a slightly different 'type', we could feasibly model rich control types. (Related: typestate in Plaid, and Keean Schupke's comment above.)

Process networks, semantically being values (like pure functions), seem a simpler target than imperative coroutines or conventional objects where one must worry about state aliasing. Aliasing resists typestate and local reasoning about or refinement of types.

Felix coroutines are procedures, hence imperative. A fibre is roughly a non-concurrent version of a process in Hoare's CSP. Felix has functions too.