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.

Math.Tau

I have just uploaded a new package to Hackage which defines the constant $\tau$. Now if you wish to use $\tau$ in your program you can just cabal install tau and then import Math.Tau (tau), and be assured that you are using only the highest-quality definition of this fundamentally important constant.

Unbound now supports “set” binders and GADTs

I have just uploaded version 0.3 of the Unbound library (and version 0.5 of RepLib). This version adds support for two major new features:

• The new permbind and setbind functions create binders that are alpha-equivalent “up to permutation”. For example, when quantifying over a list of type variables, their order really does not matter: $\forall a b. a \to b \approx \forall b a. a \to b$. Unbound now lets you express this and takes it into account when testing alpha-equivalence.
• RepLib (and hence Unbound) now supports GADTs, as long as they do not contain any existential quantification.

Enjoy!

Yesterday I was looking for a way to have some Template Haskell code generate a definition for a certain identifier if and only if such a definition did not already exist. Essentially I want to be able to call the code multiple times but have it generate something only once. This turns out to be extremely easy but non-obvious, so I thought I’d write it here for posterity. The trick is that reify throws an error if called on an identifier that doesn’t exist, and recover can be used to catch TH errors. Thus:


which uses generateBinding n to “recover” from the error of n‘s non-existence.