5 ms·

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

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.

Ixiaus 12y ago
Dependent Types? Check out Idris.
- TheLoneWolfling 12y ago
  I shall have to. That being said, I don't care much for Haskell-based syntax.
  - saryant 12y ago
    Dotty is another option, a potential successor to Scala: https://github.com/lampepfl/dotty https://github.com/lampepfl/dotty
  - ixmatus 12y ago
    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.
  - kazagistar 12y ago
    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 https://www.youtube.com/watch?v=P82dqVrS8ik
cousin_it 12y ago
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%93Pratt_algorithm#Description_of_pseudocode_for_the_table-building_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 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.
- TheLoneWolfling 12y ago
  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.
  - deleted 12y ago
    [deleted]
- Dewie 12y ago
lmm 12y ago
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.
- ixmatus 12y ago
  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.
Sharlin 12y ago
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.
- groovy2shoes 12y ago
  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.
- Sharlin 12y ago
  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 http://en.wikipedia.org/wiki/Concepts_%28C%2B%2B%29 https://isocpp.org/blog/2013/02/concepts-lite-constraining-templates-with-predicates-andrew-sutton-bjarne-s https://isocpp.org/blog/2013/02/concepts-lite-constraining-t...
tomp 12y ago
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 http://goto.ucsd.edu/~rjhala/papers/liquid_types.pdf [2] https://www.cs.purdue.edu/homes/suresh/papers/vmcai13.pdf https://www.cs.purdue.edu/homes/suresh/papers/vmcai13.pdf [3] http://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pdf http://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pd... [4] http://www.kennknowles.com/research/knowles-flanagan.toplas.2010.pdf http://www.kennknowles.com/research/knowles-flanagan.toplas.... [5] http://sage.soe.ucsc.edu/sage-tr.pdf http://sage.soe.ucsc.edu/sage-tr.pdf [6] https://github.com/tomprimozic/type-systems/tree/master/refined_types https://github.com/tomprimozic/type-systems/tree/master/refi...
- ufo 12y ago
  > 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?

Ixiaus 12y ago

Dependent Types? Check out Idris.

TheLoneWolfling 12y ago
I shall have to. That being said, I don't care much for Haskell-based syntax.
- saryant 12y ago
  Dotty is another option, a potential successor to Scala: https://github.com/lampepfl/dotty https://github.com/lampepfl/dotty
- ixmatus 12y ago
  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.
- kazagistar 12y ago
  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 https://www.youtube.com/watch?v=P82dqVrS8ik

cousin_it 12y ago

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%93Pratt_algorithm#Description_of_pseudocode_for_the_table-building_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 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.

TheLoneWolfling 12y ago
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.
- deleted 12y ago
  [deleted]
Dewie 12y ago

lmm 12y ago

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.

ixmatus 12y ago
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.

Sharlin 12y ago

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.

groovy2shoes 12y ago
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.
Sharlin 12y ago
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 http://en.wikipedia.org/wiki/Concepts_%28C%2B%2B%29 https://isocpp.org/blog/2013/02/concepts-lite-constraining-templates-with-predicates-andrew-sutton-bjarne-s https://isocpp.org/blog/2013/02/concepts-lite-constraining-t...

tomp 12y ago

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 http://goto.ucsd.edu/~rjhala/papers/liquid_types.pdf [2] https://www.cs.purdue.edu/homes/suresh/papers/vmcai13.pdf https://www.cs.purdue.edu/homes/suresh/papers/vmcai13.pdf [3] http://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pdf http://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pd... [4] http://www.kennknowles.com/research/knowles-flanagan.toplas.2010.pdf http://www.kennknowles.com/research/knowles-flanagan.toplas.... [5] http://sage.soe.ucsc.edu/sage-tr.pdf http://sage.soe.ucsc.edu/sage-tr.pdf [6] https://github.com/tomprimozic/type-systems/tree/master/refined_types https://github.com/tomprimozic/type-systems/tree/master/refi...

ufo 12y ago
> 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?