Lambda the Ultimate

People should realize that notation is often 'abused' (that's a technical term...) A good tip is not to be terrified by strange and/or unfamiliar notation...

I wrote a couple of tips on reading a formal semantics.

For a long time I tended to skip the formal stuff too readily. It can even be clearer than the prose, if it's using a formalism you're familiar with, anyway. I think the contradiction of formal systems is that they have a higher barrier to entry, but once you know the language they're easier to understand because there are fewer opportunities for ambiguity.

But it's probably better to skip the formal stuff and read the prose than give up entirely. Often there are clues in the prose that can help decode the formal parts, and sometimes they occur after the formal parts. That's one reason it's important to read a paper iteratively ('scuse me, recursively).

Nice link.

Although surely there must be a guide to reading that handout, and a guide to reading that guide and so on. Why keep bashing one's head against a hard paper (looping) when one can recurse to a simple base case? :-)

Feynman also said that he was good at distinguishing between hang-ups that counted and those that didn't. Sometimes a hang-up can be glossed over without missing the real value of the paper. I can't say that I'm particularly good at distinguishing the two, but I try.

My calculus teacher also commented that textbooks are rarely read sequentially, and almost never read from cover to cover. I like to read a paper over once to try to get the big picture. Then, I go back and try to work out the details.

Trying to explain the ideas to others works miracles for your own understanding. Don't get hung up in the abstract or the introduction. Oftentimes I find the introduction makes more sense after I've read the rest of the paper... especially when discussing programming languages and techniques. If I'm somewhat familiar with the language, I almost always head straight to the examples, and then read about the consequences or implementation or whatever.

The most important thing is to be persistent and realize there are no rules, only suggestions.

It seems to me that PL papers use humour (e.g., language games) more often than papers in other fields. This can be quite confusing to newcomers to the field and non-native speakers, but it's worth it, of course...

Categories! The answer is always categories. Right? ;-)

In fact, if you are really struggling with a paper, pause and consider.

Are they really that smart or are the merely really bad authors? Think... have they defined their notation? Are there any examples? Have they been delibrately obtuse to inflate the importance of the result?

Consider laying out $300 dollars for a text book written like this. Would you feel like you made a good purchase, or have you been ripped off?

This is part of why I gave up on physics, I found most of the papers had the difficulty artificially inflated. Once I had puzzled out the deepest mystery of it, I felt totally cheated. I _knew_ I could have rewritten most physics papers in vastly simpler and clearer language.

Maybe the LtU readership should create such a glossary and add it to the FAQ.

I sometimes find myself searching for papers which I want to reread.

Maybe it would be a nice addition for LtU to let people be able to build up a personal DB of papers/topics they want to remember? Would be great if personal notes could also be made...

Ever tried CiteULike ? It's quite good for that purpose.

Ultimately though, a community like a mailing list, IRC, or a website I can ask naive questions of regarding more than just notation is really necessary for me.

Care to share which mailing lists and websites you ask your general programming language theory questions on?
LtU is a great place to discuss current research efforts, be it seems like too many questions would be inappropriate. A lot of times I can't think of the proper forum where I can ask on-topic questions. Here's an example ;-)

What's the difference between static type inference
(like in Haskell) and a latent (tagged) type system (think Scheme) with a real good partial evaluator?
In the type-inference situation, we're using unification to solve a set of constraints. If there's no solution, we give up and say the program was ill-typed. On the other hand, it seems like tag checking code in a latently typed lanugage would be a good candidate to get partially evaluated away at compile time. For example it seems like...

;; typed values are really pairs of values and types
;; e.g. (123 . 'number)
;;      ("abc" . 'string)
(define (isnumber n) (eq? (cdr n) 'number))
(define (add arg1 arg2)
    (if (and (isnumber arg1) (isnumber arg2))
        (machine-add (car arg1) (car arg2))
        (error "not a number")))

(add '(4 . number) '(5 . number))

...should be easily changed into...

(machind-add 4 5)

... And after we're done partially evaluating our source, if we still have left over type-check predicates like 'isnumber' in the code then we again declare that the program is ill-typed. Are the two methods comparable in any way? Are there any papers available discussing this?

Two things have to be in alignment: Knowledgeable people with overlapping interests.

I'm sure there are many Schemers that are interested in Type tagging. And many of the more advanced Schemers are knowledgeable in HM Type Inference. The foundations for type inference in ML is fairly rigorous with a few known tradeoffs. I don't think that the understanding of how to do type inference in Scheme is near as tight.

Will partial reduction be enough to get you to Haskell level type inference? I would doubt it, but then I'm not an expert. Probably get you closer, but will probably end up with some things in Scheme which can not be known until run-time based on the complexity of the code path decisions.

But at the very least, I think it would be quite interesting to see how far such a path at static type checking could lead.

Wouldn't the answer be unequivocally no? In a turing complete language, a static type system that guarantees the absence of type errors must necessarily reject some programs that don't have any errors present.

One can create useful systems that guarantee the presence of the errors they find, but not the absence. One can insert run-time checks when static typing fails to make guarantees. But these systems aren't really comparable to Haskell's type system.

This answer is too easy. I really feel like I'm missing something key here.

Wouldn't the answer be unequivocally no?

I'm assuming the question is 'Is parital evaluation of type checking predicates the same as static typing?' The answer might be no (after all I'm asking a question, not making a statement), but I don't think its that easy of a question to decide. Here's another stab at trying to explain what I'm getting at. Take your program written in a safe, but dynamically typed language. (Again, think of Scheme. We won't allow the language to violate its own abstractions [i.e. 'safe'] and we won't catch these errors until run-time ['dynamic']). Then do an inline expansion of all the primitives in the code. This step will expose the hidden type checking predicates that normally get evaluated at run-time. Now, take the expanded-out program and give it to your partial-evaluator. A 'sufficiently good' partial evaluator should be able to "evaluate away" some of the type-check predicates (our program has now been specialized to work with only those particular types). Finally, take a look the resulting source from the partial evaluator and count the number of type checking predicates still left in the code. Here come the conjectures. If you have zero type-check predicates left, would the program have passed a static type checker? If you have one or more type-check predicates left, would the program have failed a static type checker? (In which case maybe we shouldn't allow the program to be run) And the third option is: does the partial-evaluator halt? (or does it run forever instead of reporting something like an 'occurs check' or an infinite type like a static type checker might).

IMO, that would have been a reasonable question to ask as a new forum topic here, since it's about languages in general, type systems, and partial evaluation, as opposed to being a question about e.g. how to do something in a particular language.

To partially answer the question, there's definitely a close connection between types and partial evaluation. See e.g. the subthread here, which starts with a reference to the paper Types as Abstract Interpretations[*]. Replies to the linked post include a few other links, such as an LL post of mine in which I gave a high-level overview of the connection between types and abstract interpretation.

I agree.

For more standard notation, one can find brief descriptions of the it with google fairly easily. I did this at one point for some logic notation. Also, most "introductory" papers/books/etc. in the area will describe the notation. That said CS/PL papers seem to be some of the worst papers I've read for inventing notation.

With some papers I've found it helpful to type in the functions and play around with them. With the Monadic Subcontinuations paper, I ended up reimplementing the library as described in the paper using GADTs instead of coercion functions, switched it the monads to monad transformers, and abstracted the interface into a typeclass.

I found the typeclass particularly helpful, because it lets you focus on the essential bits.

class Monad m => MonadCC p sk m | m -> p sk where
	newPrompt   :: m (p a)
	pushPrompt  :: p a -> m a -> m a
	withSubCont :: p b -> (sk a b -> m b) -> m a
	pushSubCont :: sk a b -> m a -> m b

I agree fully with John Carter's rules. Here are some more rules that I think are very important (some of them overlap with John's rules):

(1) The pyramid rule. The most important sentence should be the first; the most important paragraph should be the first; the most important section should be the introduction. This should be applied recursively for each paragraph and section.

(2) The give it away rule. Explain your results up front, instead of slowing working up to them. This will let readers use their time and effort efficiently. If the results are interesting, it motivates people to read the whole paper.

(3) The truth rule. Every sentence you say should be an independent truth. It should not be false, supposedly to make it "easier to understand", since it will have the opposite effect: it will only confuse the heck out of a reader trying to really understand what you are saying. True sentences are pillars of stability. [Logic programmers will see that this rule is inspired by good Prolog programming style.]

(4) The simplicity rule. This is the hardest one of all to follow, but the most worthwhile. If you find that your explanation is too complicated, it means that you do not understand the material well enough. If you really understand something well, then you should be able to explain it simply. This holds for *everything*, even things that seem very complicated. The Feynman lectures are a good example of this rule.

Rules (3) and (4) may seem contradictory, but they are not. It just takes a lot of thought to satisfy both at the same time! Needless to say, I think that this effort is really worth it.

(3) The truth rule. Every sentence you say should be an independent truth.

You just have to relax this a little bit if you are going to argue reductio ad absurdum.

Just a little bit. :)

You just have to relax this a little bit if you are going to argue reductio ad absurdum.


There is no need to relax the truth rule. Use constructive logic instead!


;-)

As every statement must be an independent truth, then only axioms can be used as statements. Any proof longer than one statement is forbidden by this "independence" clause, no?

like I said, I think the monadic subcontinuation paper is a good candidate

The first thing to observe is that this is a fairly advanced paper. To have any chance of understanding the paper you need to have understood concepts that pre-suppose that you already know how to read papers. ;-)

But if you think you really want to be able to understand this paper, someday at least, if you can read the title and pick out the references in the intro you are already on your way.

What is a subcontinuation? To understand this you need to find out what a continuation is. The paper kindly offers the Strachey, et al. paper, but you could also use Google or Citeseer or your local university library to find something else.

Once you master continuations (or if you're bold and skip right to subcontinuations) track down some of the papers referenced in the intro regarding subcontinuations, such as the Hieb et al. paper.

Continuations and subcontinuations should keep you busy for a while. ;-)

If you are still keen, the next question is "what is a monad?". Experience with thread here on LtU suggests that finding this answer will also take some time. ;-) The paper is kind enough to point you to relevant Wadler papers, which is a good start.

Once you have all this background, you are probably in a position to understand what good a monadic treatment of subcontinuations will do for you, and you probably know enough to read this paper.

If you run into trouble, reread one of the sources you consulted earlier to see if you can shore up your understanding. If you got this far, you are probably almost there.

If you run into trouble with any of the immediate sub-papers referred to from here, be a good PLT student and use this process recursively. ;-)