Lambda the Ultimate

Fixed.

LTL may be weird, but it is quite a popular modal logic. It is interpreted classically (hence the pointwise implication, as implication in LTL is defined as a De Morgan dual of conjunction). There's a design choice in how to interpret LTL constructively: do you change LTL (to include Kripke monotonicity) or keep LTL as close to its classical interpretation as possible. I went for the latter, since I thought that best highlighted the relationship between LTL and FRP.

The pointwise construction allows the native function space to be used when defining implications, and gives implication as the right adjoint of conjunction (pointwise pairing), so currying and uncurrying work as a niave programmer (er inasmuch as there is one using Agda) would expect. This doesn't matter so much for the arrowized implementation in the paper, but does make a difference to the unarrowized version compiling to JavaScript.

The pointwise semantics means there are nonmonotone type constructors, but that is mitigated by Agda, since type recursion goes via datatypes, which enforce strict positivity. It would be nice to also allow FRP constructs (in particular looping) at the type level as well as at the data level, since this would allow the solution of guarded fixed points of type equations, but I left that as future work.

This is off-topic of the main thread, but I recently witnessed a presentation of work done in Agda where the 'code' I saw was an unbelievable hack - not Agda's fault in any way, fully the programmer's "fault".

The main problem was that a lot of the results shown were (obviously) true in a very abstract setting, but the actual code/proofs consistently made use of 'accidental' features of the chosen encoding/representation. And thus even though the ideas presented easily admitted generalizations, the code presented did not.

I had been, up until that point, convinced that Agda, by its very nature, would have prevented this kind of hacking. Much to my regret, I was (constructively!) shown to be quite wrong.

On the other hand, up to now, the code bandied around on the Agda mailing list has been quite hack-free (although not necessarily unicorn-free).

One thing I always try to emphasize when I teach dependently typed programming is that there can be very large pragmatic differences between logically equivalent definitions. If you make a logically correct but unpragmatic definition of the problem, the resulting solution can indeed be a bloodbath, not to mention a code maintenance nightmare. However, it may be the case that a more pragmatic definition exists, and it's good to seek that definition. (I've recently bludgeoned my way through a horrible construction that I wasn't able to do before at all, and which I'd still like to be able to do a lot better.)

Intensional type theories are, by construction, reliant on their partial evaluation behaviour to deliver definitional-equality-up-to-computation. As a result, typechecking becomes quite sensitive to operational details; controlling strictness, in particular, becomes important. The stricter the functions you use in your types, the more detailed a case analysis you need to get them to compute. (Note for enthusiasts: Agda's hardwired pattern matching sometimes makes it difficult to control strictness and some ugliness may result; Epigram 1's more explicit construction of a case analysis tree at least helped with that problem.)

There are lots of other issues: first-order representations of things often allow more reflective proof methods, but higher-order representations are often more clearly compositional; indexing by just enough information lets you arrange the coincidences you need, but index by too much and you introduce distinctions between the type you've got and the type you want.

There is a danger of "chocolate box" syndrome, just as in many other situations: the beautifully confected programs go in the presentation pack; the rejects get eaten by the staff until they feel a little ill. Often a good solution arrives only when we've learned our lession: as writers, we must then teach the lesson and not just show off the solution. I cannot claim to be without sin in this respect, hence I cast no stones at individuals.

This much I know: to be good at dependently typed functional programming, you need to acquire skills that you don't automatically have by being good at functional programming. One should not approach with a sense of entitlement. We have some delightful, exotic, powerful new ingredients, and the recipe book is growing, but still a bit on the thin side: culinary calamities remain quite likely. So let's do science! (Of course, you may want to spend your available adventure tokens elsewhere; I quite understand.)

I am sure you are quite right that choosing good definitions is just as important in the context of dependently type programming as in other contexts. One of my own papers (on piecewise-defined functions) needed a 7 year gestation period before I was able to find the 'right' definitions. Once that was done, all the rest was easy.

I am also not surprised that strictness is an issue - binding time is a huge issue in partial evaluation (strictness by another name), and the more I learn about dependently typed programming, the more similarities I find between that and typed PE. And that is not really surprising either, at least if one buys into the Abstract Interpretation view of types (which I do).

I am still on the lookout for a typed meta-programming language (now that metaocaml seems to really be on the decline, after one attempt at revival). I have been almost convinced to try Idris for that purpose. If dependently typed programming is to be compared to French cuisine, then typed meta-programming may well be Italian; from the perspective of Indian cooking (say), they may well look indistinguishable!

In the meantime, I'm happy taking a page out of Alan Kay's book, and I am still trying to encode 1-algebra (and some more) in about 400 lines of code. Which is still too long, but I have to learn just a tad more category theory before I can shorten that.

To emphasize, mathematicians have hacky proofs too, and that is essentially all that is happening, albeit with a much crueler task master. And it is indeed a problem in mathematics to expose how an elegant proof gets made and not just show off the end result as if it was arrived at ab initio.

I think sticking with LTL-as-is made your results very striking, so that was a good decision.

However, I don't understand what you mean about implications. The Kripke implication is adjoint to pointwise pairing. (ie, (A × B → C) ≃ (A → B → C)). If you take time to be ω, then the category of presheaves over it form a topos (c.f., Birkedal et al's Step-indexing in the topos of trees). Then there's an internal delay operator which lets you interpret guarded recursive definitions at the set level.

Furthermore, the categories of metric spaces we've used in our semantics embed into this topos, so this category is probably a good place to compare your style of semantics with the models we've looked at.

I'm afraid I don't follow the argument re adjunctions. Define:

Even(t) = if t is even then 1 else 0
Odd(t) = if t is even then 0 else 1
False(t) = 0
(A => B)(t) = forall s <= t . A(s) -> B(s)
(A & B)(t) = A(t) x B(t)

(that is, => is Kripke implication/function space and & is pointwise conjunction/product). Then ((Even & Odd) => False) is inhabited, but (Even => (Odd => False)) is uninhabited.

Am I missing something here?

..don't both Even and Odd fail to be semantic types?

That is, in the presheaf semantics, a type is a functor F from ω^op to Set. So if x ≤ y, then we must supply restriction maps F(x ≤ y) : F(y) → F(x). With Even, then this says that we have to produce a map Even(4) → Even(3), since 3 ≤ 4. However, the definition you give for Even means we need a map 1 → 0, which obviously doesn't exist in Set. (And similarly for Odd.) Your definition can be seen as a presheaf semantics where Nat is viewed as a discrete category. I'm interested in the differences between these two semantic categories.

Anyway, I was trying to only quote familiar facts about presheaf categories: products and coproducts are pointwise, and exponentials are Kripke-style. If I was sounded like I meant something deeper, I apologize!

I see what you mean now, you're in the presheaf category indexed by Time as a partial order, not the discretely indexed category.

I think the design choice of how to index types over time is whether you consider knowledge to be monotonically increasing or not. In LTL, time order is not considered to be an information order, whereas in Kripke semantics, the order on worlds is an information order.

In FRP the types are usually non-temporal, so it's not obvious what should happen in the temporal case. I'd argue that the concern with time leaks implies that knowledge does not have to monotonically increase with time (that is, you are allowed to gc old state) and so the LTL model (and hence discrete indexing of types) is a good fit.

There's also a pragmatic reason why I chose the discrete category, which is that it allows the raw Agda function space to be used (at both the type level and the program level). In your work with Nick, you were happy introducing a DSL for FRP programs, whereas (at least for the JS work) I didn't want a DSL layer.

That's a good way of putting it! Nick and I were definitely thinking of time as imposing a kind of information order, in order to model causality: values at time t should only be computed from information available at time ≤ t. You can recover that with your box modality, I think.

However, your mention of gc makes me realize something I find a little surprising about your semantics -- how do you say that a value *doesn't* change over time?

Recursive definitions in FRP rely on feedback -- the output at time t becomes the input at time t+1. So we have to know how to make values at time t available at time t+1. For efficiency reasons, we often want the forwarding operation ought to be a no-op. For example, the data representing an int today will represent the same int tomorrow. But on the other hand, the data structure representing a stream might represent its tail tomorrow (e.g., a stream backed by a socket), and so making it available tomorrow can require explicit buffering. With the semantics you give, I can see how to define values which have the same type across time: [int] = λt. int. However, how do you define a type of ints which don't vary across time? With the presheaf semantics, you would say that [int] = λt. int, and also that [x ≤ y] = λn. n.

Given a property P : A -> Set, you can always use <exists P> as the type of behaviours whose values satisfy P. In particular, setting P to (_==_ x) gives you the type of signals that are always x.

But that's probably not what you're after in general, which is a form of self-dependency, where the type of a signal at time t can depend on the value of the signal at time strictly less than t. This would allow (for example) a type of non-decreasing integer-valued signals. Moreover, it would be nice if this kind of self-dependency could be expressed in the language of FRP, as a form of dependent loop combinator.

Such types would have a lot of the flavour of typestates, or session types, in that they allow types to encode an automaton. In the streaming I/O world, I did some work with Julian Rathke (The Lax Braided Structure of Streaming I/O, CSL 2011), and I wonder if there's a similar story for FRP?

...I don't know the full answer to your question, but I do know a partial answer. In the kinds of models I've looked at, all arbitrary guarded recursive types are well-defined. That is, there's a type constructor for delay •A. and all recursive types μα. A[α] are well-defined, when each occurence of α is guarded by a delay constructor. Nakano's 2000 LICS paper A Modality for Recursion explores this idea in detail for non-dependent languages, and the topos of trees paper I mentoned earlier extends this to a full system of dependent types.

However, if you think of a reactive system as a process or something changing over time, then streams (μα. A × •α) make sense, but an infinite tree type like μα. A × •α × •α makes less sense, since the system doubles in size at each step. It seems like there should be a linearity condition on occurences of α in addition to the guardedness constraint.

Thanks for the link to your paper! You might be interested in some new work Nick and I did with Jan Hoffmann, Higher-Order Functional Reactive Programming in Bounded Space (POPL '12), which adds space-bounedess to our earlier work. This induces linear structure along the lines of Martin Hofmann's work, which seems at least superficially different to the dataflow network style that approaches based on traced monoidal categories suggest.

Will you be around for POPL? I'd love to talk in person.

Thanks for the link to the paper. Interesting that you're looking at bounded space. The most surprising result in our CSL paper is that dataflow networks that are embedded in the plane can be implemented in online O(1) space. We only did the first-order case though.

I'll be at PoPL, are you attending the PLPV workshop?

I wonder if this (with apologies to the hard of Agda) is something like what you mean.

Firstly, let me fix notation for lazy codata (I can't handle the unicode):

    postulate
      Lazy : forall {a} (A : Set a) → Set a
      thunk : forall {a} {A : Set a} → A → Lazy A
      force : forall {a} {A : Set a} → Lazy A → A

    {-# BUILTIN INFINITY Lazy  #-}
    {-# BUILTIN SHARP    thunk #-}
    {-# BUILTIN FLAT     force  #-}

Now define coinductive right-nested infinite dependent record types.

    data TYPE : Set1 where
      _&_ : (S : Set)(T : S -> Lazy TYPE) -> TYPE

Each such type splits into some data for delivery 'now' and the rest 'sometime later'.

    Now : TYPE -> Set
    Now (S & T) = S

    Anon : (T : TYPE) -> Now T -> TYPE
    Anon (S & T) s = force (T s)

The data are coinductive right-nested infinite dependent records.

    data [_] (T : TYPE) : Set where
      _,_ : (s : Now T)(t : Lazy [ Anon T s ]) -> [ T ]

Does that fit the bill? There's a whiff of session types to it. There's also a mixed coinductive-inductive variant, where "Night" happens infinitely often, but you can alternate finitely many Σs and Πs before each "Night".

I claim (and I've checked this claim) that it is possible to (a) close TYPE under a notion of function space (S >> T) ensuring that output depends only on input-so-far, (b) close TYPE under a unit delay operator (Tomorrow T) that inserts a field of unit type at the start of a record, bumping everything else one step into the future, and (c) construct a Loeb-style fixpoint operator of TYPE ((Tomorrow T >> T) >> T).

That gives me some sort of story about productive corecursion. I wonder how it fits with these exciting LTL and FRP developments.

That's pretty much the construction we used in the CSL paper, and it works nicely for discrete models such as streaming I/O, but I'm not sure its a good fit for FRP where time is often considered to be dense.

Even in the discrete case, the unit of time is often much smaller than the delay between state transitions (e.g. in the JS implementation, it's 1ms, but you could perfectly well set it to be one clock cycle on your CPU). So with my pragmatists hat on, I'd be a bit worried that the type system would end up busy-waiting and swamping the CPU.

I've been kicking these structures around for a while, now, but with a different motivation, unless I'm failing to read between the lines. I'm not very happy with the rather syntactic (constructor-guardedness) characterization of productivity which Agda and Coq inflict on us. It's not a very compositional mode of programming. You can't even have nats = cons 0 (map suc nats), for example, and for the good reason that the type of map doesn't state the one-in-one-out producer-consumer contract which make that definition productive. Indeed, there are extensionally equal implementations of map which aren't one-in-one-out and thus bust that construction.

So instead, I'm looking for a way to model causality and producer-consumer contracts in types, with a view to a direct implementation, i.e., one where the Loeb-style fixpoint is really a lazy fixpoint, and it's the way to make corecursive definitions. The time-sliced coinductive records give me a model; Bob Atkey also has a step-indexed model. But I'm not trying to identify a "time" step with a fixed multiple of a clock cycle, just to keep things causal.

But if the same structures are showing up, that's interesting.

Ah, that's interesting, and goes beyond what we did in the CSL paper. One of the annoying deficiencies of that paper (and indeed the FRP paper too) is that the function space from A to B has no way to give dependencies between the input and the output (e.g. number of tokens in == number of tokens out).

One of the things I have on my to-do list is to work out a better relationship with games models (a la Abramsky/Hyland/Ong), which allow these kinds of dependencies. The reason why it's a bit tricky is that I'd like to drop the requirement for alternating player/opponent moves, but this gets into hot water pretty quickly, since it means that in a compositon (P >> Q) there's the possibility of infinite chatter between P and Q with no external interaction. So I backburnered that.

A related topic is that it would be nice to do an Int-construction and build a compact closed category out of the traced monoidal structure of FRP, but that's problematic because the trace is only partial, so the Int-construction produces a paracategory (Malherbe, Scott and Selinger) which I'm not sure I want to play with.

...the work of Peter Hancock and Pierre Hyvernat, Programming Interfaces and Basic Topology? It's been a while since I've looked at it, but they considered client-server interfaces where the alternation is not one-to-one, but one-to-finite. Given the people involved, there must be some game-ish ideas involved, but that's not something I know much about.

Conor must know more about this, too, since Peter Hancock is at Strathclyde.

I'd read Representations of Stream Processors Using Nested Fixed Points, which influenced the design of the process (or transducer, or strategy, or resumption, or iteratee, or...) language. I'd not read this paper.

The Loeb-style fixed point can also be thought of as the type of Banach's unique fixed point theorem. Operationally, this thing is most definitely a lazy fixed point, but it's of a different species than Haskell-style lazy fixed points.

Haskell-style laziness has a Kripke or rely-guarantee flavor to it: a thunk may be forced by anyone, and then it's a value for everyone. There's no time that a thunk must be forced, and you have no guarantees that a thunk you have a reference to won't be forced by someone else. Delay modalities, on the other hand, rely on the existence of a global clock. If you have a thunk scheduled for execution tomorrow, then you know that no one will look at it until tomorrow. This is the property that makes type-based productivity checking work.

However, simple delay-based streams are not actually the coinductive streams we first thought of. Banach's fixed point theorem asserts the existence of unique fixed points, and the Knaster-Tarski theorem asserts the existence of greatest fixed points. Concretely, given the simple formulation of streams as Stream a = μα. A × •α, you can easily see that this is not the same as coinductive streams, since you can't split a these streams into the even elements and the odd elements without a change of type. (The synchronous dataflow people call these clock types.)

If I undersand what Bob is doing (I might not be), he's following Martin Escardo in using steps to construct a metric nontermination monad, as T(A) = μα. A + •α, and then encoding recursive streams in terms of this, which breaks the one-element-per-tick requirement, and then using a logical relation to rule out nonterminating programs (whence the ordinal indexes in his types).

This is sufficiently sophisticated that I don't know that I can truly believe that these things are really coinductive streams until he proves the bisimulation property for them.

Indeed, the Loeb-style fixpoint is Banach's, here working over these heterogeneous dependent records, rather than streams.

I'm completely happy to consider a trickle (Trickle a = a * Tomorrow (Trickle a)) different from a stream (Stream a = a * Stream a). A stream lets me grab finitely many elements today; a trickle does not.

I'm also quite keen to unhook the global clock. Clock is a subclass of Applicative also supporting the fixpoint operator. So now let's take Trickle c a = a * c (Trickle c a). I think there ought to be a kind of limit construction: some sort of

whizz :: (forall c. Clock c => Trickle c a) -> Stream a

It's clear that you can't take limits willy nilly (or you could whizz the Loeb/Banach fixpoint and get the Y-combinator), but it looks like you can whizz things where the clock occurs strictly positively and where you don't have infinitely many of them in the way of your data.

We're in a new world now. Types shouldn't be invented globally and separately, with the programs that relate them amounting to the discovery of an astonishing coincidence. Rather, relatively to a given coinductive type, we should be able to construct something which is checkably a valid clocking-up of it: the witness of that validity is the whizz operator. We then acquire a method of productive coprogramming in general which allows us to choose, locally, any synchronous account of the process which happens to account for the causality of its dataflow.

If I've learned two things as a dependently typed programmer, they're that fancy types can provide the discipline you need and that fancy types can provide the discipline you don't need. As soon as you have a computational language of datatype definition, rather than a rigid language of datatype declaration, a candidate resolution becomes possible: support the local fancification of types.

whizz :: (forall c. Clock c => Trickle c a) -> Stream a

Rather, relatively to a given coinductive type, we should be able to construct something which is checkably a valid clocking-up of it: the witness of that validity is the whizz operator. We then acquire a method of productive coprogramming in general which allows us to choose, locally, any synchronous account of the process which happens to account for the causality of its dataflow.

That's a very pretty idea!

I have mostly been thinking about clocked types as a useful thing in and of themselves, rather than using them as a means to talk about coinductive types. And they do seem to want to live in their own universe -- the implementation techniques for them do seem to differ from the usual implementations of ML or Haskell.

BTW, they are both special cases of a more general fixed point theorem. Just a useful tool to have in one's shed.

It is indeed funny.

Is there an established name for what Wolfgang calls "¤-◊-LTL"? Is it S4.3?

Classical □–◇-LTL seems to be S4.3 indeed. Thanks for pointing this out. I don’t know whether there is an intuitionistic variant of S4.3.

By the way, is there a variant of S4.3 where □ and ◇ only refer to the future, not to the present? There is K_l, but this also includes modalities for the past, which I don’t want.

D4.3 might be too weak, but it shouldn't have any unwanted consequences.

Do you have any pointers to information about D4.3? Unfortunately, I cannot find anything useful at the moment.

The classical axioms are what you should expect: add the 0.3 axiom to D4.

These are well-behaved axioms, so classically the models are for frames that are serial (every node has a child), transitive, and without right-branching. I don't know of the logic being studied much, but K4.3 is discussed quite a bit in the literature. I don't know of any treatment at all of the K/D/S4.3 logics under an intuitionistic axiomatisation.