That being said, sum types would be a nice addition to this library.
> When most practitioners think of "typechecking", they typically think about proving properties about programs statically.
This is what the type theory community (e.g. Bob Harper) thinks...not anyone else from what I can tell (definitely not practicing programmers).
Typing it out on mobile didn't make it easy to do the right quote context. Here is a good essay about it all:
http://www.cl.cam.ac.uk/~srk31/research/papers/kell14in-auth...
vs. say
https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...
There are other ways to do typing that might make more sense for a dynamic language than going down the expressiveness rabbit hole; e.g.
I'm not saying that types or typechecking are inherently static concepts. I'm also not saying that this library should do static typechecking—that would be an absurd demand. I only meant that the wording is misleading.
Even more misleading is author's use of the term "gradual type checking", which has a well-understood meaning: the ability to add static checks to an otherwise dynamically-typed program.
Most programmers don't think "dynamic type checking" is a misnomer, while it is true that "type checking" itself leans towards a static connotation.
I've seen gradual type checking used both ways in the literature, actually. Wiki has the term defined for dual phase:
http://en.wikipedia.org/wiki/Gradual_typing
> Gradual typing is a type system in which variables may be typed either at compile-time (which is static typing) or at run-time (which is dynamic typing), allowing software developers to choose either type paradigm as appropriate, from within a single language.
I'm sure this is just poor writing (as Siek defines it, it should be from dynamic to static), but there is enough confusion here where you might bother using the term for adding stronger dynamic type checks to an otherwise less dynamically typed language (if you admit dynamic types as types, of course). Also, a dynamically checked type signature is the first step to a statically typed one (as long as your types remain weak enough that static typing is achievable in the future). So in that sense, it is "gradual" typing, just from a meta perspective :)
You can get a statically-typed Ruby here: http://infraruby.com/live
It follows Java's type system (including generics with bounded wildcards) but it doesn't support Ruby reflection.