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. ;)
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. ;)
I’ve finally set up a diagramscontrib package to serve as a home for user contributions to the diagrams project—generation of specialized diagrams, fun or instructive examples, halfbaked ideas, stuff which is not sufficiently polished or general to go in the diagramslib 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 depthfirst search along the edge graph, stopping when it reaches some userdefined 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:
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 , that is, the ring of rational numbers adjoined with and . Put simply, we use quadruples of rational numbers which represent the real number . 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 “zipperlike” 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 knottying, 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!
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.
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 symplytyped 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.
Let’s start with untyped lambda calculus terms.
> module CountSTLC where
>
> type Nat = Int  just pretend
A type for deBruijnindexed 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 Tm
s 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 .. ctx1]
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 .. n2]
> , t1 < genAll' ctx n1
> , t2 < genAll' ctx (n  n1  1)
> ]
> ++ (map Lam (genAll' (succ ctx) (n1)))
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 size4 lambda term above is not welltyped, since it involves a selfapplication. Can we modify our program to only generate welltyped 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!
I am pleased to announce the release of version 0.4 of diagrams, a fullfeatured framework and embedded domainspecific 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:
For the truly impatient:
cabal install gtk2hsbuildtools
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.
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.
The source repositories are mirrored using both darcs (on patchtag.com) and git (on github.com), and patches are accepted in either place, thanks to Owen Stephen’s great work on darcsbridge.
Happy diagramming!
Brought to you by the diagrams team:
with contributions from:
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 seizureinducing tedium.
I got sick of this so I wrote a little tool to help, which is now available on Hackage: ottparsepretty. 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.
I was quite excited when I learned that Owen Stephens was working on a twoway darcsgit 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:
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 patchtag.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.