# 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 the implementation will be under 300 lines or so (only for the bootstrap, once I get to unsafe compilation it will of course grow).

Meanwhile, I’ve been playing with the prototype implementation to get a feel for the language. It is very pleasant to work with, even without the “necessary” programmer niceties such as inference. The typechecker is partial, and it is occasionally annoying when it loops. But it is predictable, and as I gain more experience I am seeing how to avoid them, just as one avoids infinite loops when writing programs. The convenience gained by a parital typechecker more than makes up for this annoyance.

One of the things I played with is encoding sum types as product types with a church encoding. In my experiment it worked, so it’s possible that sigma types are not necessary at all. To warm up, here is a non-dependent encoding for pairs in Haskell.

```type Pair a b = forall c. (a -> b -> c) -> c

pair :: a -> b -> Pair a b
pair x y cc = cc x y

-- Here's how we destruct
unpair :: Pair a b -> (a,b)
unpair p = p (\x y -> (x,y))
```

So the encoding I used was just the dependent analog of the same thing, which I will reveal shortly. For those familiar with Agda, you will feel right at home in ΠΣ’s syntax. For those not, the trick is the notation (x : A) -> B, which is just like the type A -> B in Haskell, but first names the argument of type A, so that B may depend on it.

```Sigma : (A : Type) -> (A -> Type) -> Type.
Sigma = \A -> \P -> (C : Type) -> ((x:A) -> P x -> C) -> C.

Pair : (A : Type) -> (P : A -> Type)
-> (x : A) -> P x -> Sigma A P.
```

Look for the resemblance of the “Sigma =” line with the “type Pair a b” line above.

The encoding of Nat is straightforward (exactly the same as the encoding with ΠΣ’s built in sigma type):

```Nat : Type.
Nat = Sigma {'Z,'S} (\tag ->
Case tag of
{ 'Z -> {'Unit}
| 'S -> Nat
}).
```

And using it is almost as convenient; there are a few extra necessary type annotations.

```iterate : (A : Type) -> Nat -> (A -> A) -> (A -> A).
iterate = \A -> \n -> \f -> \x0 ->
n A (\tag -> \ns ->
Case tag of
{ 'Z -> x0
| 'S -> f (iterate A ns f x0)
}).
```

Notably, the “A” after “n” is absent when using the built-in syntax.

Meanwhile, Sigma types make a great encoding for modules. I will switch to the built-in syntax now, because it is a bit cleaner. It looks like this: (x : A ; B), which is just like the Haskell pair (A,B), except that it names the element of type A so that B may depend on it. Also, ; associates to the right, so we can make multi-field syntax.

So here is a first-class Nat module:

```NatModule : Nat : Type
; zero : Nat
; succ : Nat -> Nat
; iterate : (A : Type) -> Nat -> (A -> A) -> (A -> A)
; {'Unit}.
NatModule = Nat, zero, succ, iterate, 'Unit.
```

So the core calculus already supports first-class modules (this is true of any dependently typed language). Throw a little syntax sugar on that and I might start to prefer this to Haskell.

Which is good, because the plan is to bootstrap in Haskell and then switch to all-PiSigma, until I can build a rudimentary Haskellish interpreter that compiles down to PiSigma.

I’m doing all this work because everything has to be first-class in Dana, because there is no compilation phase. It’s all tied together in one big jumble.

# A world without orphans

An orphan instance is where you have a situation like this:

```module Foo where
class Foo a where
foo :: a

module Bar where
newtype Bar = Bar Int

module Baz where
instance Foo Bar where
foo = Bar 0
```

I.e., a class is instantiated with a type in a module where neither the class nor the type was declared. GHC issues a warning in this case, because it has to put that instance in a global table that is scanned for every compilation unit. In non-orphan cases, it knows that the instance will be in scope, because at the point of usage, both the class an the type are in scope, so the instance came with one of them.

What happens if we change that warning into an error? No orphan instances allowed!

Wonderful things, that’s what. The most notable, in my opinion, being that the very common desire for superclassing is now perfectly acceptable (modulo the many implementation concerns). For example:

```class Additive a where
(^+^) :: a -> a -> a
instance (Num a) => Additive a where
(^+^) = (+)
```

The problem used to be that, let’s say someone made a type Foo and instantiated it as Num and as Additive. Which Additive instance do we use, the one here or the one they defined? This problem vanishes if we don’t allow orphan instances, because Additive Foo and Num Foo would have to be instantiated in the same place, when Additive is in scope, and thus this superclass instance is in scope. So the collision would be caught modularly at compile time (that is, it’s not when you just happen to use these two modules together that the universe explodes, it’s precisely where the problem occurs). The module that defined Foo would be informed that he is not allowed to define an Additive instance, because one was already defined for him.

# 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 we need to kill threads with weak references and stuff). But I can’t come up with an implementation which has both. And my current theory is — I never thought I’d say this — Haskell isn’t good enough!

This language + RTS extension is still in its early stages, and I’ll have to think and prototype more to hash out the details and verify its feasibility. But since I have decided to embark on the Dana project, I am now comfortable with relying on new language features and runtime to get the job done, which previously has not been an option.

Here’s the motivating example. You have a bunch of behaviors — functions from Time to a — which are defined progressively, i.e. they use earlier results to compute later ones. In the best case, we could model these as plain functions of Time, but of course that is not practical in Haskell. In that case, it is lazy computation that never forgets. My idea is to have enough support so that it can forget.

The reason it is allowed to forget is that Time itself is also progressive; i.e. if you have a reference to a some time t, you cannot get to any earlier times. So when the last reference to a time before t disappears, all behaviors can forget everything before time t.

But that’s not a very good solution by itself (unfortunate, because it can be accomplished in Haskell with weak references). The reason is that a single naughty value that holds on to an early time will ruin it for the rest of the program — no behaviors can forget anything after that time. How do we keep the effects more local. Well, when the garbage collector does its run, instead of marking objects as “alive” or “dead”, it can mark them as “needed after t”. So you might mark an object multiple times, with decreasing times each time you see it.

And of course there is nothing special about time. The extension ought to be general enough to handle “stuff like this”. I haven’t even thought about how to make a garbage collector that does this efficiently.

Alright, enough motivation. Onto the language design. I want to add support for ‘progressive folds’, and memoize them with garbage collection. Say you have this data type:

```  data U s where
Succ :: U s -> U s
```

This looks inane, right? It is unpopulated. Or is it? We can fold a progressive function over this:

```  foldU :: (b -> b) -> b -> exists s. (U s, (U s -> b))
```

I.e. we can define functions over differences of nodes, i.e. in terms of a starting point (which is kind of what the s type variable denotes).

Also, when a particular value U s disappears, we can purge that entry from the memo table and everything that goes along with it. We also know that references inside the scope of the existential eliminator can’t escape, which will end up giving us the time-like relationships I described.

I’m still thinking about the mathematical foundations of this. I.e. what does such an “unrooted” data type mean? This fold also feels less general than it could be; is it possible to introduce two unrooted functions at the same time, or use different recursion schemes, … etc.

# 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 ideas around us. We can still communicate with the outside world by modeling them in a pure way.

Just to be clear: I will not be accepting comments about the feasibility of the idea itself (eg. don’t say “but the idea of an operating system is necessarily stateful” or any of that bull). Comments and criticisms about the approach I describe are more than welcome.

So this has been stirring away. Then at Thursday’s Boulder functional programmers group, somebody mentioned Squeak. I had seen Squeak a long time ago, and was amazed and impressed by the concept. There is no distinction between compile time and runtime, between source code and program. Everything is just objects floating around in the world. And of course this matches perfectly with the purely functional operating system idea.

It sucks to program with text. Programs are not text. Ultimately, programs are their denotation, but we need a representation. I say that representation is abstract syntax. Our program editors output abstract syntax, which the compiler turns into real objects. Text doesn’t have to enter the equation anywhere.

I don’t think this idea fits Haskell’s type system very well. We need something closer to dependent types, because types have to be objects floating around in the world too. So, while I’m at it, I think I’m going to make a pure language — pretty close to, but not exactly Haskell — which is the core abstraction language. Maybe something both expressive and barebones like PiSigma. But I’ll need a real-world language to go on top of that.

Hubris indeed.

So! What’s the large-scale plan? I am going to assume nobody will help me (other than to offer suggestions) in these early stages. This is a Grand Vision (TM), and I doubt anybody but me is going to get excited enough to contribute until it starts coming together at least a little. But I am completely excited, as this is the culmination of an idea that has been developing for years. Oh, and that was at the beginning of the large-scale plan because excitement is the top point in my book — engineering is secondary to motivation.

I don’t really know anything about drivers or hardware or any of that, and this undertaking is already way too huge for me. Therefore, I’m going to go the route of Squeak and implement an image-based sandbox — an OS inside an OS. I’ll start by choosing a core language and making a really slow proof-of-concept interactive text-based interpreter for it. At that point, many options open up, depending on what I’m inspired to do at any moment: improve the language frontend, work on graphical hooks, start work on a faster interpreter or JIT, start designing the FRP essentials, ….

As for the FRP essentials, why do I think they will be more possible in this new concept than in Haskell? Well, I have a sophisticated RTS extension that I think will handle that, which I will blog about riiiight… now! (And there are a few ways to compromise in case that idea doesn’t pan out)

Oh, btw, I’m calling this project Dana, after da man Dana Scott.

# How to shrink a git repository

I thought I would blog about this, because I’ve tried and failed in the past, and it just took a lot of tinkering to figure out. The problem is this: I have a git repository with a game in it, and a long time ago thought it would be a good idea to add the game’s music to the repository. But it turns out that was a bad decision, because it made the repository too large to easily transfer around/host on free sites/etc. So, how do I get those pesky music files out of there, and once I do, how do I convince the repository to actually shrink (this latter bit was the trickiest part).

So, first, I go into the git directory and prune out all the music:

```  % cd mygame
% git filter-branch --index-filter \
'find -name ''*.mp3'' -or -name ''*.ogg'' | xargs -d''\n'' rm -f'
```

And wait a while while it does its thing. Now we would like to run gc and get rid of all the old objects. Unfortunately, the old objects are still stored in “refs/original/”, so gc will mark them and not clean them up, and I don’t know how to delete them.

So here’s the hack. Clone the repository, which will not clone the original refs, and then gc that one.

```  % cd ..
% git clone mygame mygame2
% cd mygame2
% git gc --aggressive --prune
```

And at this point, the mygame2 repository will have forgotten all about those music files, and is much smaller.

WARNING: This will rename all the objects in the repository, so pushing and pulling from repositories which haven’t been filtered won’t work. After this process is done, everyone has to clone anew.

A less hacky way to do this would be appreciated, if anyone knows it.

# Freewrite

Here’s a freewrite. I am going to write stuff, I don’t know what, because there isn’t all that much to talk about, or at least that’s what I’ve been saying. Pause. Can’t do that. Okay keep writing.

I don’t know if I’m even going to publish this as private which my mom reads. But whatever, I don’t care. I don’t want to inhibit the flow though, so I’ll assume I won’t even if I do etc. etc.

Yeah, so there’s nothing to talk about, right? Nothing at all. Scanning, scanning, looking for something to write about that isn’t about Karen because there’s nothing to talk about, right?

Okay, enough of this bullshit. I’m actually relatively happy with the whole Karen situation, I don’t really know why I’m so avoidant(?) about it. Pause. Pause pause. Keep going. I chatted with her last night on google talk until about 3am. We had a nice personal talk, and actually talked about each other a fair amount, instead of just the external business, er, not business, that wasn’t a good word, external stuff like music and whatnot. Pause.

She’s really sweet sometimes. She said she was in a foul mood because of visiting Ithaca and her “drama-free” friends. When I further inquired, I was on her list of drama-causes. I guess that makes sense. I don’t know why or how I was hoping not to be. Anyway. She seems to have come to terms with it and says she is going to just enjoy her self for her remaining 5 months.

5 months. Man, that’s not very long, and she seems pretty certain about returning to Ithaca. Well fine. Whatever, I’ll just not worry about it and enjoy myself for the remaining 5 months also.

Am I allowed to backspace when I make a typo? I have been. Let’s try it wouthout that for a little while.

I’m wrtorried that I gave the wrong message to pause what’s his name um Will. I acted unseasy about his guitarist roommate when he said he was going to play with us., I’ve been wantint to write an email or something saying thats just a weid thing I have and it’s actually fine. Which it might be. I figure it might be nice to have a third tonal instrument for the kinds of things I want to go. Id guess that I just am afraid he will reject my ideas, since I am doing some rather weird stuff, ro rather wanting to do some rather weird stuff.

Pause. Ack this is hard to geek oing untouinteruppetd espectially not correctying tyopos. If you look closely you can see that most of tee letters in the type of are form words a coule words ahead. Means I my mind is ahead of my fingers maybe, maybe it hsouhg nt’ be, *laugh* that was a good one. Maybe I should just concentratie on writing exactly what my fingers on typeing noint on the next word. Lol this is great.

What else what ealse. What fi I dont’ write about my life? Tharjo this freewrite thing is hard beause my keyboard kind of sucks because I spilled coke on it the other day. Sticky, the shift key is quitty unresponsive andsuch. I guess
A
Ack I hace a headache! I’ve had one all day. WHatever all day means. I selpt for many many hours. Um. I got up at 7:30pm. I forget when I went to bed, but it was not after 7:30 am. So, great 12 hours. I’m sleeping a lot. I don’t know why. I thnk one of the reasons is because it’s cold in the house.

Pause. Oh eah not write about my life. What else is there in my life but my life though There are pretty carpte and things outside like I’m closing my eyes and typing now. To force myself not to correct myself and hopefully immerse myself a bit more. So things outside, like the moon and grass and a great glow. New moon right now. New moon = no moon, hm, what does that say about new ideas? Do I have anynew ideas? Should I stop being introspective for once. I probably didn’t type introspective correctly there, did I?

Programming is something. I keep saying ot myself “x times y inberse” and crap like that. I t has no context, it’s just blind mathematical formulae. I have no idea what why I do that. Hmm.

This is near, writing with my eleyes closed., I am now picturing a beatch, though I wasn’t when I started typing “I’m now picturing”. At that point, or maybe it’s now, I can’t tell, what is time, it’s fleeting after all isn’t it. What do I care what I though then or will think later. How can I trust that those things actually happene, all I know is what I am thinking now. And I only think I know what I was thinking or will be thinking, espectilally was thinking, as that is the great illusion.

And right now, I don’t care about Karen do i? I have only mainly been thinking about her for the last, um, 8 moinths? Wow. But she’s not around right now, so what does it matter. I can just be free, and why do I worry about feeling emotions or not feeling emotions. Why can do I have to label my emotions such, can’t I just be free and be? Emotions are low-level detiails that miss the big picture.

Am I sounding like namaste yet?

Monad. I don’t know why I was inclined to write that word. Neat though. What I want to type Monday, I type Monad. I think that probablly means I’ve been doing too much programming.

Okay, I’m done. here. Eyes open.

Hey that was fun. And I didn’t make any “progress” or anything. Why should I have to? It’s just a little piano improvisation without the piano.

For quite a while, a package called MonadRandom by Cale Gibbard has been available on Hackage. At first it seems like just a little silly convenience module. But I argue that it should be used instead of System.Random whenever possible, not just when it’s more convenient. Here’s why:

What’s a RandomGen?

```    class RandomGen g where
next :: g -> (Int, g)
split :: g -> (g,g)
genRange :: g -> (Int,Int)
```

It’s this thing… this thingamajigger, if you prefer, which has a next, a split, and a genRange. Cool, that’s great. Um… so, what are those things? What do they mean? And what do they have to do with randomness? next. NEXT? That doesn’t seem very random!

MonadRandom is very humble in its self-description:

Computation type: Computations which consume random values.

Binding strategy: The computation proceeds in the same fashion as the identity monad, but it carries a random number generator that may be queried to generate random values.

But it means much more than it says. Rand a is not merely an “identity monad carrying a random number generator” (a random number generator being one of those what-the-heck-is-thats above). Rand a is a probability distribution of a’s! Which is simple, meaningful and easy to reason about!

We can model it like so:

```    Rand a = a -> Real
fmap f p x = ∑ p[f-1[{x}]]
return x = δ(x)
(p >>= f) x = ∑y p(y) f(y)(x)
```

With getRandom etc. being standard distributions on various data types.

As long as your computations are in Rand (I don’t give a hoot about RandT), you can use this semantics for precise, mathematical reasoning. What did you have when you were using RandomGen?

# Ha! I can’t even get Events right

No wonder FRP has been so difficult. In going back to basics, forgetting about behaviors and just doing Events, I realize that my belief that Events are “the easy part” has been flawed. Neither of the semantics I’ve had in mind are both implementable and appropriate. Or rather, they both are, but neither of them can do as much as I thought they could.

I will leave my previously preferred semantics of Event a = Waiter a = Time -> (Time,a), for annoying practical reasons (it also violates intuition about what an event is).

The reactive semantics of Event, Event a = [(Time,a)], is no good because there is always a least occurrence. This violates relativity and intuition (relativity being an intuitive concept I’ve developed regarding the lack of a “global start time”).

So I’m left with Event a = Set (Time, a), or Set (Time, Set a) to handle multiple occurrences at the same time. I am actually inclined to resort to the former, and require a Monoid instance on a to merge. Anyway: what’s the problem with this one? No temporal operations are allowed on it, because it must be observant. Consider mouseClick :: Event Point, the event of mouse clicks. There may be many mouse clicks before the program started, before we were listening for them. If we then sequence mouseClick with some other event, then we have to know about those earlier mouse clicks to detect it. Also consider everySecond :: Time -> Event (), which occurs every second before and after the given time. There are infinitely many occurrences of this event, and so there are infinitely many simultaneous occurrences of everySecond t >> everySecond t. We can not possibly handle all of them.

I know I didn’t motivate that very well, but hopefully you get the idea. If an Event is a set of occurrences, then we must be able to see all of them, including ones that depend on events that happened when we weren’t watching.

I conclude that Event is not a Monad or even Applicative, and all we have is the following interface:

```    data Event a
instance Functor Event
instance (Monoid a) => Monoid (Event a)
filter :: (a -> Bool) -> Event a -> Event a
withTime :: Event a -> Event (Time,a)
```

Actually, as far as primitives go, I prefer this to filter:

```    partition :: Event (Either a b) -> (Event a, Event b)
```

But they are definable in terms of each other, so it really doesn’t matter except for efficiency concerns. Look how partition is dual to zip. Isn’t that cool?

But in exchange for meaning and implementability, we have given up much of Event’s usefulness. Note that we can no longer even construct the event of double clicks. That makes sense to me, though, because what if the first of the two occurred before we were watching?

I can think of a bunch of ways to get back bits and pieces of the usefulness — EventParsers and the like — and I’m still experimenting with which will be the most effective.

# Ridding ourselves of IO before there is a good replacement

I have been researching FRP for about a year now without finding or discovering an implementation I like. I don’t know if there is one — maybe my standards are just too high. However, it has initiated me into the more general interest of purely functional foundations.

Since I am tired of thinking and want to start hacking again, I am abandoning FRP proper for the time being. But I am continuing in spirit, by continuing with foundations. I will be developing this project in the Frag repository, where I keep my FRP stuff.

The idea of the Frag project is simple: get back to making the software I want to make — mostly games — but shun IO. I.e. the content of these will only be built on semantically meaningful abstractions (which are in turn implemented on IO, of course), but without concern for making it a “perfect” FRP implementation. Said abstractions will go in the Frag project. The main point is to get away from the world of fuzzy, complex operational semantics, replacing it lazily with simple denotational ones.

But this is a foundational project, meaning that once the foundations are replaced, I allow myself to do arbitrary software engineering on top of it. I think this is an important point.

Currently in the repository is a simple Event abstraction. I’m seeing how much I can write with just that, without worrying about modeling conceptually continuous things (like mouse position). Secretly my plan is to accidentally come across a good interaction model which boils down to Event, and is thus inherently meaningful (simplicity can be refined out later).

I’m having trouble foreseeing how I will model eg. network interaction using Events. Graphical games are pretty easy, since conceptually they always exist, and you’re just choosing to view them. I can’t see how network fits into a model like this, since a network program can have side-effects on another computer. Can anyone think of a way that network interactions are about being instead of doing?