ek

Microcosmographia Academica http://www.cs.kent.ac.uk/people/staff/iau/cornford/cornford....

It's not quite a blog post, but it's as close as one might have come in 1908.

I also like a whole host of articles from Matt Might's blog. I think my favorites are

12 resolutions for grad students

http://matt.might.net/articles/grad-student-resolutions/

and Responding to peer review

http://matt.might.net/articles/peer-review-rebuttals/

One last essay that I have enjoyed, also too old to be a blog post, is W.M. Turski's "I was a computer". It's here on Elsevier but fortunately it looks to be open access.

https://www.sciencedirect.com/science/article/pii/0167642395...

Unfortunately this contribution is inhibited from being significant in value by the fact that TypeScript doesn't support full gradual typing [0] and has an intentionally unsound type system [1].

[0] http://siek.blogspot.com/2012/10/is-typescript-gradually-typ...

[1] https://typescript.codeplex.com/discussions/428572

Are you saying that you think perfect pitch and absolute pitch are different things? They are synonyms, cf. Wikipedia: https://en.wikipedia.org/wiki/Absolute_pitch .

If you're saying that perfect pitch and relative pitch are different things in that it isn't as if perfect pitch is better than relative pitch, then yeah, I absolutely agree. The hacks that I mentioned involve perfect pitch specifically, but transcription ability like you mention is probably tied most to one's sense of relative pitch, even if one has perfect pitch.

You refer to perfect pitch and absolute pitch like they're different things -- do you realize that they're the same thing?

My brother and I are both musicians with perfect pitch, and we've found it useful in a variety of circumstances. To name a couple, it really helps if you're jamming and want to pick up a progression quickly, or if you're DJing and want to key match. I will concede that Traktor recently got key detection, which is nice, but especially when playing live I find that key segues will pop into my head without having to search for the next song in the right key.

Even the best relative pitch cannot help you exactly memorize a melody -- if you are unable to remember what note it actually starts on, you haven't remembered it fully.

Does it seem like cultural commentary has also improved in the last 50 years? I am young enough to not remember what it may have been like when Asimov wrote originally, but it strikes me that Vice is a relatively contemporary sort of a thing.

I would be interested in similar pieces from 50 years ago, looking back on 1914's view of 1964. So much has changed since then, though, and it seems like more has changed since 1964 than changed from 1914 to 1964. In particular, the 60s happened, but even after that, the Internet seems to have effected a fairly massive and seemingly permanent cultural shift. It might be too early to tell, but even the fact that someone posted this commentary, we all read it instantly, and then now we're discussing it here only hours later seems worlds away from the climate of 1964.

> Think of me as an MSR guy publishing a paper, it’s just on my blog instead appearing in PLDI proceedings. I’m simply not talented enough to get such papers accepted.

I wonder if someone at MSR would be interested in taking up the cause and publishing with Joe. It does seem like this work might contain the makings of a great PLDI paper.

Ah, yes. Somehow I was fortunate enough to skip over that. My first couple of Macs that I remember getting second- or third-hand as a kid were a Performa 640CD DOS Compatible which was actually not bad at all, and had the interesting property of containing within it a 486 on a daughtercard, and then later a Power Mac 7200, which wasn't great, though at least had PCI and managed to avoid the Road Apple designation from LowEndMac.

We got into Feed The Beast, a curated collection of modpacks for Minecraft, this year. Played a whole lot of that.

I've been playing the Hearthstone beta with a few friends for a couple months now and it is absurdly fun. Also played a bunch of StarCraft II and Diablo III as usual.

Skyrim and Fallout: New Vegas have held up well. Papers, Please was just fantastic. I had fun playing CounterStrike: GO with friends.

I played SimCity and liked it, though in the midst of the fallout and server issues, I found Tropico 4 and Anno 2070 to be fantastic alternatives.

On Black Friday I picked up a PS3 and have finally been getting into The Last of Us, which is stunning, and Red Dead Redemption, which I think will take longer to get into.

I want to lastly point out that we've had a lot of fun doing LANs with some classics that we've been playing for years now: CS: Source, Rise of Nations, Age of Empires II.

The tech report version of the OOPSLA paper Joe mentions, about a type system for side effect understanding, is here: https://research.microsoft.com/apps/pubs/default.aspx?id=170...

Not only that, but seL4 [0] is a cool NICTA effort that's been ongoing for almost a decade now to produce a secure, machine-verified microkernel based on L4. It seems like there's lots of room for L4 and its children to occupy interesting spaces in OS design.

[0] http://ssrg.nicta.com.au/projects/seL4/

I wonder what the really ancient Mac he links to was. The link is broken since Apple has since drastically redesigned their support site at least once.

I found this article really interesting. I started using Facebook in high school, back when high schoolers were to use hs.facebook.com to access Facebook and networks were heavily emphasized. I left Facebook about one year ago today.

One particular observation that the article makes that I want to flesh out a bit is the following: Facebook has grown and grown in terms of the size of the application itself, and it is clear that they have pushed very heavily for the 'platform' model. It seems like this is getting replaced by a series of more specialized, more mobile-centric social applications, like Snapchat and Tumblr. Of course FB owns Instagram so they have that going for them, but this does seem to hint at a bit of a growing trend in social networking.

Your understanding of univalence seems essentially correct to me.

At this point we are mostly debating what "can use" means -- it's probably enough to say that unless you reframe your thinking, perhaps radically, probably it will be hard for you to be able to use HoTT to get work done. It is possible to do classical mathematics within HoTT, in the normal way, but it would not be very fun.

Yes :) My interest in homotopy type theory is only auxiliary to my research. Designing dependent type systems in a way that balances tractability with expressiveness is a pretty hard thing to do. SMT solvers are nice because you can treat them as oracles and "see what happens". I'm not an expert on decision procedures, and I'd characterize myself more as a user of solvers than a developer of them, though of course once you get deep enough in, that line blurs.

Note that fmap writes: "Equality of rational numbers is decidable, which means that classical reasoning is provable. And yes, even if it wasn't, it would still work."

What is meant by "even if it wasn't, it would still work" goes back to something he said earlier: type theory embeds an infinite hierarchy of axioms of choice and laws of excluded middles. If you want to do propositional-like reasoning in homotopy type theory, you can assume AC or LEM for homotopy (-1)-types, corresponding to propositional logic.

In type theory you are encouraged to drop the law of the excluded middle and the axiom of choice, because of the fact that doing so gives you potentially more expressive ways of doing things as we have said, but you have gotten the impression that you have to, which you don't.

Also, the claim in this thread was that the results from classical mathematics are provable using homotopy type theory, not that they are provable in the same way (though that holds as well, as I've said above; it's just that the mathematics might not look as clean as if you did it in a more idiomatic way). This kind of a value proposition is not exactly new: category theory loses certain axioms over set theory and mathematicians adapted to the point that category theory is now the language of modern algebra.

I want to point out that I suggested that you read the introduction to the book because it provides these same answers to the questions you are wondering about. I still suggest you do so, as it goes into more detail on what we have said here in a way that I am not able to quite as well.

To be clear, constructive mathematics are new to me as well. The section in the introduction titled "Constructivity" may help you -- it is about trying to come to grips with the constructive nature of type theory. The short answer is that much of the mathematics that we might want to do does not require the law of the excluded middle or the axiom of choice at all when approached from a type-theoretic point of view. Higher inductive types eliminate the reliance classical logic will frequently have on either of these. To quote an example from this section, "In set-theoretic foundations, the statement 'every fully faithful and essentially surjective functor is an equivalence of categories' is equivalent to the axiom of choice. But with the univalence axiom, it is just true; see Chapter 9."

The emphasis that you are placing on the fact that type theory happens to be a constructive logic is perhaps causing you to miss the point. Homotopy type theory is not about advocating constructivism. The "big idea" is that HoTT is a foundation that computers can already reason about easily, based on the work that has already been invested into developing sufficiently powerful dependently typed languages (Coq, Agda). Because it is possible to formulate set theory, category theory, and even real numbers (all discussed in part 2 of the book) within the framework of homotopy type theory, it should be possible to extend these formulations to encompass more and more results from the rest of the mathematics. Because HoTT has already been shown to be implementable (in the form of a library for Coq), this means that any math that is done informally under homotopy type theory can be carried directly into a formal, machine-checkable series of theorems and proofs, in the form of a Coq development.

To expect this material to be readable and useful to every average Joe right away is asking far too much of any new idea in mathematics. This is cutting edge research, and there is still too much even the people closest to this material don't understand yet. As another comment on yours alluded to, at one time your equivalent in the 1700s would have written off calculus as indecipherable and judged it not likely to succeed as a result.

Your criticism of the book does not appear to be constructive, meaningful, or well-founded. Rather than saying "this sux, wow" and then listing your credentials, it might help if you gave some idea of what complaints you actually have with the work. While calling someone else's work "gibberish" is a low enough blow that I'm not sure it warrants further discussion, I want to at least make a couple of specific points on what you have said:

1. Despite your claim that you are not versed in type theory, chapter 1 provides what I find, as a 21 year old graduate student in programming languages with a relatively standard undergraduate background in mathematics and then some, to be a clear and helpful explanation of Martin-Löf type theory, and a good exposition of background needed for chapter 2. Did you read it?

2. This book makes extremely clear that the "homotopy theory" that is developed towards the exposition of homotopy type theory is merely synthetic, which is to say that it considers homotopies as first class objects, rather than deriving them from their traditional topological underpinnings in a more analytic way. It might be useful to have a little understanding of point-set topology with maybe a little inkling of what's going on in algebraic topology to figure this out, but certainly it doesn't seem absolutely necessary, since the book's notion of homotopy is built from first principles. Are there specific points in chapter 2 that you find confusing?

3. It appears you have a doctorate in CS, specifically to do with interactive theorem proving. Almost every proof assistant I have come across either uses dependent types or higher-order logic, and it seems like in order to have earned a PhD in interactive theorem proving you might have had to have become familiar with at least one of these formalisms. Given that you should be comfortable in one of these domains, it doesn't seem like the material in the book is a huge leap. Could you speak a little bit more to what you worked on grad school?

I don't mean to come across as harsh, but your claim that this book excludes 99% of its target population seems false; at the very least I do not consider myself in the top 1% of people who might hope to consume this book.

Thanks! I tried to answer it.

Technically Coq is not a fully automated automated prover, but leaving that aside:

We are definitely not even close. But getting mathematicians acquainted with HoTT is a good first step, I think. The book itself presents formulations of homotopy theory, set theory, category theory, and a constructive view of the real numbers, all within homotopy type theory, and on top of all this we could likely start building up a corpus of more results from topology, algebra, and analysis.

It seems like I end up plugging the book really frequently here, but it's for good reason -- it's exceptionally readable AND it's accompanied by a full Coq development. That is, you can do basically every exercise in the book, directly in Coq, if you want.

You can definitely just read the material and then come back and try the exercises in Coq later, or more tightly couple the two. I think either approach would work well, and it's up to personal preference.

The first chapter of HoTT is an introduction to Martin-Löf that I personally find quite intuitive, to the point that I'd say it's clear than most other expositions of the same material that I've tried to read.

It will be easier to understand dependent type theory if you're programmed in a dependently typed language, but I wouldn't say it's strictly necessary to understand dependent types theoretically. I have just a little bit of Coq experience and found myself comfortable with the HoTT presentation of dependent types.

The book on Homotopy Type Theory is quite readable even though the developments are quite new. The purpose of the book is to get the material into the hands of as many as it may be useful to as soon as possible.

I would argue that the book is at least as useful as Categories for the Working Mathematician or Barendregt's Lambda Calculus are likely to be for your typical software engineer interested in functional programming. To be clear, someone interested only in learning how to program in functional languages is probably not going to get very much from either of those books, which are respectively an extremely technical mathematical text on topics in category theory, and a heavily logic-oriented, mathematical presentation of the lambda calculus and derivatives thereof. Not much of the material in either book would be directly applicable to the practice of software engineering using functional languages, but someone with a deeper interest would find them useful and interesting, and I think the same holds for the HoTT book. At the very least, as the other commenter alluded to, a novice reader would probably be able to glean a nice understanding of Martin-Löf dependent type theory from the first chapter.

Great list!

A lot of the stuff there is to know about functional programming is still only contained in academic papers, and indeed many of these listed books are texts in programming languages that cite a great deal of the important literature. There is much about programming languages and functional programming that one might read interspersed with these books. Other than following references in the backs of many of these books, the Haskell wiki is a good place for starting to dig into literature on functional programming, as many articles link to important and interesting papers.

On that note it's a bit strange not to see a few books on semantics, such as Transitions and Trees or Semantics Engineering with PLT Redex, listed among books like TAPL and Barendregt's Lambda Calculus. Especially now that DSL design is something many programmers are dabbling in, it makes sense to gain some background on operational semantics. I'd recommend either of these books to anyone working on DSLs, especially in a functional language.

Finally, it might be worth adding Homotopy Type Theory to your list, especially since the list already contains several good books about Coq as well as works about type theory and type systems.

1/10; I'm terrible at this.

Consider not polluting your users' browser history.

As I answered above to another commenter with a similar question, JavaScript is a dynamically typed language and representing dynamic values in a statically typed language requires a bit of thinking, and unions are a common way of doing this.

Yes. JavaScript has dynamic types, and representing these in a statically typed language requires some finagling.

A couple years ago for a programming languages course, we wrote a bytecode compiler and interpreter for a JavaScript-like language we were using in the class (objects, prototype-based inheritance, higher-order functions, etc), and we initially started building it in Go, but the biggest thing that made us switch to C++ at that time was the fact that Go didn't have a straightforward union type.

It looks like this interpreter is using tagged unions for values, and using the empty interface to emulate a union type. I seem to remember that we may have read something at the time that recommended using the empty interface instead of unions, though I don't remember for sure. Nice to see some interpretation efforts finally being realized in Go!

I am pleased that Microsoft has a list called "hardware junkies" :). I'd definitely be on it if I were there.

Nice to know they agree with the rest of us that Samsung is the way to go nowadays, too.