Hacker News Reader

Comment by hellofunk | Hacker News Reader

You can say that something is a floating point number (a type) but what if that something must be between zero and one? A type can't tell you that.

Typing has its place but the idea that it catches all bugs at compile time certainly isn't true; the cycle of running the app itself, running its tests, is just as important for statically-typed code as dynamically typed.

Languages that have a sophisticated contract system* (like Clojure's Clojure.spec library) have a bit of a leg up in my opinion. You can much more precisely explain and control and test for the specifics of all values flowing through your system well beyond merely what type they are.

-- * Clojure's devs don't refer to spec as a contract system because it is quite a bit more versatile than that, and some are actually using it for compile-time checks, compile-time generative testing, and other nifty things that aren't covered by a "contract" system.

View on HN

> You can say that something is a floating point number (a type) but what if that something must be between zero and one? A type can't tell you that.

Of course it can. The idea behind a decent type system is to make illegal states unrepresentable. You define a type which contains a value between 0 and 1 (lets name it `probability`) and make a function `float -> probability` which checks the range. That way, everytime you'll see `probability` in your code, you will know it is in the right range.

The problem with spec is that it can only verify what it sees on run time, whereas a static type system by definition has 100% coverage over your entire program.

You are talking about a function (at runtime), not a type, verifying the range. And you can do that in any language, regardless of its stance on typing.

http://www.adaic.org/resources/add_content/standards/05aarm/...

Compile-time and run-time floating point numbers constrained by precision and range. It's been a long time so I'm just going to include the examples in that document:

  type Coefficient is digits 10 range -1.0 .. 1.0;
  type Real is digits 8;
  type Mass is digits 7 range 0.0 .. 1.0E35;
  subtype Probability is Real range 0.0 .. 1.0;

These will be checked (to the limits of the ability of the system) at compile-time, and by default enforced at run-time. You can disable the run-time checks if you want for the sake of performance. The compile-time checks will "fail" to detect things where computations beyond the compiler's ability to reason might produce an invalid value.

Cool, but I don't know much about Ada, and would like to see an example for a statically-typed "range checker" in a more mainstream language used actively today. C++ templates can do a lot of magical stuff at compile time but such techniques are well beyond the reach of most developers.

I can't think of any typed language I've used or seen in active modern professional work where you could validate a value as part of a type at compile time.

Not without extra-compiler tooling like other static analysis tools, you're probably correct. I haven't had a chance to use much Ada, it's always been a pleasure for me to work in because I get to use things like the above to make my code so much clearer.

Pascal has integer range types, but Pascal hasn't been mainstream for a long time now.

I think you can get quite far in C++ with a class that has a constexpr constructor taking a double that checks for range, and (quite a few) operator overloads that allow one to do the normal operations on such quantities.

C# with "code contracts" allows you to annotate function arguments with valid ranges which will be statically checked at compile time. It's quite verbose though.

https://docs.microsoft.com/en-us/dotnet/framework/debug-trac...

> And you can do that in any language, regardless of its stance on typing.

Yes and no, because nothing prevents you from passing the wrong kind of value in an untyped language unless, well, you check for the runtime type yourself in the function and reject that. And you can only do that at runtime, at which point you'll not be able to immediately see where you're passing in invalid data accidentally unless you hit this exact branch in your code. So actually just the type tagging is quite useful already.

Also, it looks like more powerful dependently-typed languages like Idris[0] (and probably also Agda and Coq) can encode this information in the type system.

[0]: https://stackoverflow.com/a/28436452

what if that something must be between zero and one? A type can't tell you that.

Actually, it can, using dependent types :) I'm a Python fan, but Type-Driven Development with Idris has been a very interesting read.

Yes but there are no mainstream or production-ready dependently typed languages, so I didn't mention that. But I wouldn't be surprised if dependent typing really is going to be the distant future of programming languages. Perhaps not too distant.

I also wouldn't be surprised if Clojure tends to do surprising things in this area with taking Clojure.spec more to the compilation stage; some of the most interesting research into type systems has actually be done by lispers (i.e. Typed Racket, Core.Typed) and there is active interest in it among the Clojure community.

> Yes but there are no mainstream or production-ready dependently typed languages, so I didn't mention that.

(For a number-type that is limited to eg be between 0.0 and 1.0):

Ada?

http://www.adahome.com/rm95//rm9x-03-05-07.html

Ada provides ranged types but is not a dependently typed language. So I guess it sort of falls into this particular example, but would not apply to other examples in this arena.

> You can say that something is a floating point number (a type) but what if that something must be between zero and one? A type can't tell you that.

Sure, it can; many common numeric types include specific ranges, the fact that the range 0-1 doesn't match any common floating point type doesn't mean that it isn't one that could be a type.

> many common numeric types include specific ranges

Can you give me a mainstream language example?

Every fixed-size numeric type.

> A type can't tell you that.

Yes, it can! --- but you don't necessarily want to confound your program with such a thing.

The old adage about the cure being worse than the disease applies.

> Yes, it can!

Ok, how? Other than an Ada example, or dependently-typed languages that aren't use in production, can you offer an example?

Perl 6, for instance, supports subset types such as:

  subset Positive of Int where * > -1

OTOH, while some Perl 6 supports some static type checking, subsets of this kind seem to support only dynamic, not static, enforcement.

Such subsets are readily available in all dynamic languages I've used. But the issue here is really about compile-time checking these things, and that's a different animal.

> Other than an Ada example, or dependently-typed languages that aren't use in production...

Every time someone gives you an answer, you modify the question to exclude it. Eventually you will have excluded everything that refutes the fallacy in your original post, but it is still there.

    case class Probability(value: Double) { require(value <= 0 && value >= 1, "probability must be between 0 and 1" }

What's the language and what does "require" do? Is that a compile-time mechanism?

Reply on news.ycombinator.com