On Monday I went to the first day of Conor McBride's course Introduction to Dependently-Typed programming in Agda. "What's dependently-typed programming?" you ask. Well, when a compiler type-checks your program, it's actually (in a sense which can be made precise) proving theorems about your code. Assignments of types to expressions correspond to ( Read more... )

A guy on Reddit pointed me at this article today. It's the Wikipedia biography of the Welsh computer scientist Donald Davies. Like my father, he was from the Rhondda Valley; he was the co-inventor of packet-switched networks (like this big one you're using right now); and he once found a bug in Alan Turing's code, before the first computer had been ( Read more... )

A comparison of the Haskell argmunger with its Arc equivalent (or even its Perl equivalent) should make something clear. It's been claimed that Haskell doesn't need macros, because most of the things that Lispers need macros for can be done in Haskell using lazy evaluation and so on. But the argmunger example makes it clear that there are things ( Read more... )

I'm going to make what should be an uncontroversial statement: if you don't understand and use monads, you are at best a quarter of a Haskell programmer. A corollary of this is that, since using monad transformers is the only (or at least the approved) way to use two or more monads together, if you don't understand and use monad transformers you ( Read more... )

totherme kindly drew my attention to this blog post today. The author, Slava Akhmechet, tries to explain away that horrible feeling of unproductivity and frustration that I know so well from my attempts to use Haskell: his claim is that it's just that my expectations are miscalibrated from using imperative languages. A Haskell solution to a given problem, ( Read more... )

http://arclanguage.org/Read more... )

This afternoon I gratefully took possession of the copy of Iverson's A Programming Language which the library had been holding for me. Within two sentences, he'd managed to say something so thought-provoking that I felt compelled to ( post about it here. )

SICP section 2.4 set off my wheel-reinvention alarms in a big way. It discusses writing code to use complex numbers in a representation-agnostic way; your complex numbers can be either in polar (r, θ) form or rectangular (x + i y) form, and ideally you'd like not to care. Their solution? "Tag" each number with its representation, by passing around ( Read more... )

While trying to do one of the exercises from SICP, I wanted to apply and to a list. Now, I could have used fold, but it seemed a bit of a waste given that Scheme's and is variadic: what I needed was an equivalent of Perl's func(@list_of_args) idiom, or Python and Ruby's func(*list). So, inspired by the syntax for variadic function definitions, I ( Read more... )

I got back from Wales on Tuesday, to find my copy of Structure and Interpretation of Computer Programs (sometimes known as the Wizard book, or SICP, or "sickup", as I've taken to calling it) waiting for me. It's the first-year computer science textbook used at MIT, and early signs are that it's going to be worth its weight in rather good coffee.

( Chapter summary )