The infinite tower of questions; or, what topic for 24 March?

[Adrian King]

So now we've visited the more interesting corners of the lambda cube, and we have a way of talking about what can depend on what in a type.

But this seems to be only one of the knobs you can twiddle when making up a type system. Others might include:

. How do you create new types (other than function types)? Haskell-style datatype declarations, OO-style classes, typeclasses, C structs, refinement types -- where does it all end? What do they have in common? Is there some sort of well-understood taxonomy?

. Is recursion allowed in types? Limited or unlimited? What are the implications?

. Does a compiler have to take typechecking so seriously? What about gradual typing or hybrid typechecking?

And so on.

Are these questions of sufficient interest to anyone else to be worthy of a lecture?

[Adrian King]

Not to mention subtyping in all its manifestations.

[James Koppel]

You forgot ownership types, information-flow security types, the calculus of communicating systems, typestate, types that control complexity, types for controlling stack discipline, energy types, region systems, effect systems, etc. If you can deduce a property about a program, you can write a typesystem for it.

This can be a bit of an arbitrary line, but I'd say that while the axes of the lambda cube are fundamental, most of the concepts listed are not. Exceptions are C structs (which are really just another word for products) and recursive and algebraic datatypes (which do directly correspond to some basic category theory). There does not need to be a fundamental taxonomy for mathematical ways of modeling features of programming languages any more than there needs to be a taxonomy for ways of mathematically modeling the stock market.

--
SF Types, Theorems and Programming Languages
---
You received this message because you are subscribed to the Google Groups "SF-TTPL" group.
To unsubscribe from this group and stop receiving emails from it, send an email to sf-ttpl+u...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

[Adrian King]

I figured there must be something I forget.

It might be just as interesting to know why something isn't fundamental as to know that it is. For example, I have no clue what an energy type is, but I wouldn't mind hearing how you build it out of whatever you build it out of.

[James Koppel]

It's a fuzzy concept. What does it mean for anything in math to be fundamental? One strong indicator though is using the computational trinity, or, as Bob Harper puts it, "Once you understand what something means in type theory, proof theory, and category theory, then you've really discovered something."

Energy types are a great example of something which is really, really not fundamental. They are systems of annotations that help reason about the power consumption of programs and help compilers optimize programs for energy usage. Various approaches have been developed over the past couple years (e.g.:  https://ready.cs.washington.edu/~luisceze/publications/Enerj-pldi2011.pdf ), and it's not clear which, if any, people will still care about in five years.

[Tikhon Jelvis]

We've already talked about the *simplest* example of the "holy trinity", which would be the Curry-Howard-Lambek correspondence. In particular, we can take a look at how the simply typed lambda calculus also corresponds to propositional logic and "closed cartesian categories". I never mentioned this latter term, but it basically works out to having products defined and a terminal element, both of which we covered, and exponentials, which I didn't get around to. So in a rather deep sense, the simply typed lambda calculus *is* natural, because its structure also arises in logic, category theory and set theory.

An analogy to programming would be comparing a run-of-the-mill library for doing something specific compared to an abstraction factored out of a bunch of different use cases. Energy types are like a codec library or something: they're great at doing one thing (modelling energy use or decoding video, respectively), but are not widely applicable and do not give any insights on types or computation in general. On the other hand, an "abstraction" library like lens is applicable in a whole bunch of different places and a whole bunch of different ways and leads to interesting, non-trivial generalizations (like traversals and prisms).

As far as types go, another interesting take are "linear types", which are pretty fundamental, popping up as linear logic and closed monoidal categories. In fact, for an even more general overview, take a look at Baez's famous(ish) "Rosetta Stone" paper[1] which relates all this to physics and topology. It's worth a read even if you, like me, don't understand most of the physics or topology involved.

To me, this is a strong indication that something is "natural": it keeps on popping up all over the place, in seemingly unrelated places. This is also what the "Rosetta Stone" paper tries to get across with the structures it talks about. The "holy trinity" is just a particularly clear criterion for what "popping up all over the place" could mean.

Anyhow, I actually mostly brought up linear types because the "Bay Area Categories and Types" meetup is starting a series of talks about them[2]. I think it sounds pretty interesting and will try to show up if I don't forget.

[1]: http://math.ucr.edu/home/baez/rosetta.pdf
[2]: http://www.meetup.com/Bay-Area-Categories-And-Types/events/161334112/

[Adrian King]

I'd love to make the linear types meetups, but Santa Clara is quite a trek to make on a Friday night (even if it is close to the Caltrain station). I'm hoping they'll have some video, or post some slides. Or would any of us be up to saying something about linear types?

[Adrian King]

Thanks for the lovely mental image of a teeny tiny electric meter attached to every symbol in my program.

[James Koppel]

I know a fair bit about linear logic and linear types, so I could probably prepare a talk. Not on the 24th though -- I have a lot of travel the preceding week.

[Adrian King]

Sounds like a great offer! Six weeks after 24 March is 5 May. Care to give a Cinco de Mayo presentation?

[James Koppel]

Sure!

[Adrian King]

So did anyone make the BACAT linear types meetup in Santa Clara? If so, were there any surprises?

I had thought I might make it after all, but Friday was one of those days when nothing went right.

[Tikhon Jelvis]

I went to the meetup. It was just an overview of the rules for intuitionistic linear logic and how they can be translated to a lambda calculus. You could probably understand much of the main ideas by finding an introduction to linear logic and reading some papers about it (Wadler has a colection[1]).

[1]: http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html

[adriaN kinG]

Tikhon, thanks for the reference. I did read the Taste of Linear Logic introductory paper, but that was as far as it got.

---

Date: Tue, 25 Feb 2014 16:27:03 -0800
Subject: Re: [sf-ttpl] Re: The infinite tower of questions; or, what topic for 24 March?
From: tik...@jelv.is
To: cero...@hotmail.com
CC: sf-...@googlegroups.com; jko...@thielfellowship.org

You received this message because you are subscribed to a topic in the Google Groups "SF-TTPL" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/sf-ttpl/yah9na8j_TQ/unsubscribe.
To unsubscribe from this group and all its topics, send an email to sf-ttpl+u...@googlegroups.com.