I think you meant “there is one function Void -> a” (rather than none), ignoring bottoms, namely the empty function.

instance HasTrie Void where data Void :->: a = VoidTrie trie _ = VoidTrie untrie VoidTrie = absurd enumerate VoidTrie = []

That is, there are no functions Void -> a, and a^Void is isomorphic to Unit. However, this instance makes constant functions strict, so that memo (const a) undefined == undefined. This can be alleviated with an instance closer to the Unit instance.

Any thoughts? Would you be willing to add a Void instance to MemoTrie?

I wonder if it is possible (or makes sense even) to apply the Banach fixed-point theorem to the continuous time model.

Consider that IO includes exception-handling

IO also includes concurrency, which is even more troublesome.

You start out by saying that all function futures should be created from simple futures, but of course caching futures violate that principle – at least if they themselves are not created from simple futures. And, at some point, you want to hook up actual external-world actions to get some of that reactivity the “R” in FRP is about, and caching futures are an entry obvious entry point.

Here’s the problem: Caching futures themselves are well-behaved, but caching futures combined with mappend are not: Consider two caching futures f1 and f2, and only f1 gets triggered at time t0. Mappend them to get future f. If you ask the (try-future version of) f at time t' > t0, you get Some answer. If you ask at MaxBound (which is greater than t'), you get no answer, because the system waits for f2. So monotonicity is violated. That, of course, is also the issue with my version of fToS.

The deeper problem, I think, is the fact that the event occurrences the system talks about really refer to the programmatic event (i.e. the SampleVar being filled), rather than knowledge about an external event, which only becomes available after it has actually happened. (How do you mappend two futures knowing that they’ll become known only after the timestamps that will be attached to them?)

All solutions I’ve come up with for this require going back to some notion of partial time. It can be pushed into a smaller corner than before, but it’s still there.

Since down yields an f-collection of locations, we do not need sibling navigation functions (left & right).

For instance, if f = [], then down yields a list of child zippers, which you can traverse as you like.

Conal, nice observation about Landin. I have to say “denotative” is an appealing term.

fToS f = p (unFuture f maxBound)
  where
   p Nothing -> (maxBound, undefined)
   p (Some sf) -> sf

?

Sure, you might have to wait, but that’s true in general of F.FutureG, no?

for example:

pure id <*> x /= x

You can fix this by ‘cloning’ the leaf elements though:

L2 f <*> B2 (xs :# ys) = B2 (f xs :# f ys)

B2 (fs :# gs) <*> L2 x = B2 (($x) fs :# ($x) gs)

I think a similar trick works for T4.