Reading Scalaz API Functions (Principles 5, Scalaz Files)

The Scalaz API has a large number of functions, most of which have several things in common:

1. They have type parameters.
2. Their implementations are very short, typically one line.
3. They do not have Scaladoc.

While they don’t have Scaladoc, their types are printed in the Scaladoc pages. However, with some practice, you can get a quick, accurate understanding of each function by taking into account two things:

1. One of the goals of the Scalazzi Safe Scala Subset is that “Types Are Documentation”. For example, one of the rules is “no side-effects”. Side effects, by their nature, do not appear in type signatures of methods that create them; by banishing them, we eliminate that source of untyped program behavior.
2. Heavy use of type parameters, and minimization of concrete information in each type signature, amplifies parametricity. For Scalaz API functions, there are far fewer factors to consider when working out what a type “means” than you must consider when reading typical Scala libraries.

Adding Scaladoc may be valuable to many users. However, with these factors, the value is greatly diminished, and it’s difficult to justify the development cost of comprehensive Scaladoc when we are already encouraging users to think in terms of “Types Are Documentation”.

That doesn’t mean there aren’t some simple “tricks” and rules-of-thumb that you can learn to accelerate this process.

Values of a type variable cannot arise from thin air.

Suppose that a function has a type variable B, and this type variable is used in the return type, which might be something like (List[Int], List[B]). There is no way for the function to make up its own Bs, so all Bs appearing in that list must have come from the arguments. If there were no Bs in the arguments, then that List[B] must be empty.

This rule, “must come from the arguments”, is significantly more flexible than it sounds, while allowing the caller to preserve data integrity in a type-checked way. For example, the signature def m[A, B](xs: List[A], f: A => B): List[B] does not require the result list to be empty, because the arguments supply a “way to get Bs”:

1. Take any element from the xs list.
2. Call f on that element.

Since the body of m has no other source of As than xs, it’s a fact of the return value that “all elements must have come from calling f on elements of xs”.

In this way, you can use a type signature to read the “flow” of data from its source in the arguments, through other arguments, to its destination in the result. When you get used to this, all sorts of useful corollaries naturally arise. For example, the above fact means also “if xs is empty, then the result list must be empty”.

If you don’t know anything about it, you can’t look at it.

Within the body of def m[A, B](xs: List[A], f: A => B): List[B], there is exactly one special operation available for values of type A—they can be converted to B via calling f—and there are none for values of type B. You can’t compare them, so you can’t sort either the input list or the output list. You can’t take their hash code. You can’t add two As together to get a combined A, and the same goes for Bs. You could do something polymorphic like put an A and B in an (A, B) tuple, but that tells you nothing about those values.

In Scalazzi-safe programming, we supply information about types via typeclasses. For example, if we declared A: Order, there’s a way to compare As. If we declared B: Semigroup, there’s a way to append Bs. When thinking about what a typeclass constraint means for the “flow of data” in a function, you can think of a typeclass constraint as supplying the primitives of that typeclass as extra arguments to the function. (That is, after all, how Scala implements typeclass constraints.) For example, A: Order means that there’s an extra argument (A, A) => Ordering, where Ordering is the usual three-valued result of comparison, and the function is guaranteed to follow some special properties (the laws of the typeclass). B: Semigroup means that there’s an extra argument (B, B) => B, also guaranteed to follow its own special properties.

Naturally, if there are no typeclass constraints on a type variable, no such extra arguments are supplied; only the “ordinary” arguments provide capabilities for working with the type. Surprisingly, for all that is made of the importance of Scalaz’s typeclasses, this is by far the most common case.

You can’t “just crash”.

Consider the type signature def lp[L, R](i: L, s: L => Either[L, R]): R. The flow of data says that the result must have come from s returning a Right, and that s call’s argument must be either i, or a Left from a prior call to s. Moreover, you can safely expect lp to use the L produced by s each time after the first, rather than trying i or another previous L again; in functional programming, it would be absurd to try s(i) again and expect that it might return a Right, when you already know it previously returned a Left.

In particular, there’s no allowance for “timing out” or “duplicate L detection”. Timing out (in terms of a maximum number of s calls) would require a different return type, like Option[R]. Duplicate detection would require a constraint like L: Equal at minimum.

“It’s impossible to implement this signature” is not a reason to “implement” it by crashing; it’s a reason to not have a function with that signature at all. Writing correct type signatures is part of writing a correct type-safe program. When type signatures are only declared for functions that are possible to implement, and reading those type signatures can tell you what they are honestly doing, they start to become true machine-checked documentation.

The utilities of each typeclass are bound by the basics of that typeclass.

Many of the most useful functions in the Scalaz API are defined as typeclass utilities, so they can be most easily understood by keeping in mind those basics as you read the utility functions. So utilities in Functor must have been gotten by mapping, utilities in Foldable must have been gotten by folding, and so on.

For example, consider the utility under typeclass Functor[F[_]], def void[A](fa: F[A]): F[Unit]. What does this function do? If you guess based on its name void, or a poor analogy like “F is some kind of collection” (a common mistake when first approaching Functor), you might conclude something like “it must return an empty F” or “it must return an F with a single Unit in it”. Unfortunately, these “intuitive” answers are not only wrong, they don’t make sense.

Instead, think about void like this: def void[F[_]: Functor, A](fa: F[A]): F[Unit]. Just as with the Order and Semigroup constraints described above, that constraint manifests as its primitives; in this case, “a map function for Fs”. That leaves only one possibility, which happens to be the true behavior of void: the result is gotten by calling map on fa, with _ => () as the function argument.

Practice on the simple cases.

The above are a lot of words to describe a thinking process that is very fast in practice. With practice, it’s much faster to understand what a function does by reading its type than by reading a documentation comment. At the very least, a documentation comment should only be considered as secondary advice to the primary source, the type.

The functions that are easiest to understand purely with types are, unfortunately, the most likely to be fully documented. That makes relying solely on documentation comments more tempting, but this is a mistake as a Scalaz newcomer. If you practice reading only the types for simple functions like void, you’ll gain important practice for quickly understanding much more complex functions using the same techniques.

Global typeclass coherence (Principles 3, Scalaz Files)

In Scalaz, we provide at most one typeclass instance per type throughout your whole program, and we expect users to preserve that invariant. For that type, there should be no way to get two incompatible instances. This is global coherence, and is required to make Scala programs using implicits for typeclasses understandable and maintainable.

If you want a different instance for the “same” type when working with Scalaz, the answer is always to start with a different type first. Then you can define your incompatible instance for the same structure, but on the different type, preserving coherence. Scalaz’s @@ type tags or the underlying existential newtype mechanism are convenient, flexible ways to get these “different” types.

It’s not surprising that “new type” as a solution to this problem comes from Haskell, as Haskell too depends on global coherence. While we can’t get all the benefits from coherence that Haskell does, what remain is sufficient to justify this seemingly non-modular rule.

The invisible action of implicits in Scala is a serious problem for understanding and maintenance if used in an undisciplined manner. Consider, for example, an incoherent implicit-based design: scala-library’s ExecutionContext.

At any point in the program, the ExecutionContext resolved depends on what variables are in scope. It’s unsafe to move any code that depends on ExecutionContext to some other method, because that set of variables can change, thus changing the behavior of the program. And you can’t determine at a glance whether some code depends on ExecutionContext, so moving any code carries some risk.

You can’t add an ec: ExecutionContext argument anywhere without potentially breaking working code, because it changes that set of variables. It’s only safe to introduce brand-new methods with that argument.

If you are refactoring and suddenly get an error about multiple conflicting ExecutionContexts in scope, you have no help to determine which is the “right” one; you have to figure it out based on the probable intent of the code originally was. Possibly, none of the options in scope is right.

By contrast, consider Monoid[List[N]], where N might be some type variable in scope. The correct instance depends on the type, not what variables are in scope. So you can add a Semigroup[N] constraint and know the answer won’t change. You can split up the method, or move any of its code anywhere else, and know the answer won’t change. You can even add a Monoid[List[N]] argument to your function, because you know the caller is required to come up with the same instance you were working with before.

You can add or delete constraints as required, because they’re always going to be fulfilled by the same instances. For example, Scalaz’s sorted map K ==>> V doesn’t carry the K comparator around, because we can assume it always depends on K and only on K.

If you ever get an error about multiple conflicting instances, you know there’s always a workable solution: choose one, because they’re the same.

Tools try to help with understanding Scala’s implicit resolution, but they don’t always work. Global coherence is your greatest ally when trying to understand what an implicit resolution is doing by hand: you know that any path to the instance you find is a correct one, and you can then work out why that isn’t being resolved.

Global coherence also lets Scalaz offer a much simpler API. For example, the efficient union of sorted maps requires that the ordering of K used for both is equal. With “local” (read: incoherent) instances, the only safe way to do this is to define a singleton type depending on the ordering, and treat this singleton type as a sort of third type parameter to the map type. If you happen to have built two maps with the same key type where you didn’t use polymorphism to unify their use of that singleton type, too bad, you can’t safely union them. With global coherence, because the instance only depends on K, the simple two-parameter map type is perfectly sufficient, and those maps are easy to union.

The “flexibility” of local instances is not worth it given the constraints of Scala, and Scalaz assumes you won’t be using them when you use its functionality. Define a newtype instead.

Scalazzi safe Scala subset (Principles 2, Scalaz Files)

Scalaz is designed for programmers building type-safe, functional programs. If you program like this, you can start to see very deep properties of your functions by only reading their types; in other words, types become documentation. This also lets you see how you can combine your functions in more ways, with greater confidence that the combination will actually make sense.

But Scala, the language, contains many unsafe features that get in the way of this method of thinking about your programs. “Scalazzi” means that you are avoiding or banning these features from your Scala codebase, thus restoring your ability to use types to discover those properties.

1. null
2. exceptions
3. Type-casing (isInstanceOf)
4. Type-casting (asInstanceOf)
5. Side-effects
6. equals/toString/hashCode
7. notify/wait
8. classOf/.getClass
9. General recursion

Here’s an example of how you might use these rules to reduce your testing requirements.

Suppose that you have this very simple function to return the greater Int.

def maximum(x: Int, y: Int): Int = if (x >= y) x else y

(I encourage you to imagine that this is harder than this example; after all, aren’t your own programs more complicated?) This type signature says that any Int can be returned; we must test to verify that this isn’t happening.

Instead of writing a test, we can use parametricity to check that either x or y is returned, but nothing else, at compile time instead of test time.

def maximum[N <: Int](x: N, y: N): N = // • • •

I can read from this type that only x or y can be returned. With some practice, you’ll start to see more complex facts arising from types as well.

Unfortunately, Scala has many “features” that let you break this safety. These features aren’t useful for type-safe functional programs, so we simply declare them verboten.

Scalaz expects you to follow Scalazzi rules, but is also packed with features to help you follow them. For example, if you are calling map on a List and feel like your lambda needs to perform some side effect, it’s time to look into Scalaz’s Traverse typeclass.

A standard library for principled functional programming in Scala (Principles 1, Scalaz Files)

The best way to think about “what is Scalaz?” is as a standard library for functional programming. This goes all the way back to its creation: the Scalaz project started because there are not enough facilities in Scala's standard library for convenient, everyday functional programming, without cheating.

How should this affect your approach to the library? Like a standard library, you learn the bits and pieces you need, not the whole thing. There is no must-read book, no must-watch tutorial video, no must-attend course. Scalaz can be used successfully from day 1 as a new Scala programmer; as you do not learn every part of the standard library before starting to use a language, so it goes for Scalaz as well. All that is required of you is the desire to solve programming problems in type-safe, functional ways, and the curiosity to learn about what components that others have discovered and how they might be useful. After all, most pieces of Scalaz were added to it because somebody was solving a problem, and found a solution they thought others might consider useful and well-thought-out.

Scala FP: how good an idea now?

Ed Kmett’s reddit comment full of biting commentary on the troubles of attempting functional programming in Scala remains the most concise listing of such problems, and remains mostly up-to-date over four years after it was written. It covers problems from the now famous to the less well known. It’s still a useful guide to what needs to change for Scala to be a great functional programming language, or conversely, why a functional programmer might want to avoid Scala.

But not everything is the same as when it was written. Some things have gotten better. Some can even be eliminated from the list safely. Some haven’t changed at all.

I’d like to go through each of Kmett’s bullet points, one by one, and elaborate on what has happened in the ensuing four years since he posted this comment.

Types

[1:] If you take any two of the random extensions that have been thrown into scala and try to use them together, they typically don't play nice. e.g. Implicits and subtyping don't play nice together.

This hasn’t really changed. Paul Phillips’s age-old “contrarivariance” thread about the specific example Kmett uses here might as well have been written yesterday.

On a positive note, what is good hasn’t really changed, either. The type soundness of new features still cannot be justified merely because you can’t think of any ways programs would go wrong were your idea implemented; you still need positive evidence that your idea preserves soundness. This is more than can be said for, say, TypeScript.

On the other hand, we’ve seen a lot of attempts to “solve” these kinds of feature-compositionality problems by claims like “we don’t want you to write that kind of code in Scala”. New features like AnyVal subclasses are still made with the concerns of ill-typed, imperative programming placed above the concerns of well-typed, functional programming. Proposals like ADT syntax are likely to support only those GADT features deemed interesting for implementing the standard library, rather than what application programs might find useful.

[2:] Type inference works right up until you write anything that needs it. If you go to write any sort of tricky recursive function, you know, where inference would be useful, then it stops working.

Still 100% true.

[3:] Due to type erasure, its easy to refine a type in a case expression / pattern match to get something that is a lie.

I’m not sure why Ed wrote “due to type erasure” here, but the underlying problems are there. This comment came after the introduction of “virtpatmat”, which improved things in a lot of ways, not least with the improved support for GADTs. I’ve noticed some things get better for GADTs in 2.12, too.

But there are numerous unsound things you can do with pattern matching, some accompanied by compiler warnings, some not. Most of these are due to its reliance on Object#equals. Paul Phillips wrote several bug reports a long time ago about these, and one of the major ones is fixed: the type consequences of pattern matching used to think that Object#equals returning true implied that the two values were perfect substitutes for each other. For example, you could use an empty Buffer[A] and an empty Buffer[B] to derive A = B, even when they’re completely incompatible types.

This has been fixed, but the very similar problem with matching constants has not. I suspect that it will never be fixed unless pattern matching’s use of equals is removed entirely.

[4:] Free theorems aren't.

In the base Scala language, nothing has changed here. But we’ve tried to account for this shortcoming with practice. I wrote an article elaborating on the free theorems problem in Scala; surprise surprise, Object#equals makes another villainous appearance. Tony Morris popularized the “Scalazzi safe Scala subset” through his “Parametricity: Types are Documentation” talk, and since then “Scalazzi” has become the shorthand for this style of Scala programming. (If you’ve heard “Scalazzi” before, this is what it’s about: free theorems.) Tools like Wartremover have arisen to mechanically enforce parts of the Scalazzi rules (among other rules), and they’re well worth using.

So the situation in the Scala language hasn’t changed at all. The situation in Scala practice has gotten better, as long as you’re aware of it and compensating in your projects with tools like Wartremover.

Collections and covariant things

[5:] Since you can pass any dictionary anywhere to any implicit you can't rely on the canonicity of anything. If you make a Map or Set using an ordering, you can't be sure you'll get the same ordering back when you come to do a lookup later. This means you can't safely do hedge unions/merges in their containers. It also means that much of scalaz is lying to itself and hoping you'll pass back the same dictionary every time.

I don’t want to cover this in detail, because Ed’s already gone into it in his talk “Typeclasses vs the world”. I’ve also written about Scalaz’s “lying to itself” approach (a fair characterization), and why we think it’s the best possible choice for Scalaz users in Scala as it’s defined today.

You can think of this as the “coherence vs local instances” argument, too, and Ed is describing here how Scala fails as a substrate for the coherence approach. But he’s not saying that, as a result, coherence is the wrong choice. Since we think that, despite the potential for error, coherence is still the best choice for a Scala library, that should tell you what we think about the alternative: that with local instances, the potential for error is still greater.

So for us, the important question is, what has changed in Scala? There’s been a “coherence” proposal, but its purpose is not to force you to define only coherent instances, nor even to detect when you have not; instead, it’s to let you assert to the compiler that you’ve preserved coherence, whether you have or not; if you’re wrong, scalac simply makes wrong decisions, silently.

This would be very useful for performance, and I will embrace it for all typeclasses if implemented. It will make many implicit priority hacks unnecessary. But it wouldn’t address Ed’s concern at all.

[6:] The container types they do have have weird ad hoc overloadings. e.g. Map is treated as an iterable container of pairs, but this means you can't write code that is parametric in the Traversable container type that can do anything sensible. It is one of those solutions that seems like it might be a nice idea unless you've had experience programming with more principled classes like Foldable/Traversable.

The design of the current collections library is the one Kmett was talking about, so nothing has changed in released code. As for the future collections library, known as “collections-strawman”? The situation is the same.

[7:] You wind up with code that looks like myMap.map(...).toMap all over the place due to CanBuildFrom inference woes.

I’m not sure what Kmett is referring to here, because I’ve been relying on the correct behavior for a long time, that is, without the trailing .toMap. The only thing I can think of would be the function being passed to map returning something implicitly convertible to two-tuple instead of a proper two-tuple, which would require an extra step to force that conversion to be applied.

Monads and higher kinds

[8:] Monads have to pay for an extra map at the end of any comprehension, because of the way the for { } sugar works.

This hasn’t changed at all, but is worth some elaboration. This behavior makes it so you can’t write “tail-recursive” monadic functions in the obvious way. As Dan Doel demonstrated, this can turn a purely right-associated bind chain, i.e. one that can be interpreted tail-recursively, into a repeatedly broken chain with arbitrary left-binds injected into it, thus either crashing the stack or requiring useless extra frames to be repeatedly shoved onto the heap.

This is kind of silly, and could be ameliorated if for wasn’t trying to be non-monadic. But that’s not going to change.

[9:] You have type lambdas. Yay, right? But now you can't just talk about Functor (StateT s IO). Its Functor[({type F[X] = StateT[S,IO,X]})#F], and you have to hand plumb it to something like return, because it basically can't infer any of that, once you start dealing with transformers ever. The instance isn't directly in scope. 12.pure[({type F[X] = StateT[S,IO,X]})#F] isn't terribly concise. It can't figure out it should use the inference rule to define the implicit for StateT[S,M,_] from the one for M[_] because of the increased flexibility that nobody uses.

This is probably the best story of the bunch, and possibly the most well-known of the whole series. This is good for Scala marketing, but probably not best for the future of Scala FP…

We first got the kind-projector to help us write these type lambdas more succinctly. So Kmett’s first example above can now be written Functor[StateT[S, IO, ?]]. Not as nice as the curried Haskell form, but much better.

Eventually, though, Miles Sabin implemented the “higher-order unification” feature, often called the “SI-2712 fix” after the infamous bug. This feature performs the inference Kmett describes above, and gets away with it precisely because it ignores “increased flexibility that nobody uses”.

The situation is not perfect—you have to flip this nonstandard switch, the resulting language isn’t source-compatible with standard Scala, and warts like bug 5075 (despite first appearances, this is quite distinct from 2712) remain—but Scala is in great shape with respect to this problem compared to where we were at the time of Kmett’s original writing.

[10:] In this mindset and in the same vein as the CanBuildFrom issue, things like Either don't have the biased flatMap you'd expect, somehow encouraging you to use other tools, just in case you wanted to bind on the Left. So you don't write generic monadic code over the Either monad, but rather are constantly chaining foo.right.flatMap(... .right.flatMap(....)) ensuring you can't use the sugar without turning to something like scalaz to fill it in. Basically almost the entire original motivation for all the type lambda craziness came down to being able to write classes like Functor have have several instances for different arguments, but because they are so hard to use nobody does it, making the feature hardly pay its way, as it makes things like unification, and path dependent type checking harder and sometimes impossible, but the language specification requires them to do it!

I’m not sure the situation was ever as severe as Kmett states, but that might be down to my personal experience in Scala, with Scalaz as my permanent companion.

The interspersed .rights never prevented you from using the for syntax, though they did make it significantly more obscure. Supposing foo and bar are Eithers:

for {
  x <- foo.right
  y <- bar.right
  ...

That trailing .right looks like it’s missing a dance partner, but it’s in just the right place for that biased flatMap or map method to kick in.

But in Scalaz, we never had to worry about it. Because we only supplied the right-biased Monad for Either. When you also bring in Scalaz’s Monad syntax, suddenly Either acquires the standard right-biased map and flatMap.

import scalaz.syntax.bind._, scalaz.std.either._

for {
  x <- foo
  y <- bar
  ...

No more lonely dancers.

But now ​right-biasing has returned to the standard library, so even these extra imports are no longer necessary.

Kmett pairs this point with a tangentially related point about functors over other type parameters. But I think higher-order unification is going to solve this problem, albeit in a very ad hoc way, in the long run. Programmers who want to use higher-kinded types will increasingly want to turn on the feature, or even be forced to by library designs that depend on it. Types that conform to right-bias—placing the functor parameter last, not first—will find happy users with nice inference.

class FA[F[_], A]

def fa[F[_], A](fa: F[A]): FA[F, A] =
  new FA

scala> fa(Left(33): Either[Int, String])
res0: FA[[+B]Either[Int,B],String] = FA@542c2bc8

This works even in more elaborate situations, such as with monad transformers:

trait EitherT[E, M[_], A]
trait ReaderT[R, F[_], A]
trait IO[A]
class Discovery[T1[_[_], _], T2[_[_], _], M[_], A]

def discover[T1[_[_], _], T2[_[_], _], M[_], A](a: Option[T1[T2[M, ?], A]])
    : Discovery[T1, T2, M, A] = new Discovery

scala> discover(None: Option[EitherT[String, ReaderT[Int, IO, ?], ClassLoader]])
res0: Discovery[[M[_], A]EitherT[String,M,A],
                [F[_], A]ReaderT[Int,F,A],
                IO,
                ClassLoader] = Discovery@4f20ea29

Contrarian types that don’t conform will find themselves rejected for constantly introducing mysterious type mismatches that must be corrected with more explicit type lambdas. So the libraries should develop.

[11:] You don't have any notion of a kind system and can only talk about fully saturated types, monad transformers are hell to write. It is easier for me to use the fact that every Comonad gives rise to a monad transformer to intuitively describe how to manually plumb a semimonoidal Comonad through my parser to carry extra state than to work with a monad transformer!

This isn’t so much about inference of higher-kinded type parameters, which I’ve dealt with above, but how convenient it is to write them down.

As mentioned above, the kind-projector compiler plugin has made writing these types significantly easier. Yet it remains ugly compared to the curried version, for sure.

[12:] I've been able to get the compiler to build classes that it thinks are fully instantiated, but which still have abstract methods in them.

I haven’t seen this kind of thing in quite a while, but it wouldn’t surprise me if a few such bugs were still outstanding. Let’s give the compiler the benefit of the doubt and suppose that things have gotten significantly better in this area.

[13:] Tail-call optimization is only performed for self-tail calls, where you do not do polymorphic recursion.

There are two issues packed here. The first still holds: only self-tail calls are supported. Plenty of ink has been expended elsewhere; I point to Dan Doel again for some of that.

The second issue has a fix in Scala 2.12.4!

@annotation.tailrec def lp[A](n: Int): Int =
  if (n <= 0) n else lp[Option[A]](n - 1)
// [in 2.12.3] error:⇑ could not optimize @tailrec annotated method lp:
// it is called recursively with different type arguments

scala> lp[Unit](1000000)
res0: Int = 0

To pour a little oil on, this isn’t a 50% fix; this is a nice improvement, dealing with a particular annoyance in interpreting GADT action graphs, but the much larger issue is the still-missing general TCO.

[14:] Monads are toys due to the aforementioned restriction. (>>=) is called flatMap. Any chain of monadic binds is going to be a series of non-self tailcalls. A function calls flatMap which calls a function, which calls flatMap... This means that non-trivial operations in even the identity monad, like using a Haskell style traverse for a monad over an arbitrary container blows the stack after a few thousand entries.

And this is the same, for the same reason. Kmett goes on to discuss the “solutions” to this.

[15:] We can fix this, and have in scalaz by adapting apfelmus' operational monad to get a trampoline that moves us off the stack to the heap, hiding the problem, but at a 50x slowdown, as the JIT no longer knows how to help.

Nothing has changed here. We’ve tweaked the trampoline representation repeatedly to get better averages, but the costs still hold.

[16:] We can also fix it by passing imperative state around, and maybe getting scala to pass the state for me using implicits and hoping I don't accidentally use a lazy val. Guess which one is the only viable solution I know at scale? The code winds up less than 1/2 the size and 3x faster than the identity monad version. If scala was the only language I had to think in, I'd think functional programming was a bad idea that didn't scale, too.

This is still something you have to do sometimes. Just as above, nothing has really changed here. You just have to hope you don’t run into it too often.

Random restrictions

[17:] for yield sugar is a very simple expansion, but that means it has all sorts of rules about what you can't define locally inside of it, e.g. you can't stop and def a function, lazy val, etc. without nesting another for yield block.

One thing has changed in this area! You no longer have to use the val keyword when defining a val locally in the for block.

Otherwise, situation constant.

[18:] You wind up with issues like SI-3295 where out of a desire to not "confuse the computation model", it was decided that it was better to you know, just crash when someone folded a reasonably large list than fix the issue.. until it finally affected scalac itself. I've been told this has been relatively recently fixed.

As Kmett mentions, this was fixed. It remains fixed.

[19:] No first-class universal quantification means that quantifier tricks like ST s, or automatic differentiation without infinitesimal confusion are basically impossible.

def test = diff(new FF[Id,Id,Double] { 
   def apply[S[_]](x: AD[S, Double])(implicit mode: Mode[S, Double]): AD[S, Double]
      = cos(x) 
})

is a poor substitute for

test = diff cos

kind-projector has provided less well-known support for some varieties of polymorphic lambdas, such as FF in this example, for a while. The implicit constraint and fact that we’re trying to be polymorphic over a higher-kinded type might make things tricky, but let’s see if we can get it working.

Lambda[FF[Id, Id, Double]](x => cos(x))
Lambda[FF[Id, Id, Double]](x => implicit mode => cos(x))

// both forms fail with the uninteresting error:
// not found: value Lambda

Scalaz 8 contains a very clever unboxed encoding of universal quantification based on the observation that if side effects and singleton type patterns are forbidden, as they are under Scalazzi rules, multiple type applications in Scala are indistinguishable at runtime. (To see why this is, consider the difference between List.empty[A] and mutable.Buffer.empty[A].) The one that comes with Scalaz 8 only quantifies over a *-kinded type parameter, but we should be able to use the same technique to quantify over S: * -> *.

trait ForallK1Module {
  type ForallK1[F[_[_]]]

  type ∀[F[_[_]]] = ForallK1[F]

  def specialize[F[_[_]], A[_]](f: ∀[F]): F[A]

  def of[F[_[_]]]: MkForallK1[F]

  sealed trait MkForallK1[F[_[_]]] extends Any {
    type T[_]
    def apply(ft: F[T]): ∀[F]
  }
}

object ForallK1Module {
  val ForallK1: ForallK1Module = new ForallK1Module {
    type ForallK1[F[_[_]]] = F[λ[α => Any]]
    def specialize[F[_[_]], A[_]](f: ∀[F]): F[A] = f.asInstanceOf[F[A]]
    def of[F[_[_]]]: MkForallK1[F] = new MkForallK1[F] {
      type T[_] = Any
      def apply(ft: F[T]): ∀[F] = ft
    }
  }
}

// we're using an unboxed representation
type FF[F[_], G[_], T, S[_]] = AD[S, T] => Mode[S, T] => AD[S, T]

scala> ForallK1.of[Lambda[S[_] => FF[Id, Id, Double, S]]](
           x => implicit m => cos(x))
res3: ForallK1Module.ForallK1.ForallK1[
         [S[_$1]]AD[S,Double] => (Mode[S,Double] => AD[S,Double])
      ] = $$Lambda$2018/266706504@91f8cde

Upshot? Nothing has changed in core Scala. People in the Scala community have discovered some clever tricks, which work even better than on the slightly complicated test case Kmett supplied when tried with more traditional *-kinded rank-2 idioms like ST.

scala> Lambda[List ~> Option](_.headOption)
res2: List ~> Option = $anon$1@73c4d4b5

trait ST[S, A] {
  def flatMap[B](f: A => ST[S, B]): ST[S, B]
}
trait STVar[S, A] {
  def read: ST[S, A]
}

def newVar[S, A](a: A): ST[S, STVar[S, A]] = ???

def mkAndRead[S]: ST[S, Int] = newVar[S, Int](33) flatMap (_.read)

def runST[A](st: Forall[ST[?, A]]): A = ???

scala> :t Forall.of[ST[?, Int]](mkAndRead)
scalaz.data.Forall.Forall[[α$0$]ST[α$0$,Int]]

scala> :t Forall.of[Lambda[s => ST[s, STVar[s, Int]]]](newVar(33))
scalaz.data.Forall.Forall[[s]ST[s,STVar[s,Int]]]

scala> :t runST(Forall.of[ST[?, Int]](mkAndRead))
Int

scala> :t runST(Forall.of[Lambda[s => ST[s, STVar[s, Int]]]](newVar(33)))
<console>:19: error: type mismatch;
 found   : Forall[[s(in type Λ$)]
                  ST[s(in type Λ$),
                     STVar[s(in type Λ$),Int]]]
 required: Forall[[α$0$(in type Λ$)]
                  ST[α$0$(in type Λ$),
                     STVar[_ >: (some other)s(in type Λ$) with (some other)α$0$(in type Λ$), Int]]]

Knowledgable use of these tricks will give you much better code than we could produce when Kmett wrote this, but it’s still nowhere near as elegant or easy-to-use as rank-2 in Haskell.

... but it runs on the JVM.

Indeed, Scala still runs on the JVM.

How good an idea is it?

So, a few things have gotten better, and a few things have gotten a lot better. That bodes well, anyway.

Functional programming practice in Scala will continue to encounter these issues for the foreseeable future. If you are writing Scala, you should be practicing functional programming; the reliability benefits are worth the price of entry. While you’re doing so, however, it’s no thoughtcrime to occasionally feel like it’s a bad idea that doesn’t scale.

This article was tested with Scala 2.12.4 -Ypartial-unification, Scalaz 8 3011709ba, and kind-projector 0.9.4.

Portions Copyright © 2013 Edward Kmett, used with permission.

Copyright © 2017, 2018 Stephen Compall. This work is licensed under a Creative Commons Attribution 4.0 International License.

Writing about subtyping

I want programmers to stop using subtyping, yet I keep bringing it up, in article after article. Partly that is because it is very hard to avoid subtyping-related issues in Scala, and I find myself concerned with Scala when I ought to be devoting mental cycles to simpler, more powerful languages. But that may simply feed into what I suppose is the greater reason:

Subtyping is an amusing puzzle for my mind. I enjoy the mental diversion of the needlessly complex puzzle of practical programming techniques making use of subtyping.

I can justify this self-gratification by saying to myself, “the more they read about what subtyping really means, the more their desire to avoid this mess will grow”. I think this is more rationalization than honest motivation for myself, though I do think those who learn more about subtyping are more likely to avoid it, just as those who learn more about typing are more likely to advocate it.

Yet, it does have a kind of beauty. So I take it out here and there, and appreciate its facets for a while. Then I carefully return it to its display case, lest I am afflicted with the subtyping bug again.

Spare me the tedium of “simple” linting, please

In the development environments of singly-typed languages like JavaScript and Python, one popular build step for improving code quality is the “linting” or “style” tool. Tools like jshint and pyflakes point out misspellings and references to missing variables, idioms that frequently lead to bugs like == usage, calls with apparently the wrong number of arguments, and many other things.

Much of this is meant to mechanize the enforcement of a team’s style guidelines—at their best, sincere and effective tactics for avoiding common sources of bugs. Unfortunately, many of these guidelines can seem excessively pedantic, forcing the programmer to deal with cases that could not possibly happen.

Normally, it would make sense to tell the programmers to just suck it up and follow the rules. However, this tactic can lead to a couple bad outcomes.

1. The lint check can lose support among developers, for being more trouble than it’s worth. If programmers feel that a lint is causing more code quality issues than it’s solving, they’ll sensibly support its removal.
2. Lints without developer support tend to be disabled sooner or later, or simply mechanically suppressed at each point they would be triggered, via “ignore” markers and the like. At that point, the bug-catching benefits of the lint are completely eliminated; in the worst case, you have a universally ignored warning, and are even worse off than if the warning was simply disabled.
3. If the errors spotted by the lint are serious enough, but the lint warns for too many exceptional cases, the developers might decide to move the style rule to manual code review, with an opportunity to argue for exceptional cases. This is labor-intensive, carries a much longer feedback cycle, and makes it easy to accept an argument for an exception to the style rule that is actually erroneous, as it is not machine-checked.

Many of these “too many false positives” warnings could be a lot better if they simply had more information to work with about what will happen at runtime. That way, they can avoid emitting the warning where, according to the extra information, a construct that appears dangerous will not be a problem in practice.

That is one thing that type systems are very good at. So lint users are on the right track; the solution to their woes of needless ritual is more static analysis, rather than less.

Let’s consider some common lints in JavaScript and see how the knowledge derived from types can improve them, reducing their false positive rate or simply making them more broadly useful.

Suspicious truthiness tests

(This example has the benefit of a recent implementation along the semantic lines I describe, in Flow 0.52. I take no credit for any of the specific lint suggestions I make in this article.)

In JavaScript, a common idiom for checking whether an “object” is not null or undefined is to use its own “truthiness”.

if (o)        // checking whether 'o' is defined
if (o.magic)  // checking whether 'o's 'magic' property is defined

This is concise and does the trick perfectly—if the value being tested isn’t possibly a number, string, or boolean. If it can be only an object, null, or undefined, then this is fine, because even the empty object {} is truthy, while null and undefined are both falsey. Unfortunately, in JavaScript, other classes of data have “falsey” values among them, such as 0 for number.

The “lint” solution to this problem is to always compare to null directly.

if (o != null)                     // not null or undefined
if (o !== null && o !== undefined) // required in more pedantic code styles

This might be encapsulated in a function, but still doesn’t approach the gentle idiom afforded by exploiting objects’ universal truthiness. But the object idiom is simply unsafe if the value could possibly be something like a number. So the question of whether you should allow this exception to the “always compare to null explicitly” lint boils down to “can I be sure that this can only be an object?” And if in review you decide “yes”, this is a decision that must constantly be revisited as code changes elsewhere change the potential types of the expression.

You want to mechanically rule out “possible bugs” that are not really possible in your use of the idiom, so that the linter will not warn about benign use of truthiness—it will save the warnings for code where it could actually be a problem. Ruling out impossible cases so that you only need cope with the possible is just the sort of programming job where the type system fits in perfectly.

A type system can say “this expression is definitely an object, null, or undefined”, and type-aware linting can use that information to allow use of the truthiness test. If that data comes from an argument, it can enforce that callers—wherever else in the program they might be—will not violate the premise of its allowance by passing in numbers or something else.

A type system can also say “this expression will definitely be an object, never null”, or vice versa, thus taking the lint even further—it can now tell the programmer that the if check is useless, because it will always be truthy or falsey, respectively. This is just the sort of premise that’s incredibly hard for humans to verify across the whole program, continuously, but is child’s play for a type-checker.

A type system such as Flow can even say “this expression could have been something dangerous for the truthy test, like number | object, but you ruled out the dangerous possibilities with earlier if tests, so it’s fine here”. Manual exemption can regress in cases like this with something as simple as reordering “if-else if-else” chains a little carelessly—keep in mind here the decades of failure that “be sufficiently careful” has had as a bug-avoidance tactic in programming—but type-aware linting will catch this right away, waking up to declare its previous exemption from the style rule null and void.

The more precise your types in your program, the more understanding of your use of this idiom—in only valid places—the type-aware linter will be. It will not make the reasoning mistakes that human review would make when allowing its use, so you can use it with more confidence, knowing that the lint will only call out cases where there’s a genuine concern of a non-null falsey value slipping in. And there is no need to argue in code review about which cases need != null and which don’t, nor to revisit those decisions as the program evolves; as circumstances change, the type checker will point out when the verbose check becomes unnecessary, or when the succinct check becomes unsafe.

References to undeclared variables

It’s very common to mistake a variable name that isn’t defined for one that is. The larger a program gets, the easier this mistake is to make.

This mistake comes in a few forms. It may be a simple misspelling. It may be a variable you thought was defined here, but is actually defined somewhere else. It may be a variable defined later, but not yet.

Whatever the meaning of the error, linters can catch the problem via a relatively simple method. As the file is scanned, the linter keeps track of what variables are currently in scope. When encountering a variable reference, it checks the variable name against its current working list of variables. If one is not in the list, the linter reports it.

This is better than nothing. Compared to what you can do with a type checker, though, it’s not very good at all.

Suppose that you have a few local functions defined at the top level of your module, foo, bar, and baz. A linter will point out an undeclared variable if you try to call fop, gar, or bax. So you don’t have to wait for the browser reload or test cycle; you can correct these errors right away.

Later on, your module is getting larger, so you decide to group some functions into objects to clean up the top-level namespace. You decide that foo, bar, and baz fit under the top-level object q.

const q = {
    foo(...) {...}

    bar(...) {...}

    baz(...) {...}
}

During your refactoring, references to these three functions are rewritten to q.foo, q.bar, and q.baz, respectively. This is a nice way to avoid ad hoc name prefixes as a grouping mechanism; you’re using a first-class language feature to do the grouping instead.

But let’s give a moment’s consideration to q.fop, q.gar, and q.bax. The linter will verify that the reference to q is sound; it’s declared at the module level as const q. However, the linter will not then verify that the “member” references are sound; that is a fact about the structure of q, not its mere existence.

When all you have is “simple” linting, this becomes a tax on modularity, so to speak. If a variable is defined locally—very locally—references to it are checked. If it is defined remotely, whether in another module or simply “grouped” in a submodule, references to it are not checked.

A type system cuts the modularity tax by tracking the names that are beyond the purview of the simple linter. In the case of q, type-checking tracks more than its existence; its statically-known structural features are reqorded as part of its type.

• In this module, q is defined.
  • It is an object,
  • and is known to have properties:
    • foo,
      • a function which is…;
    • bar,
      • a function which is…, and
    • baz,
      • a function which is…

This continues to work at whatever depth of recursion you like. It works across modules, too: if I want to call baz from another module, I can import this module in that one, perhaps as mm, and then the reference mm.q.baz will be allowed, but mm.q.bax flagged as an error.

An undeclared-variable linter is all well and good, but if you want to take it to its logical conclusion, you need type checking.

hasOwnProperty guards

The best lints focus on elements of code hygiene we’re reluctant to faithfully practice while writing code, but come back to fill us with regret when we fail to do so. One example arises with using for to iterate over objects in JavaScript; the lint checks that you’re guarding the loop with hasOwnProperty.

The purpose of these guards is to handle non-plain objects; that is to say, objects “with class”. The guards are always suggested by the linter to avoid nasty surprises should you try iterating over the properties of an object “with class”.

The irony of this check is that the intent of such code is usually to work with plain objects only, that is, classy objects should not be present in the first place! The construct is still perfectly usable with classy objects; it’s just that more caution is called for when using it in that fashion.

As such, there are two basic scenarios of for iteration over objects.

1. iteration over plain objects only, and
2. iteration over potentially classy objects.

The focus of the hasOwnProperty guard ought to be #2, but this concern bleeds over into #1 cases, needlessly or not depending on how pessimistic you are about Object.prototype extension. But this question is moot for the linter, which can’t tell the difference between the two scenarios in the first place.

By contrast, a type checker can make this distinction. It can decide whether a variable is definitely a plain object, definitely not one, or might or might not be one. With that information, depending on your preferences, it could choose not to warn about a missing hasOwnProperty guard if it knows it’s looking at scenario #1. So if a hasOwnProperty is needless, it need not pollute your code for the sake of the scenarios where it will be needed.

Computer, please try to keep up

Humans are pretty good at coming up with complex contractual preconditions and postconditions for their programs, and making those programs’ correct operation depend on the satisfaction of those contracts. But humans are very bad at verifying those contracts, even as they make them more complex and depend more on them.

“Simple” linting tools are good at checking for the fulfillment of very simple rules to help ensure correctness, freeing the human mind to focus on the more complex cases. What makes them a chore to deal with—a reason to put solving linter warnings on the “technical debt backlog” instead of addressing them immediately—is “they don’t know what we know”; they can handle laborious low-level checks, but lack the sophisticated analysis humans use to decide the difference between a correct program and an incorrect one.

Happily, through static analysis, we can get much closer to human-level understanding’s inferences about a program, while preserving the tireless calculation of contractual fulfillment that makes linting such a helpful companion in the development cycle, doing the parts that humans are terrible at. When your linter is so “simple” that it becomes a hindrance, it’s time to put it down, and pick up a type system instead.

Or, we could not, and say we don’t have to

I previously wrote “Values never change types”, whose central thesis statement I hope is obvious. And this still holds, but there is something I left unsaid: values do not have identity, so the notion of “mutating” them is as nonsensical as “mutating 4”. And the formal system of Scala types treats objects with identity similarly, by not permitting them or their variable aliases to change type, even though they are not quite values. But this is a design decision, and other choices could have been made.

There are very good reasons not to make other choices, though. Other type systems come with features that come very close to making the opposite design choice; by imagining that they went just a little farther down this garden path, we can see what might have been.

Refinement, flow, or occurrence typing, by any name

In Flow and TypeScript, when you test properties of a value in a variable, you can “change the type” of that variable. For example, you could have a let s: any; if you write an if block that tests whether s is a string, the type of s—at compile-time, mind you—“changes” to string within the if body. Within the body of that if, you could perform further tests to refine s’s type further; you might also have various other if blocks alongside checking for other types, so that s might variously “change” into number, function, object with a whatsit property whose type is another object with a whosit property, and so on.

So, instead of having a single type attached to a lexical variable over its entire scope, a variable has several types, each tied to a block of code that uses the variable. It is an order more sophisticated, but still tied to the lexical structure of the program, as if the variable has multiplied to honor all the faces it might have. This is a great way to model how people are writing programs at the type level without overly complicating the formal system, which still must always obey a complete set of sound rules.

Contradictory refinement

In the systems I’ve described, no further refinement can contradict a prior one. So once you determine that a variable is a string, it’s not going to turn out to be a number later; at most, it can get more specific, like being proven to be a member of a known static set of strings. So this way you know that inner blocks cannot know less than outer blocks about the nature of a variable; that is what I mean by “tied to the lexical structure.”

What “real JavaScript code” could be written that would violate this assumption?

function foo(arg) {
    let s = arg
    if (typeof s === 'string') { // refines s to type string
        s = {teaTime: s}
        // "point of no return"
        if (s.teaTime === "anytime") {
            drinkTea(s)
            ...

The first if test establishes a block in which s’s type is string. Then we pull the rug out from under the type-checker by assigning to s; with that assignment, it is no longer true that s is a string. Why does this make type-checking more complex?

Let’s twist and tangle the program to support our beloved mutation

The type of the variable s no longer follows the block structure of the program, in the way we usually perceive blocks in a structured program. That’s because the fact established by the outer if test is suddenly invalidated partway through the block. So our first problem is one of raising the complexity burden on human interpretation of the program—the reader can no longer assume that the specificity of a variable’s type only increases as you move inward, reading the block structure of the program—but it is not fatal in itself, at least for this example. We can salvage the model via the Swiss Army knife of semantic analysis, the continuation-passing style (CPS) transform.

function foo(arg, k0) {
    return (s => if (typeof s === 'string') {
                     (_ => if (s.teaTime === "anytime") {
                               drinkTea(s, k0)
                           }
                     )(s = (teaTime: s))
                 }
           )(arg)

Now it is still possible for inner blocks to contradict outer blocks, but at least this is only possible at the block level. So, by “merely” revisualizing our programs in terms of the flow of continuations rather than the visibly apparent block structure, we can sort of still think of the type of variables as a “block”-level concern, as it was before.

Unluckily, performing a CPS transform in your head with all the code you see is a kind of “reverse Turing Test”, something that an AI would have to not be able to do very well in order to fool us into thinking it was human. So no matter what, we are stuck with a significant new complication in our formal model.

But not a fatal one. Yet.

Loop unrolling according to the phase of the moon

What will prove fatal to the formal model of type-changing mutation is delay. Let us see how the seeds of our destruction have already been sown.

while (forSomeTimeNow()) {
    log(s.substring(1))
    if (itsAFullMoon()) {
        s = {teaTime: s}
    }
    drinkTea(s)
}

The first question, and the last, is “is it safe to drinkTea?”

One necessary prerequisite is that it has been a full moon. I’m using this boolean expression to inject the Halting Problem—we cannot determine in a Turing-complete language whether a boolean expression will evaluate to true or false, generally—but it is probably sufficient to say that it is nondeterministic, even if not Turing-complete. (Pragmatists love Turing completeness and nondeterminism, because “more power is always better”.) So it’s hard enough—by which I mean generally impossible—to say whether the s assignment has happened.

The next prerequisite, which should drive us wholly into despair now if hope yet remains, is that the moon has been full once. Eh? Here’s where the tie of variable types to any semblance of code structure breaks down completely, because s takes on a surprisingly large number of types in this code sample.

To assign a precise type to this program, we have to accurately model what is happening in it. So, suppose that prior to entering this loop, the type of s is string. Each assignment to s—made each time the while’s test is true and the moon is full—takes us one step down this list of types.

1. string
2. {teaTime: string}
3. {teaTime: {teaTime: string}}
4. {teaTime: {teaTime: {teaTime: string}}}
5. {teaTime: {teaTime: {teaTime: {teaTime: string}}}}
6. •••

Now if you want to assign (potentially) all of these infinite possibilities to the program, you have to go even further from the block structure model. Imagine a third dimension of the program text: at the surface, you see s having only the first two types above, but as you look deeper, you see the branching possibilities—oh so many iterations in, oh so many times the moon has been full—each assigning different types to what is on the surface the same code. Looking at this as two-dimensional text, you would only see the infinite superimposition of all possible types of s, weighted according to their probability.

Three dimensions might be too few for this code.

Of course, there’s a well-known, sensible way to type this code, sans the log call: abandon the folly of modeling mutation and assign this recursive union type to s for at least the whole scope of the while loop, if not an even wider scope:

type TeaTimeTower = string | {teaTime: TeaTimeTower}

And supposing the drinkTea function is so polymorphic, all is well, and as a neat side bonus, easy to understand. But we aren’t here to pursue sanity; we gave that up to try to model mutation.

The devil in the delay

If fully desugared, while is a two-argument (not counting still thinking in CPS) higher-order function, taking test functions as arguments. Just like you’re writing Smalltalk.

while(() => forSomeTimeNow(),
      () => {
          log(s.substring(1))
          if(itsAFullMoon(),
             () => s = {teaTime: s})
          drinkTea(s)
      })

The thing that makes so much trouble for flow analysis is this delay. Type-changing requires us to contradict earlier refinements of a variable’s type, not simply refine them further. But the ability to capture a reference to a variable in a lambda means that we need a deep understanding of how that lambda will be used. It might never be invoked. It might be invoked later in the function, just when we thought it was safe to contradict whatever refinement it was type-checked with. It might be saved off in another variable or data structure elsewhere in the program, making reasoning about when the variable might be referenced in the future a futile endeavor.

Doing flow analysis with sources of delayed execution whose behavior is 100% known, like if and for, is tricky enough. Doing it in the presence of unknown, novel, potentially nondeterministic sources of delay is intractable, if not impossible.

And that’s for the computer. How many dimensions does the model in your head have, now? Zero, no, negative points for abandoning this ivory-tower static analysis and declaring “common sense” the arbiter of your programs’ correctness.

Did anyone else see you come here?

An object with known properties can be thought of as a group of named variables. This is a longtime, straightforward way to represent modules of functions, or clean up a global namespace by putting a lot of related items laying on the floor into the same drawer.

Since we love mutation, and we love mutating variables, we should love mutating object properties (and their types) even more, right?

function schedule(s) {
    s.teaTime = "anytime"
}

The type of s in the caller after schedule finishes is straightforward: it’s whatever it was before, with the teaTime field (whatever it might have been before, if anything) type set to string, or perhaps the literal singleton type "anytime".

But what schedule is so eager to forget will not be so easily forgotten by the rest of the program.

Namely, the contradicted, earlier type of s is very hard to reliably eradicate. This is an aliasing problem, and it brings the excitement of data races in shared-mutable-state multithreaded programs to the seemingly prosaic JavaScript execution model.

To type s in the aftermath of schedule, you must perfectly answer the question, “who has a reference to s”? Suppose that teaTime was a now-contradicted function. Any code that calls that function via property lookup on its reference now takes on another dimension: before schedule executes, it is safe, but afterwards it no longer is, so it takes on the prerequisite “can only be called before calling schedule(s).” The dimensional multiplication directly results from the multiplication of possible types for s.

The problem broadens virally when you try to model other variables that are not s, but whose types will still change due to schedule being called! Here is an example of such a variable.

const drinks = {coffee: coffeeMod; tea: s}
  // where s is the value we’re talking about

So all the analysis of references to s induced by the type mutation means references to drinks must undergo the same ordeal. And references to something that refers to drinks, and references to something that refers to that, and so on, ad infinitum.

And that is assuming we can statically determine what object identities will be flying around the program. As with so much else in this article, this is generally impossible.

By the way, the problem with lambdas is just a special case of this one; it’s exactly that lambdas alias variables that causes so much grief for our wannabe-mutating ventures.

A different kind of power, at a much more reasonable price

Since we are only imagining this insanity, not attempting to truly partake of it, we have something good to feel about, after all: the grass is really quite brown on the other side, alas, but that on this side is a little greener than first glance might indicate.

Type systems like those of Haskell, Java, OCaml, Scala, and many other languages simply don’t permit the types of variables to change. When you consider the introduction of type equalities in Haskell or Scala GADTs, or more direct refinements made in Typed Racket, Flow, or TypeScript; you can include all of these languages in the broader category of type systems whose variable types can only complement, never contradict.

This is a powerful simplifying assumption, because under this restriction, none of the above problems matter. “Functional types” are not only powerful enough to model programs, and far easier to understand for the human programmer, they are the only way out of the quagmire of complexity wrought by trying to “model mutation”. Even problems that almost look amenable to mutation analysis, like the while example above, admit a simpler solution in an immutable type like the recursive TeaTimeTower.

More power is sometimes worse.

When you forbid unneeded capabilities, you get back capabilities in other areas. Sometimes this comes in the form of improved understanding, such as we get for large programs by introducing type restrictions. It makes sense to give up “power” that is not practical to get benefits that are.

Take the forbidding of mutation. We take type-level immutability for granted in the same way that many practitioners take value-level mutability for granted. Perhaps one reason for resistance to functional programming might be that we are so accustomed to the drawbacks of unconstrained mutability that it does not seem quite as insane at the value level as, seen above, it is at the type level.

But, familiarity cannot make the insane any less so.

This article was tested with Flow 0.57.2 and TypeScript 2.5.