Good Tuesday to you!

We had a languorous meeting last Friday, meandering torpidly through BER MetaOCaml and languidly ambling into digressions on modules, functors, lambda calculus extensions, LCM, CSP, CPS, LMS, FFTs, DSLs, and GHC APIs. The room was frowsty and we were all a bit knackered, but we persevered in untangling an entire staged function – proving yet again the old adage “if you need to entertain a group for half an hour, point them at a line of MetaOCaml”.

This coming Friday we’ll be reading “Go Meta!”, a staged programming advocacy paper from this year’s SNAPL. It will be a nice capstone for this metaprogramming arc, linking up a few loose ends and giving a glimpse of new vistas for future exploration. Reading Schedule

There has been discussion of taking a short break later in August, and subsequently diving into PFPL as our next book. Take a quick look at it, leave comments here or in Slack, and we’ll make a final schedule decision this coming Friday. It appears to cover many of the topics we’ve found interesting over the last six months, and ideally we’ll come out of it with a stronger foundation for reading more papers and building interesting things. PFPL Book

Happy coding!

Dann

Hey everyone, Reporting in from our Friday night session with Leo giving a demo of his Lisp DSL implementation and going over Taha’s comparison of implementing a DSL in 3 different languages, MetaOCaml, Template Haskell, and C++ Templates.

Next week is more MetaOCaml and we will cover Oleg Kiselyov’s paper “The Design and implementation of BER MetaOCaml”, in the usual time and place, Friday at 6:30pm at Bento Miso.

Also everyone who is available, on Wednesday at 6:30 Ben is giving the monthly papers we love talk at shopify, meetup link on programming with Algebraic Effects which he already started dropping some interesting facts from on Friday.

As for Friday, the discussion of Taha’s paper devolved somewhat into lamenting unresolved emotional issues stemming from overexposure to generic programming in C++. Since we were already familiar with the gentler MetaOCaml papers the material was already fairly comfortable for us which gave us lots of time for Leo to demo his Lisp DSL implementation, which in a cabal first was projected onto the big screen! With all this talk of metaprogramming, Lisp was certain to make an appearance sooner or later, since you know metaprogramming is kind of a thing in Lisp…

His code is available at his github. It was neat to see some of the strengths and weaknesses of the different implementations, as some of the approaches Leo used involved a few subtleties involving the Lisp macro system. Also, really cool was when he just quickly dropped down into inspect mode and drilled down to the actual assembly code that had been generated for his function, right from the interpreter! That is so cool, I had no idea you could do that.

Thanks again everyone, Until Next Time, Scott

Hello, computer people!

We had a perfectly lovely meeting on Friday, covering part two of part two of A Gentle Introduction to Multi-stage Programming. We started by revisiting Leo’s question from part one of part one of AGIMP, on the advantages brought by performing a CPS transformation on our exception handling interpreter. We made it further up the hill this time, but got a bit bogged down trying to understand precisely when evaluation of the various staged components occurs, how often that evaluation occurs, and how those answers impact the overall performance of the evaluation.

The primary focus of this pair of papers is interpreters, which turn out to be quite a bit different than regular programs when it comes to optimizations. If a regular program isn’t fast enough in Ruby, you rewrite the slow parts in C. But an interpreter could be orders of magnitude slower than desired – rewriting the interpreter in C isn’t likely to help in that case. Instead you need to write a compiler, which is an entirely different type program than the interpreter you’d like to speed up. Multi-stage programming is a way to speed up programs in general, but in particular it can speed up interpreters so they have compiler-like performance, which is really pretty fantastic.

After the break we spent some time simplifying and debugging Pete’s Haskell-based JS interpreter, which doesn’t use multi-stage programming but did reveal an interesting quirk in Haskell’s instance resolution procedure, which we initially thought was a bug in the FlexibleInstances extension due to the method of manifestation. Perhaps this coming Friday we’ll rewrite it in MetaOCaml, and stage a race between them.

Happy coding!

Dann

Hey everyone! Thanks for some stimulating discussion Friday night, we spent the night discussing Gentle Introduction to multi stage programming part 2.

Next week we are covering the second half of the paper, meeting at the usual time and place 6:30pm Friday at Bento Miso.

Leo spent some time elaborating on his point that the eval 6 in the previous paper was benefitting not so much from the various optimization a as from raising an exception instead of using Maybes everywhere, to settle this Pete fired up the MetaOCaml interpreter and patched in the modification and we compared the generated source code. At a glance they look similar, but we couldn’t quite decide if there was some subtle but important difference to the different generated code objects.

We seemed to pick up on a lot of the same comments in the text, for instance the comment about what if Haskell had been written with S expression syntax? Ben quipped, “Then they never would have found the Curry-Howard correspondence.” He is joking of course, maybe they would have anyway, but it started a rather wide ranging discussion on how syntax influences thought, touching upon a variety of languages as well as the distinctions between Newton’s calculus of fluxions syntax and Leibniz’ in many ways superior calculus of infinitesimals.

It’s intriguing as humans that we tend to be quite aware of what new powers our tools give us but rarely do we see as clearly how our tools in turn shape us.

Until next time, Scott

Double recap!! This week we covered Taha’s excellent tutorial, A gentle introduction to Multi stage programming (MSP) with MetaOCaml. We chose this one because it had Gentle in the title, and I think it succeeded in that respect, also in a weird convergence of Toronto developer communities, Julie Hache gave a nice intro on Wednesday to zero-overhead metaprogramming at Papers We love (Meetup Link ).

Two weeks ago we were discussing Wadler and Blott’s 1988 paper, How to make ad-hoc polymorphism less ad-hoc, and enjoyed several fruitful divergences including monoids and the representation of numbers. Not going to get into detail, but basically as far as floating point numbers go I think we can all agree if they float on water, then we need to burn them.

Next week we will delve deeper into MetaOCaml with Taha’s gentle introduction part deux, where we will use MSP to develop “Aloe”, possibly the world’s only interpreter named after a soothing medicinal herb and perhaps useful after some self-inflicted second degree floating point burns.

We had a more hands on discussion this week as we spent some time together playing the MetaOCaml interpreter Pete had running. Examining the expansions of the examples in the paper was quite interesting and Leo’s test of accepting data from stdin was also revealing. Discussion touched on a variety of topics, including meta programming in the Lisp AST and how many levels of meta is desirable, can you be too meta? We weren’t sure, but there are other goals to shoot for in this respect, Meta-Analysis.

Looking forward to spending some more time with this next week, until then, Scott

Friday Night Recap! Thanks for a fantastic evening everyone! We spent our time going over a variety of Free Theorems from Wadler’s paper and some examples of their use. So though we didn’t fully penetrate the details of section 5 and 6, I found this discussion of examples and the consequences of the various theorems highly enlightening. Again a big thanks to Pete, who I think can safely hold the title of resident Wadler guru :).

This Friday night we meet again at the usual time and place (Bento Miso at 6:30pm) we will be starting a new paper and a new month, “Miranda ML MetaML MetaMetaML and MegaMetaML”, beginning with the paper, “How to make ad-hoc polymorphism less ad-hoc”, by our dear old friend Philip Wadler (The paper).

We first looked at a fold over cons with a plus 2 map and we worked out what the functions had to be on the other side of the equation,

map (+2) . fold (:) [] = fold (:) [] . map (+2)

This says that you can either add 2 to each value and then cons them into a new list, or you can cons them into a list and then add 2. This type of transformation can be combined with map fusion and applied automatically by a compiler to transform inefficient code into something more efficient. For instance in the two equivalent expressions,

map (+2) . fold (:) [] . map (*3) = fold (:) [] . map (+2) . map (*3)

the left hand side will have to traverse the data twice, while on the right hand side only once. This is because of the map after the fold which makes it wait until the new list is constructed before proceeding.

This was one of a few different examples, we also looked into the fold fusion law which is related but more confusing somehow. Pete brought up a fascinating example where the fold plus map law can theoretically be applied even if the g function is something like sha1, making the other side of the equation difficult (impossible?) to compute,

sha1 . fold ++ u = fold ++' u' . map a

Where here ++ is concatenation and u is a string, and the expression accepts as input a list of strings. The problem is then what is the function a? And what is this other concatenation operator ++’? We know you can’t compute the sha1 piecewise, so it’s quite unclear what these operators would be or how to write them down.

We also went through polymorphic equality in section 3.4 in some detail as it is quite different from the other laws, what he is describing is close to Haskell type classes. It’s really quite an interesting result, it shows that for equality we can’t have a fully parametric function, instead we need to restrict to a set of types related by the function in a one to one way, so for instance strings and integers with the function strlen will have problems since all the strings of the same length would seem equal to each other. The type classes approach lets us keep using our Free theorems by restricting the scope of the parametricity, so no longer is the function fully parametric but only over some subset of the types satisfying a given set of conditions.

See you all next week, Scott

Hey Everyone, Smaller crowd on Friday as it seems with summer approaching many things are afoot, but that didn’t stop our intrepid group of 3 from pondering the eternal type theoretic question, “what would Philip Wadler do?” (WWWD). Next week is everyone else’s chance to ask WWWD, as we will continue reading his paper “Theorem’s for Free!” In our third and final instalment at the usual time and place Friday at 6:30pm at Bento Miso.

Bento Miso has been an incredible host for our meetings for more than a year. The community that Henry, Jennie, and Dann have created is vibrant, creative, and an important part of the Toronto art, video game, and development community. Bento Miso is a leading member of the Toronto Media Art Collective (TMAC) and I encourage you all to read about and support TMAC in their recent conflict with Urbancorp and the City of Toronto over a new nine million dollar facility. Both the city and the condo developer Urbancorp have reneged on a done deal at the eleventh hour, leaving TMAC out to dry.

WWWD? Fight til the last lambda has been applied!* TMAC is now pursuing legal and bureaucratic avenues to restore the agreement and can use our support, read more about it at http://tomediaarts.org/open-letter/ .

For the paper, we didn’t get too far, we went through 3.1 and 3.2 where he covers the proof of the first theorem he introduced at the start of the paper and the fold rearrangement theorem. We found we could follow the math, but we’re struggling to understand the full significance of the results and how they are used. Luckily Pete has already come to the rescue on slack :). Turns out it’s really important for performance optimization so hopefully he’ll be able to make it out Friday and share some of his stuff with us. We spent a lot of time working out on the white board the example in section 7 demonstrating why if you add a fixed point function to the language you can only use strict functions and almost succeeded in deriving it but got bogged down on evaluating the fixed point function composed with the identity function.

We also found ample divergence time and were talking about science fiction a bit more than usual which was highly enjoyable.

Until Friday, Scott

• I don’t him personally, but he speaks at comedy clubs so I think he could take the joke, also he knows recursive functions, so his supply of lambdas is effectively infinite.?

Greetings Caballeros, Ample cookies and confusionators were in attendance on Friday for what proved to be the longest session to date, which we may need to work on limiting in future. On the menu was parts 1 and 2 of Philip Wadler’s paper, “Theorems for free!”, a hearty, substantial dish. We made good headway and we will continue to chew on it together next week at the usual time and place, Friday at 6:30pm @ Bento Miso.

I am loving this paper so far, I still don’t understand that much, but I think that may be why I like it. The paper starts out deceptively fun; a cool title with an exclamation mark in it, the first page covers an example that seems intuitive, and then another full page of examples that seem more or less plausible if you don’t think too hard on them. Then there are some hints that all may not be as it seems. For one, I found my background knowledge lacking and the connection between fixed points and the strong normalization property of type systems required further research. Following that, Dann pointed out that in the second paragraph on page 4, there are a lot of unfamiliar keywords; “parametricity”, “polymorphic lambda calculus”, “representation theorem”, “abstraction thereom”, “dinatural transformations”, and “whom” (grammatically accurate, but who uses whom?). But the bomb comes in section 2 which begins with, “The key to extracting theorems from types is to read types as relations.” Wait, What?! What does that even mean? Wadler!

We spent a good portion of the evening going through section 2, exploring many examples of different types as relations, what functions on types look like, how they might be useful, and then it got late and we never quite got through the polymorphic expressions. I’m going to try and write out our examples and put them on the wiki, and maybe explore them in some more detail as I think they helped shed light on what the motivations for types as relations and the consequences of using them are. Special thanks to Pete for bringing up the geometric interpretation of the relational types and the excellent example of using relations as data abstraction to implement a complex number type in either Cartesian or polar coordinates. I think those ideas really helped bring to life the mathematical definitions of relational types in section 2.

Anyway, all for now, looking forward to our next meeting, Scott

Hey Everyone! So it turns out that simplifying logic proofs is equivalent to evaluating computer programs, what!?

In our drifting slide through the theory of types and programming languages, last week we careened into Philip Wadler’s lovely new paper, “Propositions as Types”, which serves as introduction, historical guide, and comic relief to the deep and (at least still for me) magical and mysterious result that logic and program evaluation are deeply entangled with each other. For those with shorter attention spans, he covers a lot of the comedy and history as a quite succesful comedy routine, http://youtu.be/GnpcMCW0RUA, again, what!?

Ricocheting off of our first Wadler paper, this Friday we will start our way through another of Wadler’s papers, “Theorems for Free”, at the usual time and place, 6:30pm at Bento Miso.

I really enjoyed reading this paper, it’s accessible, it has a lot of funny historical anecdotes and he ties them together with both the personalities involved and where they fit conceptually in a greater academic context. The core relation between logic and program evaluation is explored via a clear and pleasantly didactic introduction to the notation for proofs in natural deduction (section 7) and for simply typed lambda calculus (section 8). There is a lot here and the breadth of topics led to a lot of stimulating discussion and to one of the longest sessions to date, although I don’t think any of us noticed the time.

One thought I had while leaving is that often while writing programs you approach things from an aesthetic or design perspective, but this isomorphism tells us that maybe under our aesthetics there is a clear precise mathematical truth. I’m not sure if that last statement is true, but it’s tantalizing to think that you can pin down design concepts into a mathematical equation. I remember being very excited reading all the books I could about chaos theory and fractals. I was at an impressionable age so I believed all of their predications, especially the early super enthusiastic ones; equations to solve nature, everything from weather patterns to the social dynamics affected by your choice of tie, but then when I finally got past the fanciful claims all I got was a fistful of ferns.

Maybe we can keep iterating on this and come up with something, Until next time, Scott?

Hi Everyone! Thanks for another great session, where we went over Milner’s algorithm J and finished off the last sections of the paper. We followed that up by discussing the 3 questions I had left for everyone last week.

The group is now taking a 1 week hiatus while Dann is off presenting his work on visualizing computer processes in Florida (go Dann!), but we will be back with a vengeance in 2 weeks. Meeting at 6:30pm, Friday June 5th at Bento Miso to cover Philip Wadler’s forthcoming article, Propositions as types (http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf). Sorry Ben!

Maybe it’s just the amount of time we’ve now spent reading Milner, but I left Friday feeling like Algorithm J made sense to me, which felt unusual indeed :). Some of Pete’s explanations really helped clarify it for me in particular, thanks Pete! During the discussion, Chris brought up a famous quote from Milner, “Types are the leaven of computer programming: they make it digestible” and the more I think about it the more apt it seems. Although unleavened bread goes great with chicken tikka kabobs so maybe there is something to be said for flavour. Perhaps of interest, I found these slides from Pierce that start with Milner’s quote and give his take on Milner’s types, http://www.cis.upenn.edu/~bcpierce/papers/TypesALaMilner.pdf.

After a short celebration we discussed developing programs in typed and untyped languages at great length and I found a lot of very interesting and revealing anecdotes in what everyone said. I think we covered a lot of important design considerations, practical and theoretical contrasting typed and untyped languages. I don’t know precisely how we will use this information just yet, but it seems useful so rather than try to summarize, I just tried to remember as best as I could what everyone said and added everything to a wiki page in github, https://github.com/CompSciCabal/SMRTYPRTY/wiki/Discussion!-Practical-Aspects-of-Types. I encourage you to go take a look and correct my numerous omissions and glaring errors.

Enjoy the break, see you all back in June, Scott?