Home

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...)

By Manuel J. Simoni at 2012-02-03 15:53 | Teaching & Learning | Type Theory | other blogs | 14615 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Thanks for the plug

Of course, it's all stuff I've picked up from you fine folks (and especially Conor McBride).

I love you guys. :)

By Kalani at Fri, 2012-02-03 16:33 | login or register to post comments

blast from the past!

I read this when it originally came out, it is fantastic. I hope you expand on this a bit further. Let me include my comment from several years ago:

"I have gone through most of TAPL and read quite a lot about functional programming (from a novice’s perspective)…I have NEVER seen this explanation. This is one of the best things I have read in a very long time. Amazing and thanks!"

By shahbaz at Fri, 2012-02-03 18:06 | login or register to post comments

Don't delist me

I'm still a member, but I'm mostly lurking now :)

By Daniel Yokomizo at Fri, 2012-02-03 16:42 | login or register to post comments

Excellent

A really superior presentation of its content. (My own ideas are headed off in a different direction lately —I'm not a huge fan of types [note: for some bizarre reason that link takes me to the bottom of the page instead of the top, I've really no idea why]— but that doesn't at all diminish my appreciation of this presentation, and for my purposes it's great food for thought.)

On the theme of algebraic games with types, it put me in mind of this about container types (which, when I first saw it, led me to muse on logarithms).

By John Shutt at Fri, 2012-02-03 18:52 | login or register to post comments

Great Explanation

This one article took me from not really getting algebraic data types to understanding them completely. The explanation was concise, but understandable. My compliments and gratitude to the author for writing it and LtU for bringing it to my attention.

By Patrick Moran at Tue, 2012-02-07 16:05 | login or register to post comments

Types are obsolete?

There is well known analogy between types and physical units. To extend one of the OP article examples

int+int = 2*int

is analogous to

kg + kg = 2*kg

Now, physical units evolved to dimensionless system (http://arxiv.org/abs/physics/0110060). Does it mean that eventually we'll get rid of types in programming as well?

By Tegiri Nenashi at Tue, 2012-02-07 16:42 | login or register to post comments

Not quite

I think the analogous statement is

kg*kg = kg^2

The points is that multiplying two masses gives something with new dimensions just as building a structure from its fields gives a new type.

Dimensions tell us about symmetries in our physical systems. In particular it tells us about invariances under scaling. Similarly types give us symmetries in our programs, namely those given by the "free theorems".

The fact that you can get rid of dimensions doesn't mean you should. They can play a very helpful role in ensuring the correctness of mathematical derivations. For example at the core of physical simulation code is often a block of code that is dimensionless. I can't tell you how many times I have seen mistakes in such code because the lack of dimensionality makes it hard to notice when someone has done something crazy like add an acceleration to a velocity.

By sigfpe at Tue, 2012-02-07 17:33 | login or register to post comments

Look at Andrew Kennedy's 1997 POPL paper...

Relational Parametricity and Units of Measure for a precise analysis of how the Buckingham pi theorem is connected to parametricity.

By neelk at Wed, 2012-02-08 00:27 | login or register to post comments

dimensional analysis

Re: comment 69190:

The fact that you can get rid of dimensions doesn't mean you should. They can play a very helpful role in ensuring the correctness of mathematical derivations. For example at the core of physical simulation code is often a block of code that is dimensionless. I can't tell you how many times I have seen mistakes in such code because the lack of dimensionality makes it hard to notice when someone has done something crazy like add an acceleration to a velocity.

Street-Fighting Mathematics by Sanjoy Mahajan has a 13-page chapter on dimensional analysis. To convey the flavor of his writing, allow me to lift a quick quote:

Critics of globalization often make the following comparison [25] to prove the excessive power of multinational corporations:

In Nigeria, a relatively economically strong country, the GDP [gross domestic product] is $99 billion. The net worth of Exxon is $119 billion. “When multi-nationals have a net worth higher than the GDP of the country in which they operate, what kind of power relationship are we talking about?” asks Laura Morosini.

Before continuing, explore the following question:

‣ What is the most egregious fault in the comparison between Exxon and Nigeria?

By el-vadimo at Wed, 2012-02-08 14:28 | login or register to post comments

Nice example!By

Nice example!

By coincidence, John Baez just posted an article in which he discusses why you don't want to eliminate dimensions even though you can. Much the same argument applies to types.

By sigfpe at Fri, 2012-02-10 17:55 | login or register to post comments

A footnote

In John Baez article dimensional analysis is just a footnote. More convincing is wikipedia entry. Somewhere towards the end of the page I learned that mass,length and time based dimensional system is too limited, as the art can be elevated with inventive use of additional dimensions (e.g. more than one spatial dimension). This idea strengthens the analogy between dimensions and types so I admit -- there is more to dimensional analysis than reduction to unitless system.

By Tegiri Nenashi at Wed, 2012-02-15 00:19 | login or register to post comments