RTS Research

Over the past week, I have been again exploring low-level functional systems, in which to write an RTS (notably a garbage collector) for high-level languages. The progress has been slim, but I’ll report on my findings.
I get the hunch that linear lambda calculus is unsuitable, but I haven’t yet convinced myself of that and [...]

Dependent types are ridiculously easy

After an inquiry about a combinatory calculus for dependent types, somebody in #haskell — unfortunately I don’t remember who — recommended I look at Illative Combinatory Logic. After studying the paper a bit, all I can say is Wow! It implements a (conjecturally) complete logical system in but three simple typing rules, together [...]

Dana update: Core execution language, dependent combinators

It’s been a little while since I gave an update about Dana, so here it is.
There has been very little code progress in the last week. Instead, because of the self-embedding issues I talked about last time, I have been exploring the use of a combinator calculus as an intermediate stage for typechecking. [...]

Dana needs a self-embedding of U-Box

My first major goal in Dana is to write a console session interpreter, in which you can construct, name, compose, and observe Dana objects in the console. Since this is a foundational project, I best say what it is I mean by “console session”:

newtype ConsoleSession = ConsoleSession (String -> (String, [...]

Dana update: System U-Box compiler is go

Over the past couple days, I have been working on a compiler for something between System U and ΠΣ, as experimentation for Dana’s core language. Here is the repo. I have just finished (I think — seems to work pretty well) the typechecker and it correctly typechecks all the programs I can think of. [...]

Fun wth ΠΣ

I have somewhat irrationally chosen ΠΣ as the core language for Dana. I’ve been struggling to create a small, beautiful implementation. But I am getting closer and closer — it’s just about finding the right combination of representations so they fit together nicely — and my hope is that when I am finished [...]

Existential Memoization

FRP has this essential trade-off of computation vs. garbage collection. I can come up with implementations which are lazy in their computation, but never forget anything; and I can come up with implementations which forget but are too eager in their implementation (in which garbage collection has too much effect on runtime performance, because [...]

The Third Virtue

Ever since working with the Anygma team, the idea of a purely functional operating system has been stirring in my head: An operating system that stays denotational and composable all the way down to the device drivers. In this world, we have to make no sacrifices like IO to interface with the impure [...]