Fabulous adventures in coding

We have four kinds of things in Exp: identifiers, function calls, lambdas and lets, and we have four rules in type inference. Finally, the last recursive rule of the type inference algorithm: (iv) If e is let x = e1 … Continue reading →

Last time we gave the base case of our recursive algorithm. Today, two of the three non-base cases. But before we get to them, another annoyance. The first time I read this algorithm carefully I got to the second step … Continue reading →

All right, at long last, the type inference algorithm itself! Algorithm W. W(A, e) = (S, τ) where This is just a reminder that what we’re doing here is taking a set of assumptions that give types to identifiers, and … Continue reading →

All right; we have a deductive system whereby the types of expressions can be justified with derivations. What we want is the ability to take an expression and the typing assumptions of an environment and deduce the type scheme of … Continue reading →

Oh my goodness, I cannot believe it has been twenty years since I got this t-shirt: Happy anniversary Visual Studio, and congratulations to the whole team on VS 2017, and a particular shout-out to my Roslyn friends. I can’t wait … Continue reading →

Summing up the story so far: we have a formal system that allows us to start with the types of identifiers in an environment, and provide a series of deductive steps that ends the type of an expression. This is … Continue reading →

We’ve just seen that we can use our deductive logic system with its rules TAUT, GEN, and so on, to start from knowing nothing, and end with a correct derivation of the type scheme of a complex expression. But here’s … Continue reading →

Over the last two episodes we gave the rules of the deductive system. The paper now gives an example of using that deductive system to derive the type of a complicated expression. The way it is laid out on the … Continue reading →

Happy St. Valentine’s Day all. To solve the Smullyan retrograde chess puzzle posted yesterday, the first question to ask is “is the black king actually in check, or not?” In a great many retro problems the first task is to … Continue reading →

It’s not going to happen in my lifetime! Thus logician, philosopher and puzzle-constructor Raymond Smullyan, who died last week at the age of 97. I started reading Smullyan when I was a teenager; I don’t remember whether I read This … Continue reading →

Last time we discussed the syntax for logical deductions that is common in academia: facts above, deductions below, a line between them. We discussed the tautology rule and the instance rule. Today: more rules. A ⊢ e:σ GEN: ------------ ( … Continue reading →

All right, so far we’ve mostly been talking about jargon and background information. Now we’re actually going to get into the meat of the thing here. What we want is (1) a formal definition of what logical steps we are … Continue reading →

All right, we are getting through section four of this paper. Today: what is an “environment”? Now let Env = Id → V be the domain of environments η. Just to be clear, this is not a function in the … Continue reading →

All right, finally we are getting to typing judgments, which are the bread and butter of type inference algorithms. We said in the previous episode that the values that are manipulated by a program written in Exp are either values … Continue reading →

So far we’ve gotten through the introduction, the grammar of the Exp language, the grammar of the type description language, and what it means to make substitutions in type schemes. For the next few episodes we’ll consider the semantics of … Continue reading →

We take a break from a detailed exegesis of a 40-year-old paper for a brief political message. Freakonomics did a poll to come up with a slogan for this country, and the winner was America: Our Worst Critics Prefer To … Continue reading →

Last time we saw how we can make a substitution for a free variable to produce an instance of a type scheme. This time we’ll look at a much more powerful form of substitution. By contrast a type-scheme σ = … Continue reading →

Last time we learned what is meant by “free” and “bound” variables both in the context of the Exp language and the type scheme language. So, substitutions: If S is a substitution of types for type variables, often written [τ1/α1, … Continue reading →

In this short section the paper gives a somewhat formal definition of what we mean by generic type substitution. You are of course familiar with the basic idea in C#: if you have delegate T MyDelegate<T, U>(T t, List<U> us); … Continue reading →

Last time we defined the grammar of our language “Exp”, which consists of identifiers, lambdas, function application and let expressions. This is a programming language. We also need a different language to formally describe types and “type schemes”. The paper … Continue reading →

Happy new year all, well enough chit chat, more type inference! Recall that we are going through the seminal paper on ML type inference line-by-line and explaining all the jargon and symbols. Last year we got through the introduction. 2 … Continue reading →

From the paper we’re studying: For simplicity, our definitions and results here are formulated for a skeletal language, since their extension to ML is a routine matter. For example recursion is omitted since it can be introduced by simply adding … Continue reading →

Continuing with the question of how to deduce the “type scheme” of letrec map f s = if null s then nil else cons(f(hd s)) (map f (tl s)) Knowing the type schemes of null, nil, and so on. Let’s … Continue reading →

Today, what’s the type of map given the types of its parts? The type checker will deduce a type-scheme for map from existing type-schemes for null, nil, cons, hd and tl; the term type-scheme is appropriate since all these objects … Continue reading →

During my blog hiatus I also did a brief interview with Dot Net Curry magazine, which was a follow-up to their 2013 interview with me. Long-time readers will recognize the puzzle that I pose at the end!

Continuing with my excessively detailed explanation of type inference in ML… After several years of successful use of the language, both in LCF and other research, and in teaching to undergraduates, it has become important to answer these questions — … Continue reading →

Continuing with my excessive explanation of type inference in ML… Here we answer the question in the affirmative, for the purely applicative part of ML. It follows immediately that it is decidable whether a program is well-typed, in contrast with … Continue reading →

The nice people at the New Jersey Institute of Technology asked a dozen people for some extremely brief thoughts on the impactfulness of computer programming in the coming economy, and were kind enough to include me among those dozen. And … Continue reading →

Podcaster Dave Rael was kind enough to invite me to his geek interview podcast show “Developer On Fire” recently; we talk about developer tools and impact and blogging and all kinds of fun stuff. Check it out!

We continue with my excessively detailed explanation of the seminal paper on the ML type inference system… 1 Introduction This paper is concerned with the polymorphic type discipline of ML, which is a general purpose functional programming language, although it … Continue reading →

Well that was a long break! When I was studying for my Facebook interviews I realized that I was going to have no time to write in my blog if I got hired, so I wrote several dozen articles, batched … Continue reading →

> look In the middle this room a small shaft descends into darkness below. Above the shaft is a metal framework to which a heavy iron chain is attached. There are exits to the west and north. A foul odor … Continue reading →

At the east end of this narrow passage, a ladder leads upward. There’s a strong draft from the west, where the passage narrows even further. There is a small pile of coal here. > take the coal Taken. > go … Continue reading →

This is a nondescript part of a coal mine. Someone carrying a large bag is casually leaning against the wall. It is clear that the bag will only be taken over his dead body > examine the thief The thief … Continue reading →

This room smells strongly of coal gas. Narrow tunnels lead east and south. There is a sapphire-encrusted bracelet here. > go east This room of course explodes if the burning torch is brought into it. I note that this game … Continue reading →

In the middle this room a small shaft descends into darkness below. Above the shaft is a metal framework to which a heavy iron chain is attached. There are exits to the west and north. A foul odor can be … Continue reading →

You are in a small room with exits to the east and south. There is an exquisite jade figurine here. In the corner of the ceiling, a large vampire bat is holding his nose. > go east Code for this … Continue reading →

You are at the entrance of an abandoned coal mine. Strange squeaky sounds come from the passage at the north end. You may also escape to the west. > go north Ominous. Code for this episode can be found in … Continue reading →

This small chamber appears to have been part of a coal mine. To the west and south are passages, and a steep metal slide twists downward. > go west Well I guess now we know where the unclimbable steep metal … Continue reading →

This is a crooked corridor from the north, with forks to the southwest and south. > go north If you think the winding passage is deliberately designed to be easily confused with the twisting passage, you’re right! Code for this … Continue reading →

This is a tiny cave with entrances west and north, and a dark, forbidding staircase leading down. > go north If you think the drafty cave is deliberately designed to be easily confused with the windy cave, you’re probably right! … Continue reading →

This is a crooked corridor from the north, with forks to the southwest and south. > go north > go west > go south > go up > put the skull and the emerald in the trophy case crystal skull: … Continue reading →

You are in a square room with tall ceilings. A huge mirror fills the south wall. There are exits east and northeast. > look in the mirror An ugly person stares back at you. > go northeast Hmph. Code for … Continue reading →

You have entered the Land of the Living Dead. Thousands of lost souls can be heard weeping and moaning. In a corner are the remains of previous adventurers less fortunate than yourself. A passage exits to the north. Lying in … Continue reading →

You are outside a large gate inscribed, “Abandon all hope ye who enter here!” The gate is open; beyond you can see a desolation, with a pile of mangled bodies in one corner. Thousands of voices, lamenting some hideous fate, … Continue reading →

This is a tiny cave with entrances west and north, and a dark, forbidding staircase leading down. > wait Time passes… A gust of wind blows out your candles! > go down Code for this episode can be found in … Continue reading →

…in the magic boat You are on a narrow strip of beach between the White Cliffs and the Frigid River. A tiny passage leads west into the cliff. > get out of the boat You are on your own feet … Continue reading →

You are on the Frigid River just below the dam. The river flows quietly here. There is a landing on the west shore. > wait Time passes… The current carries you downstream. The river descends here into a valley. The … Continue reading →

You are at the base of the dam, which looms above you. The river Frigid begins here. Across it, to the east, cliffs form giant walls stretching north-south along the shore. There is a folded pile of plastic here which … Continue reading →

You are in a cavern to the north of what was formerly a lake. However, with the water level lowered, there is merely a shallow stream, easily. A slimy stairway climbs to the north. There is a hand-held air pump … Continue reading →