Gui Half-Epigram

Here’s just a quick jot of an idea before I give my bed a much-needed visit.

Recently I’ve become interested in dependent types, a la Epigram and Agda. I like Agda’s concise style more, but Epigram definitely has an appeal from a user interface perspective. Let’s not be fooled, Epigram’s user interface is terrible, but it shows an amazing amount of potential.

So I got to thinking, what could you do in a Epigram-inspired style for a non-dependent language as far as GUI-based programming. It wouldn’t be as powerful, of course, because the compiler has far less information in languages like that, but you still might be able to get away with something. In particular, when I’m implementing very general functions, such as Arrow instances, I often do type-directed programming. Essentially I just find a series of functions which typechecks and there’s a high chance that it will be the correct implementation.

Here’s the GUI idea. You have a list of all the types you “have” (labeled with what they are of course), and a list of types you “need”. Then, say, you’d click on something you have and it would show you everything you could do to it; i.e. all functions which accept that type as an argument. There would naturally be very many of these things, so you’d need some sort of smart search. You click on one of those things, and it would add the return type of the function to the list of things you have, and add the other arguments to the list of things you need.

It would work in the other direction too: you could click on one of the types you need, and it would show you all the functions which return that type.

This is essentially Epigram’s method, but with a bottom-up component as well. Epigram can be precise about it, this interface would be less precise, more of a helper tool. I think it deserves a prototype though, since it represents a leap from textual information to spatial information (if you presented it right), and brains are very much better at manipulating spatial information.


2 thoughts on “Gui Half-Epigram

  1. There’s an autocomplete helper for Java in Eclipse which did something like this. Called “Jungloid mining”, the paper is at: and

    The idea was given the type you want to get, and an object, it showed you the likely calls to get from the object you have to the one you want. I’m not sure if that corresnponds with what you’re suggesting actually, but I hope you find it interesting!

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s