I don’t have much time, so here’s just a quick jot. I don’t think System IG can prove this rather obvious proposition:
|- GL(\a. Ga(Ka)) (\a x. x)
Or translated to more conventional notation: (\a x. x) : (a : Type) -> (a -> a), the type of the polymorphic identity [...]
When working the latest incarnation of my System IG compiler, I used a thingy which I now realize ought to be characterized as a design pattern. It substantially changed the way I was thinking about the code, which is what makes it interesting.
Summary: separate an algorithm into certificate constructors and a search [...]
It has been a little while since I posted anything. So here’s a general update about my work and other aspects of my life.
I’ve been passively thinking about Dana, but not doing very much significant. I have abandoned the RTS language on the grounds that it is too hard for my little mind [...]
Over the last week, I took a break from Dana and wrote a Geometry Wars-style action game. The main idea the game explores is virtuosity. Essentially there is so much to control that our puny human brains cannot comprehend it all for a long time; the game is engineered to have a very [...]
