## Modern art with diagrams: the face of progress

As an addendum to my previous post, here are a few outputs generated while I was debugging:

For extra credit, deduce what the bugs were. ;)

Posted in diagrams | Tagged , , , , | 5 Comments

## Generating plane tilings with diagrams

I’ve finally set up a diagrams-contrib package to serve as a home for user contributions to the diagrams project—generation of specialized diagrams, fun or instructive examples, half-baked ideas, stuff which is not sufficiently polished or general to go in the diagrams-lib package but is nonetheless worth sharing.

As the first “contribution” I put some code I wrote for fun that generates tilings of the Euclidean plane by regular polygons.

So how does it work? I’m sure there are more clever ways if you understand the mathematics better; but essentially it does a depth-first search along the edge graph, stopping when it reaches some user-defined limit, and drawing polygons and edges along the way. This sounds quite simple on the face of it; but there are two nontrivial problems to be worked out:

1. How can we tell whether we’ve visited a given vertex before?
2. How do we represent a tiling in a way that lets us easily traverse its edge graph?

The first question is really a question of representation: how do we represent vertices in such a way that we can decide their equality? Representing them with a pair of floating point coordinates does not work: taking two different paths to a vertex will surely result in slightly different coordinates due to floating point error. Another idea is to represent vertices by the path taken to reach them, but now we have to deal with the thorny problem of deciding when two paths are equivalent.

But it turns out we can do something a bit more clever. The only regular polygons that can appear in plane tilings are triangles, squares, hexagons, octagons, and dodecagons. If you remember your high school trigonometry, these all have “special” angles whose sines and cosines can be represented exactly using square roots. It suffices to work in $\mathbb{Q}[\sqrt{2}, \sqrt{3}]$, that is, the ring of rational numbers adjoined with $\sqrt{2}$ and $\sqrt{3}$. Put simply, we use quadruples of rational numbers $(a,b,c,d)$ which represent the real number $a + b\sqrt{2} + c\sqrt{3} + d\sqrt{6}$. Now we can represent vertices exactly, so remembering which we’ve already visited is easy.

The other question is how to represent tilings. I chose to use this “zipper-like” representation:

data Tiling = Tiling [TilingPoly] (Int -> Tiling)

Intuitively, a Tiling tells us what polygons surround the current vertex (ordered counterclockwise from the edge along which we entered the vertex), as well as what configurations we can reach by following edges out of the current vertex. Thanks to laziness and knot-tying, we can easily define infinite tilings, such as


t4 :: Tiling
t4 = Tiling (replicate 4 Square) (const t4)


This is a particularly simple example, but the principle is the same. You can look at the source for more complex examples.

Of course, this doesn’t really show off the capabilities of diagrams much (you can draw regular polygons with any old graphics library), but it sure was fun!

Posted in diagrams, haskell, math, projects | Tagged , , | 1 Comment

## Wanted GHC feature: warn about unused constraints

Consider the following function:

 

foo :: (Show a, Ord a) => a -> a -> String
foo x y = show x ++ show y

 

Currently (as of GHC 7.2.1) when compiling this code with -Wall, no warnings are generated. But I’d really love to get a warning like

 

Foo.hs:1:1: Warning: Unused constraint: Ord a

 

I see no theoretical impediments here. At the level of fully desugared and elaborated GHC core, it is no harder to tell which constraints are unused than which arguments are unused, because constraints are arguments.

One possible objection is that there is some inherent ambiguity here. For example, consider:

 

bar :: (Eq a, Ord a) => a -> a -> String
bar x y | x == y    = "yay"
| otherwise = "boo"

 

When elaborating bar, GHC has a free choice of where to get the needed (==) method: from the Eq constraint or from the Eq superclass of the Ord constraint. So we might get a warning about Eq being redundant or about Ord being redundant, depending on which one it decides to use. But I don’t see this as a big problem.

I think this could make for a nice project for someone wanting to dig into hacking on GHC. Perhaps I’ll do it myself at some point if no one else takes it on.

## More counting lambda terms

Yesterday someone submitted a comment to an old post of mine about counting linear lambda terms, asking the following question:

I am interested in a similar problem: given a natural number N, what is the number of different symply-typed closed lambda terms with size smaller than N?

They don’t need to be observationally different. They should be different modulo renaming of variables and types, though. So:

lambda x^A.x and lambda y^B.y

should be considered the same…

Do you know where I can find the answer? Answers using any kind of size measurement would be fine for me…

It’s an interesting question, and I thought it would make for a good way to illustrate one of my favorite techniques when trying to research a combinatorial question like this. Namely, write a program to compute the first few values by brute force, then look it up in the Online Encyclopedia of Integer Sequences and follow the references.

> module CountSTLC where
>
> type Nat = Int  -- just pretend


A type for deBruijn-indexed lambda terms.

> data Tm = Var Nat
>         | App Tm Tm
>         | Lam Tm
>   deriving (Eq, Ord, Show)


We’ll define the size of a term as the number of constructors used by its representation in the above data type.

> size :: Tm -> Nat
> size (Var _)     = 1
> size (App t1 t2) = 1 + size t1 + size t2
> size (Lam t)     = 1 + size t


Here’s a function to generate all the closed Tms of a given size. We pass along an index giving the current level of nesting (so we know what variables are available).

> genAll :: Nat -> [Tm]
> genAll = genAll' 0
>   where


There are no terms of size zero (or smaller).

>     genAll' _   n | n <= 0 = []


The only terms of size 1 are variables. We can choose to refer to any of the currently enclosing lambdas.

>     genAll' ctx 1 = map Var [0 .. ctx-1]


Otherwise, we could have an application (splitting the available size between the two sides in all possible ways) or a lambda (remembering to increment the nesting level).

>     genAll' ctx n = [ App t1 t2
>                     | n1 <- [1 .. n-2]
>                     , t1 <- genAll' ctx n1
>                     , t2 <- genAll' ctx (n - n1 - 1)
>                     ]
>                  ++ (map Lam (genAll' (succ ctx) (n-1)))


Let’s see what we get:

*CountSTLC> genAll 4
[ Lam (App (Var 0) (Var 0))
, Lam (Lam (Lam (Var 0)))
, Lam (Lam (Lam (Var 1)))
, Lam (Lam (Lam (Var 2)))
]

Looks reasonable: there are four closed lambda terms of size 4. Now let’s count:

*CountSTLC> map (length . genAll) [1..10]
[0,1,2,4,13,42,139,506,1915,7558]

Searching for this sequence on OEIS turns up something promising, with a bit of information including a formula for computing the counts directly. It also has a link to someone’s research but unfortunately it seems dead. But it does have the email address of the person who submitted this sequence, and emailing him might be a good start!

This is all well and good, but the commenter actually asked for simply typed lambda calculus terms. The first size-4 lambda term above is not well-typed, since it involves a self-application. Can we modify our program to only generate well-typed lambda terms? This seems much more difficult. I may write about it in a future post. For now I’ll leave it as an exercise for the interested and motivated reader!

## Announcing diagrams-0.4

I am pleased to announce the release of version 0.4 of diagrams, a full-featured framework and embedded domain-specific language for declarative drawing.

The last announcement was of the 0.1 release; there have been quite a few changes and improvements since then, including:

• A new website including a gallery of examples
• A new comprehensive user manual with lots of illustrative examples
• New primitive shapes: rounded rectangles, wedges, and a new flexible API for generating polygons
• Cubic splines
• Basic text support
• Support for external image primitives
• Lots more convenient combinators, bug fixes, and improvements

## Cool, how can I try it out?

For the truly impatient:

cabal install gtk2hs-buildtools
cabal install diagrams


For the slightly less impatient, read the quick tutorial, which has detailed information about how to install the necessary packages and will introduce you to the fundamentals of the framework.

For those who are even less impatient but want to really dig in and use the power features, read the user manual.

## Cool, how can I contribute?

There are lots of ways you can contribute! First, you may want to subscribe to the project mailing list, and/or come hang out in the #diagrams IRC channel on freenode.org.

• There are lots of easy bug fixes, improvements, and feature requests just waiting for people wanting to get involved: see the bug tracker for a list of open tickets.

The source repositories are mirrored using both darcs (on patch-tag.com) and git (on github.com), and patches are accepted in either place, thanks to Owen Stephen’s great work on darcs-bridge.

• Create a higher-level module built on top of the diagrams framework (e.g. tree or graph layout, generating Turing machine configuration diagrams, Penrose tilings … your imagination is the only limit!) and submit it for inclusion in a special diagrams-contrib package which will be created for such higher-level user-contributed modules.
• Use diagrams to create some cool graphics and submit them for inclusion in the gallery.
• Start your own project built on top of diagrams and let us know how it goes!
• Last but certainly not least, just try it out for your pet graphics generation needs and contribute your bug reports and feature requests.

Happy diagramming!

Brought to you by the diagrams team:

• Brent Yorgey
• Ryan Yates

with contributions from:

• Sam Griffin
• Claude Heiland-Allen
• John Lato
• Vilhelm Sjöberg
• Luite Stegeman
• Kanchalai Suveepattananont
• Scott Walck
Posted in haskell, projects | Tagged , , , | 2 Comments

## Effective parse tree support for the working semanticist

If, like me, you spend large amounts of time designing, discussing, and proving things about programming languages and formal calculi, chances are you have used Ott (and if you do, but you haven’t, you are really missing out). You write down a formal system once, in a special format that Ott understands, and Ott typechecks it and can automatically generate nice LaTeX as well as code for proof assistants like Coq or Isabelle.

However, anyone who has worked with Ott is familiar with is the dreaded ambiguous parse error. Quite often Ott grammars end up being ambiguous, and Ott needs some guidance to know which parse you want. However, the error messages are horrendous: Ott spews forth several massive parse trees in a format requiring formidable patience to read. Finding the slight differences between two such parse trees is an exercise in seizure-inducing tedium.

I got sick of this so I wrote a little tool to help, which is now available on Hackage: ottparse-pretty. You paste in an Ott parse tree and it shows it to you in a nicely formatted tree view with a bunch of useless cruft removed. For example, it turns this:

 (St_node :formula:formula_judgement: (Ste_st (St_node :judgement:judgement_Jtype: (Ste_st (St_node :Jtype:coerce: (Ste_st (St_nonterm G)) (Ste_st (St_nonterm g)) (Ste_st (St_node :s:T_MultiTypeApp: (Ste_st (St_node :s:T_EqTy: (Ste_st (St_node :s:T_MultiTypeApp: (Ste_st (St_node :s:T_MultiKindApp: (Ste_st (St_node :s:T_Cons: (Ste_st (St_nonterm H)))) (Ste_st (St_nonterm k)))) (Ste_st (St_nonterm t)))) (Ste_st (St_node :s:T_MultiKindApp: (Ste_st (St_node :s:T_Cons: (Ste_st (St_nonterm H)))) (Ste_st (St_nonterm k)))))) (Ste_st (St_nonterm t'))))))))) 

into this:

 

formula_judgement
|
- judgement_Jtype
|
- coerce
|
+- G
|
+- g
|
- T_MultiTypeApp
|
+- T_EqTy
|  |
|  +- T_MultiTypeApp
|  |  |
|  |  +- T_MultiKindApp
|  |  |  |
|  |  |  +- T_Cons
|  |  |  |  |
|  |  |  |  - H
|  |  |  |
|  |  |  - k
|  |  |
|  |  - t
|  |
|  - T_MultiKindApp
|     |
|     +- T_Cons
|     |  |
|     |  - H
|     |
|     - k
|
- t'

 

It’s pretty simplistic at the moment—I may add more features depending on feedback. But it’s been useful for me so it seemed worth packaging it up in case it’s useful to anyone else.

Posted in haskell, projects | Tagged , , , , , | 2 Comments

## diagrams repos now mirrored on github!

I was quite excited when I learned that Owen Stephens was working on a two-way darcs-git bridge for his Google Summer of Code project. You see, I’m one of those holdouts who, despite acknowledging that github is pretty cool and a lot of people in the Haskell community are using it these days, still really loves darcs and refuses to give it up. Well, thanks to Owen’s great work, it looks like I can now have my cake and eat it too.

I’ve now mirrored four diagrams repositories on github:

• diagrams-core – core library
• diagrams-lib – standard library of primitives and combinators built on top of diagrams-core
• diagrams-cairo – rendering backend using cairo
• diagrams-doc – documentation for the project, including source code for the website, tutorial, user manual, IRC logs, etc.

I will continue to use darcs as my primary VCS, and of course I will still accept darcs patches (the darcs repos are hosted on patch-tag.com). But I can now accept pull requests on github, for contributors who prefer using git/github. It will probably take a while to get the kinks worked out and figure out how to manage everything properly. But I’m excited by the opportunity to encourage more collaboration.

Oh yes, and the user manual is coming along nicely! You can see a preview version here. Comments and patches (via either darcs or git!) welcome. There have also been quite a few cool features added since the 0.3 release, and we hope to have an 0.4 release out soon.