The strength of this system is that map is type checked to be provably side-effect free. The mapping function is free to internally allocate and mutate objects

The strength of this system is that map is type checked to be provably side-effect free. The mapping function is free to internally allocate and mutate objects to get its job done, e.g. a RegexMatcher, but it may not mutate existing (non-isolated) state. This composes transitively, so even wrapping side-effects in abstractions and closures is insufficient to hide them.