My monthly cellphone bill averages less than $10 per month. I have a smartphone. I have data, texting, and voice, and I use them. Let me tell you how I achieve such a low bill.

Disclaimer: I will get a credit if you sign-up through my referral link, but so will you.

I need to write more.

In order to practice writing clearly and concisely,

to organize my thoughts,

to let small thoughts grow,

to store my thoughts in a less imperfect storage medium,

I need to write more.

And so begins a weekly¹ Rambling.

¹ hopefully.

Today I read Ur: Statically-Typed Metaprogramming with Type-level Record Computation. This paper presents the Ur language, a functional programming language based on an extension of System Fω. The novel idea is to use type-level functions as a form of type-safe meta-programming. The paper claims this novel idea enables safe heterogeneous and homogeneous meta-programming in Ur.

The interesting insight is that type-level computation may be valuable outside of dependently typed languages. The paper quickly and easily makes this case. The type-level computations reduce type annotations by enabling the programmer to compute types rather than manually write them everywhere. This could be a useful form of meta-programming in any typed language.

The claims about heterogeneous and homogeneous meta-programming seem overstated. Ignoring the novel ability to compute type annotations, type-safe heterogeneous programming could be as easily accomplished in any other type-safe language. I could just as easily (or more easily) write a program in Coq, ML, Haskell, or Typed Racket that generates HTML and SQL queries as I could in Ur. As for homogeneous meta-programming, restricting the meta-programs to record computations at the type-level seems to severely restricts the ability to generate code at compile-time and abstract over syntax, features which are provided by general-purpose meta-programming systems such as Racket’s macros or Template Haskell.

Yogurt is stupid expensive compared to the milk from which it is made, particularly if you want Greek-style yogurt.

So I decided to do it myself.

This summer I was in Paris for two months. Every day I got a fresh baguette for under €1. When I got back, I couldn’t eat store bought bread. It was terrible. And it cost $3. There’s no bakeries nearby, and the grocery store baguettes are crap and even more expensive.

So I decided to do it myself.

In my recent work, I found it useful to pair a term and its context in order to more easily reason about weakening the context. At the prompting of a colleague, I’ve been reading about Beluga, [1] [2], and their support for programming with explicit contexts. The idea seems neat, but I’m not quite sure I understand the motivations or implications.

So it seems Beluga has support for describing what a context contains (schemas), describing in which context a type/term is valid, and referring to the variables in a context by name without explicitly worrying about alpha-renaming. This technique supports reasoning about binders with HOAS in more settings, such as in the presence of open data and dependent types. Since HOAS simplifies reasoning about binders by taking advantage of the underlying language’s implementation of substitutions, this can greatly simplify formalized meta-theory in the presence of advanced features which previously required formalizing binders using more complicated techniques like De Bruijn indices. By including weakening, meta-variables, and parameter variables, Beluga enables meta-theory proofs involving binders to be much more natural, i.e., closer to pen-and-paper proofs.

Obviously this is great for formalized meta-theory. While I have seen how HOAS can simplify life for the meta-theorist, and seen how it fails, I don’t fully understand the strengths and weakness of this work, or how it compares to techniques such as the locally nameless. I’m also not sure if there is more to this work than a better way to handle formalization of binding (which is a fine, useful accomplishment by itself).

If anyone can elaborate on or correct my understanding, please do.

Sometimes I play minecraft. Sometimes I play a lot of minecraft and sometimes I just stop playing for months. Lately when I do play, I’ve bene playing with a slightly modified version of Tekkit and running my own server. I have a VPS that I probably under use, so I decided to run the server there for when I do play with my friends.

My VPS is not very powerful, and running a Minecraft server when I stop playing for months is a huge waste of resources. I sought a way to automatically bring the server up when I wanted to play and shut it down when I wasn’t playing for a while.

I wear my tinfoil hat proudly. I block ads, and JavaScript, and tracking cookies. I use HTTPS everywhere, I encrypt all my hard drives, I used randomly generated passwords, and I would encrypt all my emails if anyone else bothered to use GPG. I even run my own mail server, and have been considering running my own CalDAV and CardDAV server ...

But lately, I’ve been thinking maybe I should allow some ads and tracking, and let Google or Apple manage some of my data.

I’m converting my blog and website to Frog/Scribble.

This is my first post.

I like it better than Octopress. I get Racket and Scribble for templating, Markdown or Scribble support for blogging and pages, and I don’t need Ruby. The conversion process was dead simple, given that Octopress posts were already in Markdown.

FASTR is a bill to ensure all publically funded research is open access. I urge you all to contact your congresspeople and demand they support this bill.