,
18 tweets,
5 min read
Read on Twitter
I didn't actually *answer* the original question, so let me try to write a few tweets about it here. It really depends on what you're starting with. Some would (very reasonably) argue that you should co-design a language and its type system. »
That would seem to work well if (a) you're designing a language from scratch and (b) you want that language to be typed. However, it's a smart idea to do it *even if you don't want the language to be typed right now, but might in the future*. That's what we did with @PyretLang: »
We asked, "What kind of type system might we someday want for this language", which also included (VERY CRUCIALLY) "What kind of type system do we NOT want for this language", and then designed it around that intended type system. »
Along the way we have diverged from that goal for two reasons: (a) we were inheriting some legacy APIs that we didn't want to break, and (b) we ran into language features that we wanted and didn't fit. But they were *conscious*, and we are always aware of them. »
Meanwhile, much of @PyretLang is very much typable using the Beta type-checker that's built into the IDE. Some of us use it on a regular basis, and several students have used it too. So that's the co-design story: can be done even without implementing the type system! »
But there is another kind of type system design, and this is the *retrofitted* principle. You have an existing language, given to you by your favorite deity (@BrendanEich, say), and you have to fit a type system around it. This is a really interesting exercise. »
In an invited talk I've given several times, I articulated what I called the retrofitted type system design principle: » 
This is a very different exercise. You work through your language's operational semantics. You define (or identify) error states. You figure out which ones you want to catch. And then you devise rules to get you there. »
This is not trivial. In fact, JavaScript is fun to pick on because so many things that would normally be considered errors…aren't. JavaScript is the new C. [I'm liberally pasting slides from my talk, here.] »
Therefore, your type system isn't canonical (it never can be, since you have a choice of what things to make errors, but it's especially bad in JS because there's a combinatorial explosion of choices—you have a choice on each thing in the previous slide.) »
Here you run into patterns of language use. For instance, if you rule out arity mismatch errors completely, you disable the standard JS vararg pattern. Whereas "trailing args with `U Undef` are legal" lets you handle that while catching what we normally consider errors. »
In short, the retrofitted world feels very different from the by-design world. In the latter, you control the operational semantics as well. In the former, you're at the mercy of someone else whose choices you have to deal with. »
Our work on jQuery types is more interestingly in the middle because of course jQuery wasn't designed with types in mind, but it's a far saner "language" to deal with, so retrofitting isn't quite as frustrating. So there's a spectrum. »
HOWEVER, all of this is still very narrow, because we're talking only about "types for catching errors". Type systems have many more uses than that: modular abstraction enforcement, reasoning, etc. Those different uses will lead to other type designs. »
So a *starting* point in your quest should be, "Why am I building a type system?" I purposely avoided this question at the beginning to lull you into complacency, but it really ought to be your first question. Of course there's lots of overlap, but also (subtle) differences. »
In terms of the how, several people have posted about tools [], but the more basic things to think about are: (1) what information do I need in my judgments, and (2) do I have a good reason to not make it syntax-driven. »
Ideally you are syntax-driven and you have a clear sense of what information you have coming in (type environment, what else?) and what you have going out. The "going out", in particular, is important: it's usually "strengthening of the inductive hypothesis" kind of info. »
Once you have thought those things through, then you're in a position to start playing with those tools, experimenting, working towards a soundness proof, etc. The rest is easy, it only takes a few years. <-; Good luck, and hope this helps. •
