4.1 What Is This Assignment’s Purpose?🔗

“Dynamic” or “scripting” languages pose special challenges to classical type systems. Some of these are an artifact of trying to add types to a language that was designed without them and wanting to not reject a large part of the existing codebase. We want you to study one such feature.

One consequence of this accommodation is this. If languages are going to add type systems eventually anyway, perhaps they should be designed with types in the first place?

4.2 Task🔗

In TypeScript 2.0, Microsoft introduced a notion called control flow based type analysis (search for it in the document if the link doesn’t work). There are similar features in Facebook’s Flow checker—hence its name—and in JetBrains’s Kotlin. You can read more about this on the Web.

You can play with TypeScript online. For instance, in this program, you can hover over variables and see the typehints.

As the above TypeScript example shows, TypeScript has union types. These are similar to, but not the same as, algebraic datatypes. In an algebraic datatype, there is a constructor for every variant; and a given variant can only be a part of one type. In a union type, there is no explicit tag (so these are often called “untagged unions”), and one type can be a part of many different unions.

Contrast this with the type-checker we’ve studied in class and that you’ve implemented. Suppose we extended it with union types. Would you then be able to type-check the program above? Why or why not? Please explain your answer using the vocabulary of the class, e.g., in terms of type environments.