[curryhoward]

When most practitioners think of "typechecking", they typically think about proving properties about programs statically. This project seems equivalent to adding a runtime check at each call site to ensure the arguments and return values are the correct type.

This is certainly useful sometimes, as it gives programs the desirable "fail fast" property. But it isn't "typechecking" as most engineers understand it. Or at least, it should be clarified that this is run-time typechecking. As such, it negatively impacts runtime performance, unlike compile-time typechecking.

This project also seems to miss the primary opportunity of run-time type checking: checking properties that are difficult to prove statically! For example, checking that a number is even, that a string is lowercase, that an index is within the bounds of an array, etc. These exotic types require a dependent type system to be checked statically, but in a dynamic environment they are trivial to verify.

Two suggestions for improvement: 1) add "sum" types (i.e., discriminated unions), and 2) let the user define their own types via lambdas, such as PrimeNumber.

[girvo]

> When most practitioners think of "typechecking", they typically think about proving properties about programs statically. This project seems equivalent to adding a runtime check at each call site to ensure the arguments and return values are the correct type.

It basically seems equivalent (albeit somewhat nicer in a few ways, ie. scalar types are supported) to PHP's "type hinting"[0]. I will say that it is useful, in combination with unit testing, as you can pick up on problems with things slightly easier than hoping for the best in production and tailing error logs, but proper static type analysis is more useful.

[0] http://php.net/manual/en/language.oop5.typehinting.php

[foolfoolz]

editor support for php type hinting and phpdoc method comments goes a long way. intellij can do significant refactors and and searching. you'll get real time feedback for violating types. it's not quite the same as a explicit compile step but pretty close

[girvo]

Komodo IDE helps with that, but I personally switched to HHVM and have a simple bash script that swaps the `<?php` for `<?hh` and back, so that `hh_client` can statically tell me about problems, even when I'm not using any of the Hack features. Works a treat, to be honest!

[rtpg]

One thing we've applied on a Python(2, unfortunately, so can't go deep on the static type analysis) is enable this sort of type hinting when running our app in debug or test mode. Obviously can't catch everything, but it catches some of the sillier bugs.

[jbbarth]

Would you share how you did that technically in Python? Maybe some code example or a lib to recommend? decorators? assertions?

[rtpg]

python's warnings library is good for this

For example, in our application code, we'll use a warning for some type coercion for example

    if isinstance(obj,Bar):
        warnings.warn('Using a Bar as a Foo!')

In production, this will just print a message to the log. So this is useful for things like phasing out old behavior, where we try to stop using it but don't want hard failure if it's used for now.

But in our tests, we do want hard failure (so we can phase out the behavior as much as possible before removing the functionality). So we do something like the following:

    if TEST:
        warnings.filterwarning('error','Using a Bar as a Foo!',RuntimeWarning)

Which basically says "if I receive a warning matching the regex given, then raise an error instead of just logging". So if I hit that code path during tests it will fail the test.

It's very useful, even if warnings is a bit too much about regex matching for my tastes

[seanmcdirmid]

This is kind of pedantic. What programmers think of and find useful as types and type systems is quite different from what type theorists think.

[kpmah]

It's not pedantic at all. It's a very useful distinction. Personally I thought this was static checking and got the wrong idea from the submission title. I can see some other comments here have made a similar mistake.

[nahiluhmot]

I would definitely find what curryhoward described as useful, but I don't think Ruby is that language in which it should) be implemented.

That being said, sum types would be a nice addition to this library.

[seanmcdirmid]

I was only referring to the starting quote:

> 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.

https://www.youtube.com/watch?v=__28QzBdyBU

[curryhoward]

Perhaps it's true that many programmers don't realize the fundamental connection between typechecking and theorem proving (i.e., that they are the same thing). But that wasn't meant to be the point. The point is that when most programmers hear the word "typechecking", they think of compile-time typechecking. This word is usually used in a static context.

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.

[seanmcdirmid]

> The point is that when most programmers hear the word "typechecking", they think of compile-time typechecking. This word is usually used in a static context.

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 :)

[infraruby]

> I would definitely find what curryhoward described as useful

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.