My brand new Acer laptop’s video card died a few days ago. The computer still worked, I just couldn’t see anything. So, while it’s being fixed, I’m back to using my old piece of junk which refuses AC power while turned on. It has an old battery, so I’m limited to about an hour of usage before it forces me to take a break. Needless to say, this is not enough time to get any significant coding done.

Coq is totally awesome! I proved Rice’s theorem for the SK calculus, which was a bit more satisfying than proving that every natural is either even or odd. My proof is pretty ugly, I can see a lot of ways I could clean it up, but I forgive myself; I’m a noob.

Coq is making me very excited for dependent types. For example, toward the end of the aforementioned proof, I started to define some combinators so I could construct the “impossible program”:

Definition compose := S (K S) K. Lemma compose_really_does : forall f g x, compose f g x = f (g x). (* ... *) Qed.

I can envisage doing this kind of thing *all the time* in my regular programming practice. Write a little function, then prove that it does what I want it to. I’ve already begun exploring ways to use Coq for my every-day programming tasks, such as clean ways to hook into Haskell libraries with Extraction. Who knows how fruitful this endeavor will end up.

I have been making some interesting findings on the FRP front. Here’s an executive summary of each; I may or may not go into more detail in future posts.

(1) The semantics of behaviors are “functions of time”, but what the hell is time? In the real world, time has more structure than numbers. So I claim that in FRP what we’re actually constructing is *causal transformations* of time functions. A transformation R is causal if R(f)_{t} = R(f_{t})_{t} for all f, t, where the t subscript means “restricted to times before t”. As yet this has not led to any new implementation insights.

(2) FRP would be simple, easy to work with, and expressive even without its Event type, if only there were an efficient Monad instance for Behavior. For most of the cases where we would use Event, we substitute Behavior :. Future.

(3) Behavior has an efficient Monad instance, but it is not implementable in Haskell as it stands. It requires some support for linear types. Behavior itself is not linear per se, but each separate lexical instance is always accessed in a monotone pattern. So if multiple references were indicated by the compiler with `split :: Behavior a -> (Behavior a, Behavior a)`, then you could destructively update each reference to the latest time it was accessed and avoid the expensive “fast-forwarding” necessary for the naive Monad instance. There are some other tricks, but that is the main idea.

(4) (What I’m currently exploring) It may be possible to get this efficiency without linear types by embedding the linearity in a monad, getting the “Behavior Monad Monad”. Ironically, the best candidate for doing this so far is the “Behavior :. Behavior Monad” (semantically). Whether or not it ends up working, I don’t think it will be very easy to work with.

I’ve already begun exploring ways to use Coq for my every-day programming tasks, such as clean ways to hook into Haskell libraries with Extraction.

Have you looked into ynot?

Could you please explain what you mean by hooking Haskell libraries “with Extraction”?

Very short and clear proof, thanks for posting this! I’m just confused about one detail though, the predicates complete and nontrivial take as inputs any program, but should they not instead only take

representationsof programs? (i.e. restricting the domain T to something like church encodings of an AST).dave: I had seen that before, but when I last looked I think the project was less mature, or something else happened that caused me to lose interest. In any case, thanks for the refreshment, it’s very interesting. I’m exploring a different avenue right now, but really more as an exercise: namely, encoding domain theory into Coq so it is possible to reason about general recursive functions the way we do eg. on haskell-cafe, talking directly about the domains. Hopefully I’ll find a way to extract that encoding back into Haskell, though I suspect that will be the hard part.

dreams: nothing significant. I just mean using Coq’s Extraction mechanism to generate code which calls out to Haskell libraries.

v: Great question! I’ll get back to you on that when I have more time to write. Short answer: I don’t know, but I have some ideas…