Lambda the Ultimate

Incremental computation + state preservation is necessary to make immediate-mode abstractions convenient and performant. And once you go immediate-mode, you don't need FRP anymore (for building user interfaces).

Ok, the above discounts the whole reasoning about the past via event streams aspect of FRP.

Immediate mode GUI libraries end up structuring themselves very naturally as FRP-style libraries. Since you redraw everything on every tick, simple temporal abstractions like streams and futures work extremely well, because there is naturally a global clock which governs when everything happens.

OTOH, retained mode libraries are far more challenging to formalize in FRP. The scene graph is fundamentally a gigantic shared mutable data structure, which gets manipulated via imperative callbacks, which are idle until they fire at potentially distant times in the future. The temporal and aliasing structure of the DOM/scene-graph/etc is super-intricate, and so decomposing it into simple primitives is very hard. (I've been working on this for the past year, and I think it's possible, but I couldn't tell you exactly how yet.)

If your UI is running in an infinite render loop, a procedural x = y + z will always be re-evaluated inside that, so continuous behaviors, at least, are no longer necessary. Where FRP diverges from immediate mode is with discrete event streams. In immediate mode, you simply handle the event on the repair where it is raised, and trap the effect into external mutable state that is preserved across repaints!

Implementation wise, I find doing Glitch over retained WPF is OK, you just remember what you added before and remove the difference. I would never dream of formalizing anything, however.

Even giving it a sensible specification is really, really hard, and proving that an implementation actually meets that spec is even harder than that. Basically, you have to show that in the limit as the sampling rate goes to infinity, the implementation will behave the same way as the spec. This is hard, and I'm not sure this is actually a good idea, since programmers and UI designers often seem to want to do things differently at different frame rates.

Once you accept that discrete time is OK, it's easy to see that streams are actually --- state machines! Consider a state machine as a triple $(Q \in \mathrm{Set}, q \in Q, t : Q \to \Sigma \times Q)$, and you can see that the transition function $t$ will emit a new symbol in $\Sigma$ and transition to a new state. If we don't observe the state directly, then what we can see is a stream of symbols. So stream operations like unfold and map are basically a way to build up state machines from smaller ones.

By continuous, I always mean "the stuff that isn't directly exposed to discrete time"; so "x = y + z" I mean that x is updated whenever y or z change, but they can only change discretely (so x can only change discretely, and so on). So continuously over discrete steps :)

I never got why pure FRP decided to include real continuous time; it seems difficult to realize in practice. We still get a measure of resolution independence if tick dependent computations are aware of the time step (like a physics engine would be).

...of why you might want the step size to be exposed by the UI layer to clients. (Unless you want to argue that a UI library should also supply a physics engine, which is reasonable as a matter of actual fact, but makes me cringe.)

Anyway, I find I prefer making time-varying things into explicit temporal abstractions (for instance, but not limited to, streams), rather than implicitly lifting all computations into time-varying ones. It seems like you end up needing with a lot of heuristics and optimizations to make the changeable values big enough that the overhead of change-management is reasonable, and AFAICT it doesn't really work with higher-order functions anyway.

So the story I want to tell about the programming model is "Start with a simple functional language, like you already know, and then add some very basic machinery for talking about time. Everything else, like streams and futures and so on, is programmed up using the basic primitives."

Isn't that the Rx approach? Focus on the wiring; fold, map, filter...

Declarative programming in its very essence is the ability to ignore time, or at least have a sane view about it. Being able to provide the illusion that computations occur at the same time (x = y + z occurs concurrently with assignments to y and z) is very powerful.

I don't really want to ignore time, because programs naturally want to support decisions based on the time (eg, letting users cancel downloads that are taking too long). To make this easier to get right, I want to typecheck the temporal behavior of a program.

This means reifying things like "downloading files with progress info" as first-class values. And the surprising thing is that these things also have sensible types! E.g., you can type a downloading file using the until operator of temporal logic -- it's a value which gives you progress info until it gives you a file, and then it's done.

The wiring just falls out of this approach, as the operations each kind of temporal gadget naturally supports.

I very much agree with this sentiment. Explicit time - be it discrete or continuous - is very useful and natural in a great many problem domains, and further is useful for many cross-domain concerns like process-control, concurrency, and scheduling.

Interrupts seem like a bad hack to work around atemporal conventions for expression of computation.

Where do I buy this programming language? :-) Really...

I guess I'm not very confident in rigorous approaches. I like the ideal that the type system can represent many things, but the result is often either undecidable or a complex mess that no one can use. I'm not trying to be discouraging, and would love to be proven wrong.

Take "downloading files with progress info", no type system can really help out given unreliable networks, and the problem is basic enough that some extra boilerplate is sufficient and tolerable. But I guess this gets at the crux of the argument: where should abstraction be applied and boilerplate be removed. The answer probably isn't "everywhere", we just have to relieve the most common pain points.

If you're thinking of encoding complex invariants into general-purpose type systems (like Haskell or Scala), then I agree -- which is why I'm looking at special-purpose type systems. When you look at, say, temporal logic specifically, then the type-based invariants start to look like the invariants programmers talk about in English, which makes the error messages more comprehensible.

I'm also interested in the other side: GUI toolkits are *enormously* complicated, and I think a lot of that complexity arises from handling unneeded-but-possible corner cases gracefully. My ICFP paper from last year illustrates this point -- some careful use of types permitted greatly reducing the amount of machinery you need relative to other reactive libs like Flapjax and Scala.react, while still increasing overall expressiveness, because the edge cases that you don't actually want were statically forbidden. I'd like to do the same for MVC!

Does temporal logic still boil down to products and coproducts?

Eventually : now OR later
Always: now AND later

The computational interpretation of Always is familiar as a Stream: now is the head, later is the tail. Eventually is less familiar. But it could be encoded as the Demorgan dual:

Eventually x = NOT Always NOT x = NOT (now NOT x AND later NOT x)

which seems to correspond to a continuation accepting a stream of continuations. Now given that Always x implies Eventually x, this provides an alternate encoding of a Stream.

A Restaurant comes to mind: it's a consumer of a sequence of diners - each of whom is a consumer of a meal, i.e it's a consumer of consumers of meals ~= a producer of meals.

Is this how I can get to the Rx Observable type? I.e Observable of x ~= Observer of Observers of x, which corresponds to its "subscribe" operation? Meijer mentions the continuation monad but this seems to be something fancier.

As far as computer graphics, time can be treated as a 1-dimensional affine space (translation and scale) in which case "animation clips" can be seen as analogous to 3d visual primitives. The playhead takes the role of the camera (translation and scale correspond to forward/rewind and changing the play rate). You can have an animation clip hierarchy with local timelines analogous to the visual 3d transform hierarchy. As the playhead raycasts into this hierarchy, you have animation blending analogous to the blending of transparent meshes (for animation clips that can play simultaneously).

For interactive programs, you also have events, e.g mouse, keyboard. Here you also need effects. Apparently you could have a "pull" effect, that lazily pulls a stream of frame buffers from a stream of events. Or a "push" effect that eagerly sends in events. These seem to correspond to a lazy comonad and an eager monad? Can you have both? The lazy memoized pull reactivity seems to fail for the Unit type - e.g if you tried to model button clicks as a Stream of Unit. After memoization you'd have only a single click forever. It also seems like you'd like to zip together lazy and eager streams. For example, in a drawing program you could change the brush color and then drag the mouse to draw something on the screen. The output on the screen zips together both the color and the mouse coordinates, but only the latter creates new output. Apparently Rx CombineLatest tries to provide this?

It turns out that when you turn temporal logic into a programming language, the always modality turns into *two* types. First, it turns into the type of streams. So the type of streams of X:

    S(X) = μα. X × next(α)

is read as "a stream of X's gives you an X now, and gives you anoter stream starting tomorrow." This tells you that you potentially get a different X on each time step.

However, you also get another notion of always, which I wrote â–¡X. This is a value, which you can use as an X now and at every point in the future. Unlike a stream, you know that the *same* value is good at every time step.

When you dualize streams, you get an "eventually" operator:

    E(X) = μα. X + next(α)

This tells you that on each tick, you either get an X, or you told the computation is still running, and you get an E(X) on the next tick. In semantics, this is a type of "resumptions", and in programming terms, these are a type of promises or futures. Specifically, they are a type of futures which permit you to query them to find out if they are done or still running.

But, because we have two notions of always, we also get two notions of eventually. If you use the de Morgan dual on the box operator, you get a type like:

    ⋄X = ¬(□(¬X))

Negation is computationally a kind of continuation, and you can view ¬X as a type X → ans, where ans is an answer type. Taking it to be IO () (using Haskell notation), we get:

    ⋄X = □(X → IO ()) → IO ()

That is, says that if you have an action taking an X as an argument, which you can evaluate any time, then a â‹„X is something which will invoke that callback when X happens. So it's the type of an onEvent handler! I think this second notion of eventually is the type of promises which you *can't* query if it's done, because they will run asynchronously.

I say "I think", because I (and my collaborators) haven't yet worked out how to *prove* this second notion of eventually works the way we think it does. But we're working on it!

S(X) = μα. X × next(α)

Should streams be formed with nu? And eventually with mu?

¬(□(¬X)) [... becomes ...] □(X → IO ()) → IO ()

I don't see how that substitution works. Isn't it:

¬(□(¬X)) = □(X -> f) -> f = □(X -> forall a. a) -> forall a. a

It looks like the quantifiers don't support it.

In the situation with ordinary continuations, you have that (X -> f) -> f is not constructively equal to X, but you can add callCC to convert. Shouldn't we expect something similar here, where â–¡(X -> f) -> f is classically equal to an existential -- an X from some time, but we don't know which. It looks like the only thing you could do with such an existential is use it in types that are known to work with an X from any time.

1) Yes, you can form streams with mu and eventually with nu -- I just assumed that we had full recursive types where the two coincide.

¬(□(¬X)) [... becomes ...] □(X → IO ()) → IO ()

I don't see how that substitution works. Isn't it:

¬(□(¬X)) = □(X → f) → f = □(X → ∀a. a) → ∀a. a

In the CPS transform, a base type X gets translated to a type like (X → a) → a. However, the transformation is parametric in the choice of the "answer type" a -- you can make any choice you like. It has to be the same choice for the whole program, but it doesn't matter what that choice is. So the intuitive idea is to use that freedom to specify a type of imperative commands which preserve the invariants the event loop and GUI toolkit expect, and then use the parametricity of the CPS transform to ensure that all of the code the programmer can write respects that invariant.

The idea is to give the programmer the full freedom to organize her code however she wants, using her whole programming language, but ensuring that the invariants of the runtime system are maintained. In this, it's very much like GC -- there are complex invariants about the GC, the stack layout, and heap structure, but every ML or Haskell program you write preserves those invariants.

I had the same question Matt had. Does it make much sense to see IO () as ⊥. Since, constructively, ⊥ is a proposition for which you cannot construct evidence, I guess there is an analogy to IO a. But at the same time one assumes IO a is a value/has an inhabitant. Maybe IO () corresponds to something where you know you have evidence but you cannot know what that evidence is?

And then there is the point that I imagine you construct an IO () value exactly at the point where you see something in the input stream; which is somewhere again exactly opposite of X → ⊥ being true. But maybe that even makes sense in a twisted manner. If you don't have X → ⊥ then you have X → IO()? Yah. Maybe.

Yes, you can form streams with mu and eventually with nu -- I just assumed that we had full recursive types where the two coincide.

Yeah, that makes sense. I guess the two coincide in e.g. Haskell. I hadn't noticed that before. Thanks. (I think you may have swapped mu/nu. Streams are co-inductive, eventually is inductive?)

In the CPS transform

OK, so you're doing a whole program CPS transform, and you're hoping that the existential type can be made to correspond to something after CPS transform. I'd be interested to see the details worked out.

I looked at your paper again, and I'm skeptical about working in a temporal logic. How do you imagine this framework being integrated into programming practice? Wouldn't your proposed system require sprinkling â–¡ all over the place for definitions that aren't temporal? Or not?

OK, so you're doing a whole program CPS transform, and you're hoping that the existential type can be made to correspond to something after CPS transform. I'd be interested to see the details worked out.

No, you don't end up CPS-converting the whole program. Only the asynchronous eventually type is implemented with a double negation, essentially like using a continuation monad in ML or Haskell.

I looked at your paper again, and I'm skeptical about working in a temporal logic. How do you imagine this framework being integrated into programming practice? Wouldn't your proposed system require sprinkling â–¡ all over the place for definitions that aren't temporal? Or not?

Top-level definitions are not time-varying, and so don't need to be annotated. As a result, you only need boxes when you define a temporally recursive process that uses a value at many different times. I actually find it very nice to program in.

i'd like to say it is ok to link to your paper, it shouldn't come across too much like advertising :-)

The paper is Higher-Order Reactive Programming without Spacetime Leaks. Basically, the moral of the paper is that with the right type discipline, unadorned call-by-need evaluation gives you everything you need for the right space behavior.

You can also download an almost completely undocumented implementation right here. It implements the system in this paper, together with the linear type system from my earlier ICFP 2011 paper A Semantic Model for Graphical User Interfaces. It works by compiling programs into JS, which you need to run in Firefox (which supports more ES6 extensions than other browsers).

I'm just starting to do a reimplementation of this language, this time with dependent types.

Imperative code, and imperative read/write state models, do not readily support continuous time.

But continuous time is a significant part of reactive demand programming (RDP), and I've developed some flexible state models and rules for creating more. Essentially, if we have continuous time + discrete state changes, we must also have either fixpoint behavior, or idempotent updates (which essentially gives us fixpoint behavior), or a model that limits the number of updates in a given period of time (thus forcibly distributing updates through time). The latter can be modeled using energy, power, queues, timeouts, etc.. Using these various techniques, we can model tuple spaces, term rewriting, state machines, and many other things in continuous time. Continuous state change is a more natural fit with continuous time.

I would not say that continuous time is especially difficult. However, it is different, and a lot of imperative idioms don't work nicely with it.

programmers and UI designers often seem to want to do things differently at different frame rates

Using continuous time does not hinder this at all. To the contrary, continuous time might actually make it a bit too easy to model different things varying with different rates or periods, which can be problematic because it it results in some awkward beat frequencies with respect to program performance characteristics.

One might be wise to choose to artificially constrain the rates users can choose, to ensure they align in simple ways and make it easier to analyze simple periodic behavior, thus effectively using a discrete-time subset of continuous time when modeling discrete actions.

accept that discrete time is OK

Continuous time has a few advantages over discrete time that would make me reluctant to give it up. First, logical continuous time aligns well with wall-clock 'real' time, which makes it easier to use when composing open systems where agents may be coming and going at their own schedules. Second, continuous time works very nicely with common 'bursty-stable' update patterns, where subprograms are stable for long periods of time then update in short bursts; this also applies if we have many orders-of-magnitude variation in periodic frequencies.

AFAICT, discrete time works best in a confined system where most of the model updates in each timestep. Multiple independent discrete-time models tend to compose in a non-deterministic manner. Memoization techniques can help with bursty-stable update patterns, but (in my experience) are relatively awkward.

I'm not sure that you're disagreeing with Neel. Continuous time fits into the model he was advocating just fine as long as it's just continuous parameterization. That is, a stream of functions (t:Real -> X) is fine. It's when you're allowed to ask questions like 'what is the first time at which this function is non-negative?' that you're heading into a thicket.

It's when you're allowed to ask questions like 'what is the first time at which this function is non-negative?' that you're heading into a thicket

Yes, these questions can be difficult - if you're allowed to ask them, and we have continuous state (not just continuous time).

I've occasionally wondered about representing continuous state symbolically, e.g. using piecewise trigonometric polynomials, such that such questions can be answered. However, continuous state isn't as important to most of my use-cases, and I've chosen to not support it natively.

If I'm able to write f(t) = (t - 1/2)**8 and then ask for zero crossings of f, the problem is already intractable, right?

When I say 'continuous state' I really mean 'continuous-varying state'. Similarly, I often say 'discrete state' as shorthand for 'discrete-varying state'. And by 'varying', I mean over time.

We describe state with a value. Not all descriptions admit continuous state. E.g. if I have a function of type `Time → String` or `Time → Integer`, then I know that the state value varies at discrete times regardless of whether Time is continuous. If I have `Time → (String,Rational,Integer)`, only the Rational element can potentially vary continuously with time. If I have `Time → Tree of Rational`, then I know the tree structure is necessarily discrete-varying, but the values contained within the tree may vary continuously.

It is, of course, possible to model continuous-varying types more explicitly within a type system, i.e. such that `Rational` by itself does not imply the possibility of continuity on the temporal axis. By doing so, we can also restrict expressiveness of continuous-varying state, to make questions about it more tractable. There are many important problem domains (e.g. animation, robotics, sound synthesis) where even a severely limited expression of continuous-varying state values is very useful.

I don't directly support continuous-varying state or value types in Awelon, but I can imagine modeling them indirectly and developing a DSL that supports them.

If I'm able to write f(t) = (t - 1/2)**8 and then ask for zero crossings of f, the problem is already intractable, right?

I don't believe so. In this case, the only zero is t=1/2. Roots are relatively tractable for certain fixed-form polynomial and trigonometric polynomial functions like this one, e.g. that can be described by a vector of coefficients and a time offset.

In any case, I can't think of any use-cases for embedding hard-coded time values (like the `1/2` in `t-1/2`) within reactive code. Indeed, in RDP I don't even directly allow developers access to the time value `t`; they may only access it indirectly through interactions with temporal state models or resources. Expressiveness can be limited much more than you're suggesting without much damaging the utility of continuous-varying state.

I'm not following exactly what your setup is. In some places it sounds like you're modelling time as with rational numbers, but then you say that Time → Integer varies discretely. But consider this function of type Ratio → Integer which is discontinuous everywhere:

f(p / q) = q -- p, q relatively prime

Even if you model time with Reals, I don't see how you're going to get a discrete set of changes. Consider this function:

f(t) = if t > 0 then floor(1/t) else 0

The discontinuities are dense around t = 0.

Denying absolute time literals seems fine, but I don't see how it helps minimize any of these issues.

consider this function [...]

I don't need to consider arbitrary functions. I only need to consider the subset of functions developers are able to express constructively.

I do model time using rational numbers. But (a) developers cannot directly access time in order to express functions on it and (b) my Awelon bytecode doesn't provide any operators to observe the numerator and denominator of a rational value. These conditions would render both of your examples inexpressible.

I suspect you're tackling the whole problem of continuous-varying state in an unnecessarily difficult way. Instead of asking "how can I take arbitrary functions and prove them safe for such and such a use-case?", try "can I find a safe, compositional subset of continuous-varying functions that covers (or adequately approximates) my use-cases?". We can get most of the benefits for continuous-varying state for relevant use-cases (robotics, animation, physical simulations and collision detection, etc.) with only a fraction of the hassle if (when we use continuous values at all) we stick to piecewise-continuous polynomials or trigonometric polynomials.

Therefore, I use those those and I'm free to ignore irrelevant concerns involving floor functions with time in the denominator, or involving decomposition of time values relative to some arbitrary zero.

In some places it sounds like you're modelling time as with rational numbers, but then you say that Time → Integer varies discretely.

Regardless of how Time is modeled or varies, Integers cannot vary continuously. The closest we can get is piecewise constant, which is really just another way to describe discrete variation. (But there are many qualitative differences between discrete variation in continuous time vs. discrete variation in discrete time.)

Denying absolute time literals seems fine, but I don't see how it helps minimize any of these issues.

Even with `Integer → Integer` we can ask impossible questions. But, for the most part, we don't have reason to ask them, and it is quite feasible to create languages with limited expressiveness where every function of `Integer → Integer` is computable, and which are adequate to support our program requirements.

The same principle applies for `Real → Real`. Most of the issues you're raising... aren't.

I missed the context that you were just talking about functions of a limited form.

I suspect you're tackling the whole problem of continuous-varying state in an unnecessarily difficult way.

Well, I'm not tackling it at all.

can I find a safe, compositional subset of continuous-varying functions that covers (or sufficiently approximates) my use-cases?

If you mean all use-cases, then I conjecture the answer is 'no'.

piecewise-continuous polynomials or trigonometric polynomials.

This set isn't even closed under addition. So you can represent the coordinates of a point on a falling object or on a rotating object, but not on a falling, rotating object? If you need rotation and acceleration, you what... switch to a periodically updated best-fit polynomials? That's a bunch of math to approximate something that's easy to calculate.

Approximation by piecewise-nice functions has its place in many projects, but I'm skeptical that you want to choose what 'nice' should mean for all reactive programs. Reactive programming is very general and powerful and I think you're introducing features that will be worked around as much they're used.

Approximation by piecewise-nice functions has its place in many projects, but I'm skeptical that you want to choose what 'nice' should mean for all reactive programs.

Sure. I share this skepticism. Which is why, as I wrote above, "I don't directly support continuous-varying state or value types in Awelon, but I can imagine modeling them indirectly and developing a DSL that supports them." Continuous time is widely useful. Continuous-varying state has more specialized applications. I see no need to conflate the two, nor to couple them as a feature.

you can represent the coordinates of a point on a falling object or on a rotating object, but not on a falling, rotating object? If you need rotation and acceleration, you what... switch to a periodically updated best-fit polynomials? That's a bunch of math to approximate something that's easy to calculate.

Using an ad-hoc functional representation, something like 'the coordinates of a point on a falling, rotating object' can be relatively easy sample. But if we want to ask or calculate other properties of the model, such as whether that point touches another object, we'll often find utility in more rigid expression.

It is true that periodically updated best-fit polynomials are quite messy on the small scale. But it's a relatively controllable mess - one that doesn't get much worse as we compose functions or deal with representing real-world messiness (e.g. modeling the motion of a mouse pointer or pen).

The blog post describes a variation of React, called Bloop, for didactic purposes. Bloop renders the whole DOM each frame (via requestAnimationFrame), but uses a React-style difference computation to determine what actually needs changing. In this sense, Bloop is very similar to Immediate Mode - arguably more so than React.

Can't find a description of this difference computation in the docs. Anybody have a link?

Yeah. And with pretty pictures in a separate blog.

Thanks, that's helpful!

Yuck. Just modify the com directly since it's retained. In Glitch, this could just be:

var div = new Div
if first:
  div.className = "first"
  div.node = new Span { node = "A span" }
else:
  div.className = "second"
  div.node = new Paragraph  { node = "A para" }

Glitch memoizes allocations and assignments, so...if nothing changes, no changes are made to the DOM, if first goes from first to false, two assignments are rolled back and one object is deallocated, while two assignments are installed and one object is allocated.

The diff is implicit in the log and doesn't need to be computed.

Maybe I should write a web framework. Edit: why is a virtual DOM needed, wouldn't the browser also batch reprinting changes to the DOM itself, like WPF does?

why is a virtual DOM needed, wouldn't the browser also batch reprinting changes to the DOM itself, like WPF does?

I can think of a few reasons for a virtual DOM:

1. a virtual DOM can be extended in flexible ways that a browser's native DOM cannot, e.g. introducing the 'key' attribute, or introducing new abstract tags
2. browser native DOMs are notoriously slow, and haven't kept pace with the improvements in JavaScript's performance
3. a virtual DOM allows us to simply generate a fresh DOM instance from model state, without acknowledging or explicitly updating the prior DOM instance

The second point could be addressed by better browsers that can support batching, diffs, incremental rendering, and atomic swap.

The third could be addressed by Glitch, RDP, or other reactive models, but that sort of overhaul for browser technology would be a significant overhaul of browser technology - a hard sell due to the enormous network effects.

I would like to develop a browser based on my own reactive model, but I similarly don't have much hope for its success in the current browser's domain of competence; I'm thinking VR or AR might be a better area to target these improvements. Meanwhile, something like React (together with WebSockets) would be an excellent basis for integrating browsers as they exist today to a more reactive model.

So then is React just a standard retained-mode UI with some syntactic sugar? I honestly can't tell.

React is not retained mode, at least in the sense that React developers do not directly manipulate the retained DOM, nor even a virtual representation of the DOM. They instead generate a fresh virtual DOM after each state update to their model (modulo use of caching). The difference between one virtual DOM and the prior is computed to update the real DOM.

But conventional immediate mode UIs (and Bloop) are driven by a timer, rendering in each frame, whereas rendering in React is triggered by any change in the model state. This can be more efficient for web-apps which remain inactive for long periods between bursty updates, albeit at a manageable risk of a model change going unnoticed if React's clients aren't careful to use React's state update methods or triggers.

I'd say React is closer to immediate mode than to retained mode, because it 'renders' the whole DOM rather than updating it manually. Bloop is simply even closer because it's timer based.

Ah, perhaps we should manage time in language runtimes like we manage memory.

I'm aware of your work on Glitch. One of these days I'll write up my thoughts about it in its respective thread. However, I'd like to address what it even means to "manage time" or even more generally what it means to manage "resources".

On the topic of managing memory: Some in the C++ community will argue that RAII is the way to go and garbage collection is wrong. Besides provably nonsensical claims about GC performance, there's a philosophical argument that memory shouldn't get any special treatment because it's just another resource. Assuming that you believe, as I do, that garbage collection has (rightfully) won, you may still be swayed by the "memory is not special" argument. You may have decided that automatic memory management is just too convenient to avoid special casing it. However, I don't think that memory is just another resource. I think that it's the *only* resource that exists from the perspective of your program.

All resources are backed by memory. This includes all other computation resources, such as file handles, and even external physical resources such as the humans sitting around waiting on a match making server for a chess opponent. Different resources naturally have different life times. If you don't write it down in memory somewhere, it doesn't exist from the perspective of your code.

Garbage Collection handles the lifetime of "reachable" data. RIAA handles lifetimes that are tied to the dynamic extents of evaluation, such as an output file handle. React's state model handles the lifetime of objects that are in the rendered output. Timeouts on network connections can act as a proxy for the lifetime of a potential chess opponent. Allocating or freeing any of these resources implies allocating or freeing the memory that stands in on behalf of those resources.

When we talk about the lifetime of objects in React.js, we need to consider what happens if we want stateful widgets that outlive their presence in the dom. Right now, the best we can do is to promote the component-local state to application model-state and rely on the garbage collector. At that point, we need to explicitly name state and manually evict it when we no longer need it. If you have a two-tabbed view with stateful components on each tab and toggle between them, you lose your state... unless you 1) overdraw or 2) store the state at the model level. Neither of which are attractive options. I may wish for that state to live as long as the document it is associated with. Or I may wish for it to live as long as my current usage session. Or I may wish for it to live until I click the "submit" button.

Storing state at the model level is no different than adding or removing objects from a database. And managing data in a database is essentially reference counting. Deleting a row in a table might as well be `set refcount = 0`. This is also true of the traditional OOP model for UI widgets. Calling `panel.addChild` or `panel.removeChild` is essentially manual reference counting. This tradeoff makes sense for long-lived data in your system of record, but not for UI state.

In my head, there is a sort of gantt chart of lifetimes which I'd like to see reified. If each bar represents a concurrent process and all resources are tied to those bars, then one can begin to work with time as if it were space as well. Assuming such a lifetime graph lives in a root mutable cell, reachability from the vertical "now" line covers all of your resource management bases.

Whew. That was much longer and less coherent than I hoped it would be. That probably means I don't understand this vague notion enough to really justify talking about it. However, since it's already written, hopefully you found it interesting.

The best way I see to equip a nice high level language with the ability to be systems language is to make the representation selection step explicit. We need to be able to reason about abstract values and, when appropriate, reason about representations of those values. Whether or not to use garbage collection (for memory, files, or other resources) is a representation issue.

Rust goes in that direction, I think, but they seem to be backtracking a lot. It is not as easy as it sounds!

I've looked into Rust briefly a few times and I don't think they're doing this, exactly. They were looking to make their values parametric in representational choices, but all of that complexity still permeates their values.

Can you elaborate on this? I'm not sure I understand this (or actually -- I'm quite sure I do not). Do you intend to separate the representation selection from the rest of the program? If so, how?

There is some support for this in Ada. While not really "separate" from the rest of the program, specifying some representation information via a separate declarative layer seems somewhat feasible, ie. alignment, packing, etc.

Finding a modular way to represent the representations is tricky. It's the same problem, I think, as finding a modular way to store proof scripts. You could store something like Coq's Ltac. Or you could take an approach that math papers usually use, of re-copying excerpts of code elsewhere and explaining the representation of those. Or if you store your program as an AST, you could directly annotate it with representation guidance. The main thing to consider is how these annotations are tied to the changing program text.

I take it as a requirement that for a given value you should be allowed to build several representations of it (with garbage collection, without garbage collection, GPU side, etc.). Also, as with type inference, you want to avoid requiring explicit annotation whenever possible.

I have more design work to do in this area, so I don't have all the answers, but I'm far enough along that I think it's a good idea. Needless to say I have no practical experience with such a system to back that up.

I'm going in the opposite direction. Types specify representation. For example, you can have an unboxed pair. On top of that you build abstractions with representation hiding like ML modules. Do you see any problem with this?

I looked at using my module system for representations initially, but didn't think it would be a good fit. The problem is that representation is often not proper logical refinement.

Take the simple example of representing natural numbers with machine words. The problem is that machine words can't hold an arbitrary natural number. Thus, in order to provide a conformant machine word implementation of Nat, you have to support bignums. And even then, you have to be using an abstract memory model, because if you're using a machine model with fixed size pointers then you can't establish that it won't run out of memory (because it will).

With a system of representations, I get to choose the relation that should hold between the value and the representation. I can try to find a representation that always provably produces the correct result under the assumptions of machine behavior, or I can choose a weaker relation, like a representation that produces the correct result as long as it doesn't encounter integer overflow or an out-of-memory condition. Or I can extract a special representation that handles the important case where such-and-such parameter fits in a single byte. etc.

I haven't thought too hard about it yet, but I have at the very end of my TODO list the idea of defining numerical functions in terms of real reals (e.g. Dedekind cuts) and then extracting a floating point approximation with the rep system. This could allow algebraic reasoning on the reals before delving into the pit of floating point despair.

And then there are cross-cutting issues like garbage collection, shader representation, etc. I don't see how you'd get very far handling those with modules.

Do you at least have a solution for high-level representations, e.g. representing a list with a rope or finger-tree?

It seems to me that almost any data type can be used as a representation for other data types, and that this is a normal way of modeling things. Thus, it's difficult to separate the two concepts of type and representation. In some senses, interfaces or typeclasses allow a little separation on the small scale... though are often not very compositional.

What does fundamentally mean to separate type from representation, if we are to apply this at both low and high levels? That we can transparently replace one set of types and subprograms with another, in a given usage context. without affecting observable behavior? That seems like a form of optimization. Perhaps we should be trying instead to modularize proof-of-correctness for optimizations.

Do you at least have a solution for high-level representations, e.g. representing a list with a rope or finger-tree?

It's the same solution. This isn't just a low level facility... it's very general: building a related value from an expression.

It seems to me that almost any data type can be used as a representation for other data types, and that this is a normal way of modeling things. Thus, it's difficult to separate the two concepts of type and representation. In some senses, interfaces or typeclasses allow a little separation on the small scale... though are often not very compositional.

I don't follow. Is this a counterpoint to something I wrote?

What does it fundamentally mean to separate type from representation, if we are to apply this at both low and high levels? That we can transparently replace one set of types and subprograms with another, in a given usage context. without affecting observable behavior? That seems like a form of optimization. Perhaps we should be trying instead to modularize proof-of-correctness for optimizations.

The system I have in mind is even more general than that, because it allows "without affecting observing behavior" to be relaxed in arbitrary ways. As in the example I gave of out-of-memory, you can represent a function with a process that either produces the correct answer or fails in some way. Or that produces the correct answer with probability 1. Or unless a hash collision is encountered. Really, this pattern of an implementation that works with caveats comes up all over the place, if you look for it.

Earlier, you wrote:

With a system of representations, I get to choose the relation that should hold between the value and the representation.

The trouble I have with this is that... values are themselves representations. This is most obvious when we have some organization of values representing another value, or when we use 'newtype' or similar. The very idea of separating value from representation seems somehow flawed... akin to separating wet from water.

But the idea of substituting representations seems reasonable. I wonder if thinking about it in those terms would help us unify representation control with other areas, like optimization control. (And, yes, 'works with caveats' can be useful for optimization control, too.)

The trouble I have with this is that... values are themselves representations. [...] The very idea of separating value from representation seems somehow flawed.

I would phrase it conversely as representations are themselves values, but yes, I didn't intend to imply that values and representations should be disjoint.

But the idea of substituting representations seems reasonable.

It's not a substitution, exactly. It's translation to a related value. Compilation in general is finding a related value: find me a string of bytes that, when interpreted by the processor, will produce the output of this function. The compilation result represents the original value under that relation. So the two related values aren't from the same domain in that case. If you choose your relation to be "is isomorphic to", then they would be and you could extract a representation like the list -> rope translation.

Math is lucky in that it can operate at a single abstract level of representation and not worry too much about "performance" (beyond beauty). Programming however suffers from this tension between concrete and abstract representations.

I've come to despise towers of abstractions & representations, but some level of layering seems inevitable. Chains of representations, one built from another, but not *on top of* another seems far preferable. Even still, this distinction between value and representation definitely persists.

What have you got in mind for explicit representation selection? I can't really think of anything much better than modular use of factories up front and explicit conversions throughout the representational pipeline.

Programming however suffers from this tension between concrete and abstract representations.

I don't think the usual approach of polluting the abstract definition with representational issues is the right one.

Chains of representations, one built from another, but not *on top of* another seems far preferable.

Can you give an example of what you mean here? How would something like this approach garbage collection?

What have you got in mind for explicit representation selection? I can't really think of anything much better than modular use of factories up front and explicit conversions throughout the representational pipeline.

I have in mind an explicit representation selection programming step, where you work with the IDE (much like you'd work with a theorem prover -- I see theorem proving and representation selection as closely related) to build representations for your abstractions, separate from the abstractions themselves.

Ubiquitous use of factories and representation parameterization adds significantly to the complexity of everything. Any equational reasoning that you had probably goes right out the window.

I don't think the usual approach of polluting the abstract definition with representational issues is the right one.

That sounds nice in theory, but in practice an abstract representation from one vantage point is a concrete representation from another.

Consider that you can represent a persistent sequence in many concrete ways: eg linked lists and array mapped tries. From the outside, you've got an abstract vector. However, that same abstract vector is now concretely how you may represent something else. For example, you may represent an abstract interval as a concrete 2-item abstract vector. Or you may represent that same abstract interval as a concrete 2-field struct.

Abstract vs concrete is a matter of perspective.

Chains of representations, one built from another, but not *on top of* another seems far preferable.

Can you give an example of what you mean here?

This is just a plea for a language and evaluator oriented worldview over the common call/return API oriented approach. If all of your representations are implicit in the evaluation process, hidden in the space between API calls, you can't ever capture a pointer to the world at any step and look at a sane representation. You can't slice out a layer of your tower of abstractions, without great mock-object pain.

How would something like this approach garbage collection?

Garbage collection frees resources when they are not reachable anywhere in your process. React.js does something similar: when components are no longer reachable from the "current frame" then they are freed. Given manual memory management operations (alloc & free), you can imagine a tree of processes where the evaluator in any given subprocess explicitly allocates & frees resources as they become reachable (or not) from the machine state for that processes' subprogram. Various interleaving of manual/automatic resource management is quite achievable in this way.

Is this the same as this?

Not sure what you think the connection is.

I'm not a believer in the Rx model at all.

I was reading posts above and responded in the wrong window on the "pipeline" heading.

.

There are a lot of similarities between GC and managing time. For one, cycles are a big problem in both, though I haven't found a good equivalent to a copying collector yet for Glitch (I use multi-phase replay to break bad feedback cycles, but it is too slow...).

Also, because "creating" an object is just another effect, they are rolled back (i.e. the object is deallocated) in glitch when they are no longer performed! This means...GC isn't strictly needed anymore in a managed time system. Events throw a wrench into this: they allow you to propagate objects along that might no longer exist, and so object access must be checked dynamically (also, god forbid if someone creates an object in an event handler!). Also, I haven't really explored the full implications of this behavior yet.

Glitch explicitly names state using token identifiers, which is quite useful since the state can then be "found" again on replay and cleaned up when no longer needed.

You can use time to unravel cycles.

Consider Functional Programming with Structured Graphs which also speaks to Matt M's point about values and representations. By deferring a value via a symbolic representation, a graph representation's pointer cycles are broken. Only when you traverse the structure do you build up a context with which you can traverse the cyclic relationships.

You can always unravel cycles by introducing an indirection and giving that indirection meaning within a dynamic extent. I'd argue that traditional pointer cycles are just that, but where the indirection is a memory address and the dynamic extent is static in the sense that it outlives your program. Once you flatten conceptual values on to memory, it's not really cyclic until you begin to interpret that data.

Time can't unravel cycles if the computation is intrinsically iterative; e.g. if you are computing connectivity over a cyclic graph, or doing iterative data flow analysis on a control flow graph with loops.

The delay approach just doesn't work at that point.

You lift a fixed point expression in to one that labels cyclic terms with time subscripts. This turns a relation in to a function, which you then evaluate over time. Algorithms interpret a cyclic reference in the context of that algorithm's state.

Even if your program never terminates, a traversal over a cyclic structure is effectively unraveling it. It's only cyclic if you perceive it as cyclic. The problem is that when we traded in our pointers for references, we lost the ability to choose whether or not to evaluate the indirection. For acyclic structures, that choice is almost never useful, but it's essential for cyclic ones.

You can only use time to unravel your cycle like that IF your program doesn't need to accommodate change incrementally. So say I want to compute connectivity for a cyclic graph that also changes over time. If we have a graph g at t_0, then we can use t_1, t_2, t_3 to iterate over that graph and compute a solution S for its connectivity. However, if the graph changes at t_4, then we can't take S at t_4 and go to t_5, since the cycles are already included in S. We have to start over again to compute S'.

Note that if changes and computations are only monotonic, then we can go from S to S' easily, but then time is not really required to break cycles.

Wouldn't it make sense to have two separate indices, one for time and one for iteration count?

Suppose we have a graph G represented as a set of edges (v,w) and start with an initial vertex set S_0 = {v} as the starting vertex to compute connectivity from. Then we can define S_(n+1) = {w for (v,w) in G for v in S_n} as the iteration of the algorithm to compute connectivity. We can incrementalize that by instead of computing a whole new set at each iteration, we only compute the difference between S_(n+1) and S_n. Lets call the representation of that difference ΔS_n = diff(S_(n+1),S_n).

Now if the graph is changing over time we have G_0, G_1, ... G_t. We can also represent that as a series of differences ΔG_t. This gives us sets S_n_t, with *two* indices: one of the iteration in the connectivity algorithm, and another for the time step. The algorithm can now be made incremental in *two* different directions. We have ΔS_n_t = diff(S_(n+1),S_n) and ΔΔS_n_t = diff(ΔS_n_(t+1),ΔS_n_t).

Ya, this is actually kind of how my existing multi-phase solution works. Here is a simple example to illustrate he problem:

if A: B = true
if B: A = true
A = true

This is the code at t-0, at t-1 retract the last assignment and evaluate so A's truthiness doesn't get trapped between the two remaining assignments. My current system will execute the code in two phases always where A's truthiness at the first statement is only visible in the first phase. Now, when the last statement is retracted, A is still not visible on the first phase, and A's assignment to true is rolled back before it could be seen in the second phase.

But this might be too expensive; I'm looking at other options, including explicit cycle detection (which would also help with paradoxes).