1. 8

  2. 9

    An explanation that I find enlightening goes something like this “Maybe is a typed nil.” That is, it lets you tell the difference between, say, the lack of a string and the lack of an integer (as well as the lack of a polymorphic type, ‘a’, but now I’m getting carried away). From a tweed-jacket beard-stroking philosophical perspective, this is kinda interesting, no? If I search a database for a user and get nil and I likewise search a database for a telephone number, also getting nil, it makes sense that these “nope-flavored” answers would be incompatible. What nil does then is take a lack of a user and obscures even that little bit of information leaving only a jagged nope! in its wake.

    1. 1

      “An explanation that I find enlightening goes something like this “Maybe is a typed nil.” ”

      Like “nan” ?

      1. 1

        Yeah, that’s a really good example! The use of NaN in the wild follows this pattern. We don’t see people writing functions where this happens:

        function getName(id) {
          var result = lookup(id);
          if(result) {
            return result;
          } else {
            return NaN;

        So the concept for at a typed null, at least for numbers, is out there.

    2. 7

      “How is this different from nil?” is the inevitable question I get from rubyists upon learning about the Maybe monad. Until a flash of inspiration the other day, I didn’t quite have a good explanation for this question. Sure, I had an explanation, but I don’t think it was very convincing to rubyists. It went something like: “Because it forces you to explicitly handle the nil case rather than accidentally let it through.”

      That much only explains why you would prefer Maybe to unrestricted nullability. It doesn’t explain why you would prefer Maybe to, say, Ceylon and Kotlin’s type-tracked nullability. To understand the latter, consider the type of the join function:

      join :: Monad m => m (m a) -> m a
      -- specialized to Maybe
      join :: Maybe (Maybe a) -> Maybe a

      Monads nest, because they’re type constructors like any other. On the other hand, nullability doesn’t nest, because it’s a hard-coded special case in the language.

      1. 3

        The example I like to give is to think of any real world situation where Maybe (Maybe a) makes sense and is a meaningful thing to return. These are actually pretty easy to come by, especially if you’re also talking about Either because then Either e1 (Either e2 a) forces the issue.

        At this point, join becomes a highly meaningful operation and you can talk about how Kotlin-style nullability doesn’t let you talk about that. It becomes a tradeoff between convenience and expressiveness, and expressiveness can be defended by picking out real-world examples where nested errors are important to distinguish (see that Either e1 (Either e2 a) example again).

        1. 2

          For me, the justification for preferring Maybe to nil is much simpler: The basic building blocks of our programs must have nice algebraic properties. The introduction of special cases should be delayed until you have enough information about your problem domain to justify it. Language designers in general don’t have this sort of information, so language features should be as uniform as possible.

          1. 2

            Yeah, I honestly agree with you but think that kind of argumentation puts the cart ahead of the horse. Anyone who buys the value judgement won’t really need convincing as to why to include Maybe, no?

        2. 2

          I’m not sure I completely grok this comment, but I like it.

          I’ve twice written “Maybe” implementations for languages with unrestricted nullability (C# and TypeScript, back when TypeScript lacked nullability annotations of its own), and it’s been a very interesting learning experience doing so.

          Both types were naive implementations that broke associativity just like java.util.Optional does.

          What I think is interesting is that at first it seemed like this breakage was the most appealing feature of the type — that is, by funneling all sorts of function calls through “Maybe”, each individual function could be assured of receiving non-null arguments, since any nulls would be “consumed” by the chaining machinery. Sounds great! Guard the “borders” of your module with Maybes and then everything inside can be your Happy Place!

          Knowing what I know now, I probably would not have written that code. As you say: nullability is a special case in the language. It doesn’t seem possible to circumvent it without incurring breakages somewhere else.

          1. 1

            In general, when confronted with special cases, you can either embrace them (e.g., the way Common Lisp treats NIL) or pretend they don’t exist (e.g., the way idiomatic Scala treats null), but you can’t really fix them (e.g., the ways in which “perfect” forwarding in C++ fails to actually be perfect). That’s why IMO one should think twice before introducing special cases: you are imposing on the users of your code the responsibility to handle them all correctly.

        3. 3

          If we wanted to truly solve the problem of codebase-exhaustiveness, however, I posit that it is impossible to create a fully robust type checker for Ruby.

          I don’t have any proof, but I don’t believe this to be true. The example given (a function with a block) could be type checked if blocks can have types specified, for instance. I think the problems of having type checked dynamic languages is hard for a number of reasons(that are more complicated than dealing with blocks) but I don’t think it is impossible.

          1. 9

            I don’t have any proof, but I don’t believe this to be true.

            Oh, I do! http://erlang.org/doc/man/dialyzer.html

            Anyway type checking aside you can definitely benefit from Maybe in a dynamic language. The requirement is actually not so much to have a static type system as it is to have pervasive pattern matching and buy-in from the standard library. Erlang is dynamic but often returns tuples of {ok, Value} or {error, Reason} from functions which could fail; the presence of the wrapper indicates you need to match against it to separate out the happy path from the failure. Obviously you can defy it, but you basically have to go out of your way to do this.

            1. 2

              Agreed on Maybe. I do not much care for nil/null.

            2. 4

              My observation is that people from dynamic programming backgrounds usually imagine things like String and Int when talking about types. Even though these are the kinds of types that appear the most often in your codebase, they’re not the things that determine the power of a type system. Whenever you want to reuse code and express patterns, you need abstractions, and that progressively demands more and more from the type system. So,

              • you start with a String but then you need a function String -> Int
              • then you want to work with such functions so you need (String -> Int) -> [String] -> [Int]
              • then you want this to work for all types so you need forall a b. (a->b) -> [a] -> [b]
              • then you want this to work for many kinds of data structures, so you need forall f a b. Functor f => (a->b) -> f a -> f b
              • then you want to interleave side effects, so you need forall t f a b. (Traversible t, Applicative f) => (a -> f b) -> t a -> f (t b)

              And this is really just the tip of the iceberg. So, please take a moment to think about a metaprogramming utility you use in Ruby, and try to express its type completely (not just “this takes boring stuff and returns cool stuff”), in any type system you can imagine. I think this exercise quickly demonstrates how easily types get intractable once you try to model the creative things people do in dynamic languages.

              1. 2

                First off, I find your “observation” and overall tone a bit condescending but it probably is true for many dynamic programmers. Myself, I’ve used typed languages enough to not have this simplistic view but I’m not well versed enough to be able to discuss it at a formal level. I plan to learn a lot more, but my list of learning projects is miles long so I don’t know when I’ll get to it.

                Typing some forms of metaprogramming actually seems quite easy to me. If you are doing lisp macros for metaprogramming, a lisp macro takes a code form and returns a code form so you need a type representing a code form (which basically would be a list of literals and symbols) and then you can have a super generic type definition for macros. Since code forms are lists in lisp, each macro would be taking a specific “shape”(or shapes) of list and returning another specific “shape”(or shapes) of list so that should be able to be typed as well. That being said, depending on the implementation of the type system some things that we currently do in macros might not be possible simply due to being hard/impossible to express the type. I haven’t played with shen much yet, but I assume it must be doing something with types and macros.

                For Ruby it is harder/possibly impossible to type metaprogramming since everything is basically side effect based from what I understand. For that matter, due to Ruby’s overall design of side effects everywhere ruby in specific may be not possible to build a robust type system for. There might be a way but I have no idea what it’d look like.

                I don’t think that applies to “dynamic programming languages” in general though.

                1. 5

                  I’ll say that “Typing Ruby” is probably a pretty difficult endeavor. I come at this from a lot of strongly typed programming experience, significant experience with gradually-typed systems, and the experience of having written a few type systems. On top of that all, I used to use Ruby in anger quite a lot a long while ago. That said, I haven’t tried to actually write a type system for Ruby, so what follows is speculation.

                  There are at least two technical challenges. Broadly, applying types to dynamic languages refines them and adds more information. The complexity curve of this new information can be quite high since it’ll be describing a system that was designed outside of the influence of the refinement.

                  Firstly, this will make inference a really, really tricky proposition. Inference is very delicate in type systems and can go from complete-and-easy to completely inoperable in a flash. Annotation of methods and procs is a good first step—it sidesteps the need for inference by demanding that the programmer provides intent—but a practical type system will allow you to elide these types at least some of the time.

                  Secondly, there will be a tradeoff between complexity of the type language and the set of features which can be given types both at all and in practice. Since rising complexity makes the type system harder to use and breaks inference even more this will probably instead be interpreted at the cost of loss of Ruby features.

                  Both of these technical challenges apply pretty much only if your goal is to build a New Ruby With Types and are willing to lose the entire Ruby community and existing codebase. If that’s not your goal then you additionally need to handle code which is untyped alongside code which isn’t. There are roughly two approaches here that I know of:

                  • Give all untyped code the any type and be forced into doing manual value-shape checks at the boundaries between typed and untyped code (a la Typescript)
                  • Do the above semi-automatically by extending a contract system into the untyped fragment of the language (a la Typed Scheme)

                  You’ll also run into the question of “Can we give types to existing code?” which again you can follow Typescript’s lead here, but note that this is extra burden on either the community or the original maintainer and it gets a little dicey.

                  Finally, after all that we can scratch the surface a little bit of interesting Ruby features which would be difficult to typecheck. Assuming we don’t have a dependently typed system (which is a good assumption since those are still heavy research subjects) you’ve already struck the motherlode in naming Ruby’s runtime metaprogramming features. The easiest target is “eval”. This is pretty much right out. With dependent types we could add a new function “check” which, given a runtime type representation that reflects its compile-time type could link up a successful checking process with an option to evaluate the expression into that type… but let’s leave that for now.

                  Idiomatic Ruby makes heavy use of method_missing. There are worse offenders used popularly, but this one is simple to analyze and crushingly difficult to type. Let’s just leave on the table its relationship to respond_to? which allows even more dynamic use of the functionality (and room for error when respond_to? and method_missing don’t align). Under the presence of method_missing the fragment

                  x.method arg1, arg2, arg2

                  can take essentially any type whatsoever. It also provides zero information about what the types of arg1, arg2, and arg3 are. We can special case this to first infer x’s type and then read out its known methods via its class hierarchy so that at least if a known method exists we can easily do the right thing statically, but the level of runtime shenanigans available to change the type of x.method when method_missing is in use is extreme.

                  A sophisticated type language could constrain method_missing at least some of the time by constraining what sort of overloaded methods are allowed to exist, but this is (a) restricting its power to the point that it’s really almost completely defunct and (b) breaking most idiomatic use-cases of method_missing.

                  You could make it so that method_missing just accepts any types and returns an any type, but again this breaks inference since you often will want method calls to put constraints on their arguments so that type information can “flow backwards” and, additionally, it will force manual runtime type guards in places which are normally elided. The common practice is to just “know” that method_missing calls have certain behaviors without any static description amenable to the language.

                  So, where does this leave things? Really, there are a lot of great examples of type systems which are sufficiently rich and generic to make meaningful dents in dynamic languages today: Typed Scheme, Typescript, and Flow come immediately to mind. Additionally, Erlang’s Dialyzer should be studied although it tries to do a slightly different thing. All of them (except Dialyzer) face really enormous difficulties though in that they splinter the community. Javascript programmers are not immediately Typescript programmers, although Typescript programmers do sometimes get the opportunity to reuse some Javascript code.

                  These examples are probably the best leaders for any Typed Ruby exploration. They also set the limits for what people have figured out how to do with respect to gradual type systems in practice.

                  1. 2

                    I’m sorry if that sounded condescending, it wasn’t my intention.

                    1. 1

                      Yeah, I wasn’t offended and I figured it wasn’t intentional. It still bugged me slightly though :).

                2. 4

                  I’m pretty sure you can do heinous tricks with class objects and VM to defeat even the most earnest attempt at type checking.

                  1. 3

                    Ugh. I meant to say eval instead of define_function. Does that change anything?

                    1. 3

                      I’d have to think about that one. My first instinct is that eval breaks type systems but not 100% sure.

                      Edit: found that haskell has an eval. http://hackage.haskell.org/package/plugins- So they were able to do limited type checking it looks like but not “robust”.

                      1. 5

                        Notice the way that Haskell’s eval works

                        • It constrains the return type with a Typeable constraint meaning that we have access to runtime type representatives
                        • It can fail Maybe
                        • The IO is incidental to Haskell’s pure nature—an impure language won’t suffer too much here

                        Typeable and Maybe here are providing the structure for what’s known as a type safe cast. You can think of eval as working in stages:

                        Here, Dynamic represents a value which can take any type whatsoever—the specific type information is not known at compile time, but it’s guaranteed that Dynamic values will be stored alongside runtime type representations which match their actual type. Stage 2 is the type-safe cast (and actually already has a definition as Data.Dynamic.fromDynamic).

                        Stage 1 is just a hook into the Haskell compiler. It typechecks the code and if that check succeeds produces a runtime representation of the result type. It runs the code fragment and obtains the result and then packages that result up with its runtime type information into a Dynamic value.

                        Stage 2 is a trick. Since a is left generic, it’s up to the caller of stage2 (and ultimately eval) to pick what a they want. In effect, it’s a guess by the user of eval as to what the return type of their fragment will be. We use Typeable to obtain a runtime type representation of the caller’s “guessed” type and then compare that representation with the type we inferred/checked in stage1. If they match then we coerce the result into the “guessed” type and things are OK. If they don’t match, we fail and return Nothing.

                        Really, the stages probably ought to be mixed so that if the caller guesses the wrong type then perhaps the string fragment shouldn’t be run at all.

                        Finally, as the docs note, there is a limit to how much this guess-and-check game can be played with real code in that the eval’d fragment more-or-less has to be monomorphic.

                        Also worth noting is the unsafeEval variant there. As always in Haskell, unsafe means really, really unsafe and requires that the user is carefully checking invariants. It is equivalent to a call to unsafeCoerce and can be used to break type invariants in a completely arbitrary fashion. It also doesn’t provide much more power than normal eval.

                        1. 2

                          article updated. thanks for pointing it out!