Feed fabulous-adventures-in-coding Fabulous adventures in coding

Fabulous adventures in coding

Link https://ericlippert.com/
Feed http://ericlippert.com/feed
Updated 2017-12-16 18:32
Excessive explanation, part twenty-four
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 →
Excessive explanation, part twenty-three
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 →
Excessive explanation, part twenty-two
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 →
Excessive explanation, part twenty-one
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 →
Happy anniversary Visual Studio!
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 →
Excessive explanation, part twenty
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 →
Excessive explanation, part nineteen
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 →
Excessive explanation, part eighteen
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 →
The chess mystery, solved
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 →
Why should I be worried about dying?
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 →
Excessive explanation, part seventeen
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 →
Excessive explanation, part sixteen
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 →
Excessive explanation, part fifteen
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 →
Excessive explanation, part fourteen
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 →
Excessive explanation, part thirteen
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 →
Real Americans
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 →
Excessive explanation, part twelve
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 →
Excessive explanation, part eleven
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 →
Excessive explanation, part ten
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 →
Excessive explanation, part nine
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 →
Excessive explanation, part eight
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 →
Excessive explanation, part seven
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 →
Excessive explanation, part six
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 →
Excessive explanation, part five
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 →
Another spicy interview
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!
Excessive explanation, part four
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 →
Excessive explanation, part three
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 →
Impactfulness
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 →
I’m on fire!
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!
Excessive explanation, part two
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 →
Excessive explanation, part one
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 →
Shaft room, again
> 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 →
Ladder room
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 →
Coal mine
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 →
Gas room
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 →
Shaft room
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 →
Bat room
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 →
Mine entrance
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 →
Slide room
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 →
Winding passage
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 →
Drafty cave
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 →
Twisting passage
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 →
Mirror room
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 →
Hades
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 →
Entrance to Hades
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 →
Windy cave
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 →
White Cliffs Beach
…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 →
Frigid River, in the magic boat
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 →
Dam base
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 →
Reservoir North
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 →
123