Teaching & Learning

Dependently-Typed Metaprogramming (in Agda)

Conor McBride gave an 8-lecture summer course on Dependently typed metaprogramming (in Agda) at the Cambridge University Computer Laboratory:

Dependently typed functional programming languages such as Agda are capable of expressing very precise types for data. When those data themselves encode types, we gain a powerful mechanism for abstracting generic operations over carefully circumscribed universes. This course will begin with a rapid depedently-typed programming primer in Agda, then explore techniques for and consequences of universe constructions. Of central importance are the “pattern functors” which determine the node structure of inductive and coinductive datatypes. We shall consider syntactic presentations of these functors (allowing operations as useful as symbolic differentiation), and relate them to the more uniform abstract notion of “container”. We shall expose the double-life containers lead as “interaction structures” describing systems of effects. Later, we step up to functors over universes, acquiring the power of inductive-recursive definitions, and we use that power to build universes of dependent types.

The lecture notes, code, and video captures are available online.

As with his previous course, the notes contain many(!) mind expanding exploratory exercises, some of which quite challenging.

Socio-PLT: Principles for Programming Language Adoption

In their survey paper and their website, Leo Meyerovich and Ari Rabkin take Jared Diamond approach to explaining Programming Language adoption.

Why do some programming languages fail and others succeed? What does the answer tell us about programming language design, implementation, and principles? To help answer these and other questions, we argue for examining the sociological groundings of programming language theory: socio-PLT.
Researchers in the social sciences have studied adoption in many contexts. We show how their findings are applicable to programming language design.

There are also videos of talks available from Splash 2012 and Google Tech Talks.

See also previous discussions.

Brown CS: CSCI 1730: Programming Languages: On-Line Offering

We will be making this course, Brown's upper-level programming languages offering, available for free on the Web. People anywhere are welcome to view the lectures, read the materials, and do the assignments

This is a great opportunity! I have relied heavily on Shriram's lecture notes when I was starting out.

It is nice to see that he promises to give personal recognition for those who participate, and even has a system in place for giving partial credit to busy professionals who cannot spare the time to do all the assignments and projects.

My only misgiving is that the course uses Racket; I wish it was in Scheme.

Google Blockly Lets You Hack With No Keyboard

Following on from recent discussions about graphical languages in the Russian space program, here's a recent story about Google's new visual programming language.

Cade Metz, "Google Blockly Lets You Hack With No Keyboard", Wired Enterprise.

Now available on Google Code — the company’s site for hosting open source software — the new language is called Google Blockly, and it’s reminiscent of Scratch, a platform developed at MIT that seeks to turn even young children into programmers.

As the Blockly FAQ says, "Blockly was influenced by App Inventor, which in turn was influenced by Scratch." So if you've seen Scratch before, this will look very familiar. If you haven't seen Scratch, and want to have a go with Blockly, you can find the maze demo from the Wired story here.

Interactive Tutorial of the Sequent Calculus

Interactive Tutorial of the Sequent Calculus by Edward Z. Yang.

This interactive tutorial will teach you how to use the sequent calculus, a simple set of rules with which you can use to show the truth of statements in first order logic. It is geared towards anyone with some background in writing software for computers, with knowledge of basic boolean logic. ...

Proving theorems is not for the mathematicians anymore: with theorem provers, it's now a job for the hacker. — Martin Rinard ...

A common complaint with a formal systems like the sequent calculus is the "I clicked around and managed to prove this, but I'm not really sure what happened!" This is what Martin means by the hacker mentality: it is now possible for people to prove things, even when they don't know what they're doing. The computer will ensure that, in the end, they will have gotten it right.

The tool behind this nice tutorial is Logitext.

The Algebra of Data, and the Calculus of Mutation

Kalani Thielen's The Algebra of Data, and the Calculus of Mutation is a very good explanation of ADTs, and also scratches the surfaces of Zippers:

With the spreading popularity of languages like F# and Haskell, many people are encountering the concept of an algebraic data type for the first time. When that term is produced without explanation, it almost invariably becomes a source of confusion. In what sense are data types algebraic? Is there a one-to-one correspondence between the structures of high-school algebra and the data types of Haskell? Could I create a polynomial data type? Do I have to remember the quadratic formula? Are the term-transformations of (say) differential calculus meaningful in the context of algebraic data types? Isn’t this all just a bunch of general abstract nonsense?

(hat tip to Daniel Yokomizo, who used to be an LtU member...)

Cambridge Course on "Usability of Programming Languages"

From the syllabus of the Cambridge course on Usability of Programming Languages

Compiler construction is one of the basic skills of all computer scientists, and thousands of new programming, scripting and customisation languages are created every year. Yet very few of these succeed in the market, or are well regarded by their users. This course addresses the research questions underlying the success of new programmable tools. A programming language is essentially a means of communicating between humans and computers. Traditional computer science research has studied the machine end of the communications link at great length, but there is a shortage of knowledge and research methods for understanding the human end of the link. This course provides practical research skills necessary to make advances in this essential field. The skills acquired will also be valuable for students intending to pursue research in advanced HCI, or designing evaluation studies as a part of their MPhil research project.

Is this kind of HCI based research going to lead to better languages? Or more regurgitations of languages people are already comfortable with?

CRA-W/CDC and SIGPLAN Programming Languages Mentoring Workshop

CRA-W/CDC and SIGPLAN Programming Languages Mentoring Workshop, Philadelphia, PA (co-located with POPL 2012) Tuesday January 24, 2012

We are pleased to invite students interested in programming languages research to the first PL mentoring workshop. The goal of this workshop is to introduce senior undergraduate and early graduate students to research topics in programming language theory as well as provide career mentoring advice to help them get through graduate school, land a great job, and succeed. We have recruited leaders from the programming language community to provide overviews of current research topics, and have organized panels of speakers to give students valuable advice about how to thrive in graduate school, search for a job, and cultivate habits and skills that will help them in research careers.

This workshop is part of the activities surrounding POPL, the Symposium on Principles of Programming Languages, and takes place the day before the main conference. One goal of the workshop is to make the POPL conference more accessible to newcomers and we hope that participants will stay through the entire conference.

Through the generous donation of our sponsors, we are able to provide travel scholarships to fund student participation. These travel scholarships will cover reasonable travel expenses (airfare, hotel and registration fees) for attendance at both the workshop and the POPL conference. Anyone may apply for a travel scholarship, but first priority will be given to women and under-represented minority applicants.

The workshop registration is open to all. Students with alternative sources of funding for their travel and registration fees are welcome.

The travel funding application can be accessed from the workshop web site. The deadline for full consideration of funding is December 2, 2011. Selected participants will be notified starting December 9th and will need to register for the workshop by December 24th.

Stephanie Weirich, Kathleen Fisher and Ron Garcia

The Computing Research Association's Committee on the Status of Women (CRA-W), the Coalition to Diversify Computing (CDC), and the ACM Special Interest Group on Programming Languages (SIGPLAN).

We don't usually post conference or workshop announcements on the front page, but this seemed sufficiently new and worthy to me. Please note that the deadline for the application for travel support is only two days away!

Programming and Scaling

Programming and Scaling, a one-hour lecture by Alan Kay at his finest (and that's saying something!)

Some of my favorite quotes:

  • "The biggest problem we have as human beings is that we confuse our beliefs with reality."
  • "We could imagine taking the internet as a model for doing software modules. Why don't people do it?" (~00:17)
  • "One of the mistakes that we made years ago is that we made objects too small." (~00:26)
  • "Knowledge in many cases trumps IQ. [Henry] Ford was powerful because Isaac Newton changed the way we think." (~00:28)
  • "Knowledge is silver. Outlook is gold. IQ is a lead weight." (~00:30)
  • "Whatever we [in computing] do is more like what the Egyptians did. Building pyramids, piling things on top of each other."
  • "The ability to make science and engineering harmonize with each other - there's no greater music." (~00:47)

And there are some other nice ideas in there: "Model-T-Shirt Programming" - software the definition of which fits on a T-shirt. And imagining source code sizes in terms of books: 20,000 LOC = a 400-page book. A million LOC = a stack of books one meter high. (Windows Vista: a 140m stack of books.)

Note: this a Flash video, other formats are available.

Levy: a Toy Call-by-Push-Value Language

Andrej Bauer's blog contains the PL Zoo project. In particular, the Levy language, a toy implementation of Paul Levy's CBPV in OCaml.

If you're curious about CBPV, this implementation might be a nice accompaniment to the book, or simply a hands on way to check it out.

It looks like an implementation of CBPV without sum and product types, with complex values, and without effects. I guess a more hands-on way to get to grips with CBPV would be to implement any of these missing features.

The posts are are 3 years old, but I've only just noticed them. The PL Zoo project was briefly mentioned here.

XML feed