Hacker News Reader

Comment by TheLoneWolfling | Hacker News Reader

Personally, I wish that type systems allowed for arbitrary pure (as in "same input -> same output") code to define what is and isn't a valid instance of a type at compile time.

Being able to declare a function that is only valid for, say, power of two inputs (say: a hashmap's initial size, when the hashmap is using a bitwise and for wrapping) and having it actually enforced at compile time would be very useful.

I mean, even range types are useful.

View on HN

Any such system would need a theorem prover that's powerful and easy to use, and such a prover doesn't exist. For example, to implement an algorithm that involves arrays and indices, you'd need to supply machine-checkable proofs that all indices involved in the algorithm are valid for their respective arrays. That's really difficult, e.g. you can try to come up with some static reasoning scheme that would work on this algorithm:

http://en.wikipedia.org/wiki/Knuth%E2%80%93Morris%E2%80%93Pr...

The original paper on this topic is Hongwei Xi's "Eliminating array bound checking through dependent types", http://www.cs.bu.edu/~hwxi/academic/papers/pldi98.pdf . You will note that he failed to remove all bound checks in the algorithm, even though he started out with a good language (ML), added many manual annotations, and used a sophisticated method of automatically proving theorems. Also, his method and most subsequent methods will fail on any problem that involves multiplication of integers to get array indices, e.g. addressing a rectangular array as a[i*n+j], because integer arithmetic with multiplication is undecidable and even simple instances make the computer cry.

This is a hard research problem. If you come up with a language design that is guaranteed to be memory-safe, eliminates array bound checks in most realistic use cases, and can be used by regular programmers, you will be hailed as a hero. I'm not exaggerating at all.

Well, the thing is, anything would be better than what we have currently.

I know that in general the problem is undecidable. But we don't need to solve the entire problem to solve a large chunk of practical cases.

Even a simple runtime cast (with check) / asserting cast (a cast with an assertion that would be triggered at compile time if the compiler can find a valid counterexample, otherwise unchecked) combination would be miles above what we have now in most strongly typed languages.

> If you come up with a language design that is guaranteed to be memory-safe, eliminates array bound checks in most realistic use cases, and can be used by regular programmers, you will be hailed as a hero. I'm not exaggerating at all.

I'm just guessing, but wouldn't most uses of arrays be in traversing the whole array, ie mapping over the array, folding it etc.? I have seen a ton more

> for i = 0 to a.length -1

then I have seen something like indexing a sorted array like in a binary search. So if these operations are abstracted to functions that don't use array indexing directly, then they could perhaps be proven once in some library. And such a proof seems very straightforward (conceptually, perhaps not realistically) - just prove that your for loop exits when the index i gets incremented to out of bounds of the array.

I think Rust's iterators use no bounds-checked indexing underneath, at least for simple things like mapping over an array. They probably haven't proved that the indexing won't go out of bounds, though, probably just vetted and tested it a lot.

Yeah, Rust's iterators are a good example, and they indeed solve this specific use case.

(For those who don't know, an iterator in Rust has a function next() that returns an Option<A>. That allows you to do array bound checking and loop termination checking with a single operation, like when iterating over a linked list.)

Also I've seen a promising paper by Corneliu Popeea: http://gallium.inria.fr/~naxu/research/abce.pdf . It says it works on unmodified C code, doesn't require annotations, and successfully removes all checks in quicksort (!) Kinda sounds too good to be true though, I wonder what's the catch.

Not only quicksort, but recursive quicksort.

That indeed looks promising!

Elaborating on my previous reply.

The way I wish things worked:

Programmers code with three types of constraints: soft cast, hard cast, and unsafe cast. Soft cast is a runtime assertion that the constraint isn't violated, hard cast is a "do not compile unless you can prove that this constraint isn't violated" and unsafe cast is a "check at compile time to make sure you cannot provide a counterexample, but do not include a runtime check". Hard cast will be rarely used, for obvious reasons.

Compiler propagates known values / constraints forwards as much as possible, and propagates constraints backwards as much as possible. Note that this generally already happens as part of compiler optimizations. If at any point any value violates a constraint, error out and provide a "constraint trace" of what caused the violation.

After this step, the compiler looks at all unknown-at-compile time variables and randomly (or rather, pseudo-randomly, maybe seeded with the md6 of the file or something to be deterministic) generates and tests values (along with some common values - note that this could be integrated with a test framework built into the language!), ensuring that no constraints are violated. (There are a bunch of optimizations here that I'm not going to mention.) If any constraints are, error out with the variables required to violate the constraint and the values assigned to them.

This is too much machinery to build into a general-purpose compiler today, but there are static analysis tools (see Frama-C and the like) that will analyze your program text (optionally with annotations like you've mentioned) and figure out constraint violations.

In general, what you want to be able to mix types and values are dependent types (see languages such as Coq, Agda, Idris). However, dependent types are way too powerful, and as such extremely difficult to use.

A light-weight form of dependent types are refined types, which are essentially dependent function types that have contracts on their parameters and return types. As refined types are way more limited than full dependent types (essentially, linear arithmetics, logic, and simple stuff like this), you don't always need to write the proofs manually but can use an automated theorem prover such as Z3.

This is a hot research topic. There are attempts to do type inference for refined types - see [1] and [2]. The Liquid Haskell team is also exploring the issue of dependent types and laziness [3]. Below you mentioned that you want "soft casts" as well - check out [4], which attempts to do just that (implemented in language Sage [5]).

I'm very interested in this topic as well, and have experimented a bit [6]; as it turns out, it's not that hard to implement a basic type-checker for simple refined types. It's also quite powerful - using Z3, even non-linear problems such as rectangular array access (mentioned by a poster below) are solvable, since you can trivially prove its safety using real arithmetics (which is decidable).

The only big disadvantage that I see is the difficulty with dealing with state, but then again, even programmers can't reason about it properly; I mean, if `x` is a mutable object, can you really say `if x.a != 0 then 1 / 0` and be sure that no-one will modify `x.a` in the meantime from another thread? I hope that linear types could help.

[1] http://goto.ucsd.edu/~rjhala/papers/liquid_types.pdf

[2] https://www.cs.purdue.edu/homes/suresh/papers/vmcai13.pdf

[3] http://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pd...

[4] http://www.kennknowles.com/research/knowles-flanagan.toplas....

[5] http://sage.soe.ucsc.edu/sage-tr.pdf

[6] https://github.com/tomprimozic/type-systems/tree/master/refi...

> A light-weight form of dependent types are refined types, which are essentially dependent function types that have contracts on their parameters and return types

I had never seen it written that way. What can full dependent types do that you can't do with refinement types?

I'm not sure, as I'm not really knowledgeable in programming with full dependent types (as in Agda, Idris, or Coq).

However, I can point you to this discussion on Reddit [1]; essentially, one user (kamatsu) is saying that refinement types are not dependent types:

> More or less, if you have sigma and/or pi types, then you have dependent types. If you don't, you don't.

Also, he claims that a crucial difference is that dependent types are proofs, while type-checking refined types requires proof search. Then, another user (neelk) points out an article [2] which claims (I haven't read it) that dependent types can be encoded using singleton types, which can be written using refined types.

[1] http://www.reddit.com/r/programming/comments/26se9k/refined_...

[2] http://www.iro.umontreal.ca/~monnier/comp-deptypes.pdf

Your example is perfectly possible to implement in most languages; you just can't expect to give a function an arbitrary run-time integer value and have its validity checked at compile time :) So, the type would have to look something like this:

    class IntegerPowerOfTwo {
      private int exponent;
      public IntegerPowerOfTwo(int exponent) {
        this.exponent = exponent;
      }
      public int toInt() {
        return 1 << exponent;
      }
    }

If you want a compile-time conversion from a constant integer to an IntegerPowerOfTwo, it is possible with C++, for instance, although you need a bit of template metaprogramming.

I'm not sure why you're being downvoted. This technique is not entirely unlike using a phantom type, which is a common way of encoding such constraints into the type system.

I'll admit it's not ideal; in fact, it's often downright cumbersome. In some cases, it's not possible to encode desired information into a particular type system.

But in this case, it seems valid to me. There is no way to construct a value of IntegerPowerOfTwo that does not represent a power of two, and therefore it fulfills GP's example requirement.

I'd like to know why this was downvoted. (Edit: other than the fact that the exponent should be unsigned int :/)

The whole point of encapsulation is to be able to write data types that have invariants other than those offered by the machine-level types. If you want a type T that satisfies the predicate

    ∀n∈T: ∃k∈N: n = 2^k

then you write a type that only provides operations that maintain the constraint. In this case, for instance, construction from k and multiplication by another T. As I said, some languages like C++ do also allow things such as compile-time conversion of an unconstrained constant integer into a power-of-two integer, with a compile error if the constraint isn't satisfied, but in my opinion that's mostly syntactic sugar. Would be nice if you could simply write, say,

    type intPowerOfTwo = unsigned int where ∀intPowerOfTwo n: ∃unsigned int k: n = 2^k

but what about the unsigned int operations, such as addition, that do not maintain the invariant? Should the type system include a general theorem prover that can deduce which operations are allowed?

However, I understand this was simply an example and do agree that expressive and powerful type systems are certainly a very useful tool. C++ template metaprogramming (pretty much computing with types as values) is very impressive even if horribly ad hoc and the concepts feature (constrained templates), if ever actually implemented, will make all kinds of things easier.

http://en.wikipedia.org/wiki/Concepts_%28C%2B%2B%29

https://isocpp.org/blog/2013/02/concepts-lite-constraining-t...

Dependent Types? Check out Idris.

I shall have to.

That being said, I don't care much for Haskell-based syntax.

Dotty is another option, a potential successor to Scala: https://github.com/lampepfl/dotty

To each his own. I rarely hear fluent Haskellers say they don't care for the syntax though; if you haven't really gotten far enough to write production code in Haskell that leverages Haskell's powerful abstraction features, then you should and you might find the syntax growing on you.

The syntax is nice because it enables the programmer to express software in a terse way, generally favoring the types as documentation and a strong mental model to understand the abstraction.

It is also a lot of work to prove your code. Here, have a nice Idris video to give you a taste: https://www.youtube.com/watch?v=P82dqVrS8ik

You can do that in Scala (though it won't necessarily be easy). Just require an implicit parameter that witnesses whatever constraint you want, and define basically functions at the type level that supply it.

You can do "kind of" dependent types in Haskell too but it's an ugly mess (like trying to do it in Scala). Idris handles it really well for general programming tasks.

Reply on news.ycombinator.com