So if I understand correctly, the real point is instead of programming defensively at runtime, you can do it in the type system.
My main question is the extent to which this is possible in more conventional languages.
My main question is the extent to which this is possible in more conventional languages.
C's language of types is incredibly primitive. Haskell's is quite nice. Agda/Idris/Coq's type language is technically equivalent to its value language so you can encode incredible things.
It turns out that due to people's general desire for compilation to always terminate that the type language behaves quite different from the value language. It also turns out that the type language operates differently because we're more interested in logical constraints than actual evaluation.
The major thing that the above change is that you no longer have the "it's always a Turing complete language" excuse. Type languages can actually significantly and meaningfully differ in power.
So it's meaningful to say that there are constraints that can be encoded statically in Haskell but cannot in C (no matter how you try). And it's also true that Coq can encode constraints that cannot be encoded in Haskell (though Haskell keeps making its type language stronger!).
Anyway, this was quite an enlightening comment for me: Agda/Idris/Coq's type language is technically equivalent to its value language.
Given a sufficiently interesting type language, could we statically type the problem I posed in another comment here
https://news.ycombinator.com/item?id=8966065
?
To encode what you're looking for requires type-level natural numbers and a reasonable notion of type-level equality. These are fairly non-trivial. You can encode this in Haskell, but type leve" equality is a bit hard to work with so you may suffer some pains (I know, I've done it several times!). Agfa and Idris would be where I would look to see this sort of thing materialize.
About your example, it's not idiomatic Haskell. If you try to code the same exact algithm in Haskell, you'll have the same exact problem (ghc has a warning for it); if you recode it in fmap or list pattern matching that are idiomatic to Haskell, you'll avoid the problem.
First, "Turing complete" means that you can compute anything anyone else can compute. It doesn't necessarily mean you can do it with a reasonable encoding, or do with it what you need to do with it. At the boundary between systems, encoding matters quite a lot!
Second, it's certainly true that there are constraints you can express in Haskell and not in C, but I was surprised by some of the things I could enforce in C with a little creativity.
And, yeah... even a type system as primitive as C can catch interesting invariants. This is an important counterpoint to the general idea that "types never say anything interesting".
Certainly. I had every confidence you understood that. I just wanted to be sure we avoided strengthening the "Turing complete means it can do anything any other language can" misconception.
If I understand you correctly, if the type system behaves the same as the value system, then it is possible for the compilation to never terminate. Do I have that right?
" I've been trying to get my mind around this kind of stuff for maybe a year. And I have to say that monads don't look like the solution to any of the problems that I actually face or have ever faced, in a thirty-year career." - https://news.ycombinator.com/item?id=8815973
You might be interested in this link:
http://haskellrescue.blogspot.com/2011/03/cooking-delicious-...
If you respond quickly enough and I can delete this, I will ;)
There are also some things that I'm not sure are reasonable at all in something like Java/C++ without writing a lot of code. For example: https://www.chrisstucchio.com/blog/2014/type_safe_vector_add...
x = r_[:n].reshape((3, -1, n/15))[:, :2].sum(axis=-1)
y = x + randn(m, 1, 2)
z = y - r_[:7]
I suppose this may have been tackled in Haskell in the Repa library, but I'd need to read papers like
http://benl.ouroborus.net/papers/repa/repa-icfp2010.pdf
to know. Hence my question if we could lift this into the type system in a conventional language, but I don't think it's possible in a general way.
Java is in an interesting place in that its type system is rudimentary but not unpowerful. C is a more useful didactic target---there really do exist invariants which can be encoded in Haskell types but could never be encoded in C types!
Another huge target is parametricity. You can write Java code which is "maybe sort of parametric" but it really isn't and subsequently you can never trust it because of the existence of things like global reference equality and hash codes (in the least).
Finally, there are expressivity concerns. Java cannot encode as many things in its type language as something like Agda (to make a clear comparison). You can simply note that Java's type equality is nowhere nearly as developed as Agda's!
As an example of using Java to indicate a fairly non-trivial invariant and comparing that implementation to Scala, Haskell, and C# consider Tony Morris' challenge
http://tonymorris.github.io/blog/posts/understanding-practic...
Just like regular old code helps you manage the relationships between an input file and an output file, the type system helps you manage the relationship between libraries, or sets of functionality in your code. I don't care what type of data you pull from the database, but that type must agree with the type of matrix you're constructing. The parser may return a syntactically correct tree, or an error. One use of the type system is to ensure that all possible error conditions are handled in a meaningful way.
You can do this in java, but haskell's type system is a bit more expressive, so it's easier to enforce higher level constraints.
Another way to look at it, the type system is like the algebra axioms you want your system to follow. if equality is reflexive, a == b, then also b == a. At that level we don't care if a is 5 or "hello" or @TcpConnection(0x1342341a).
It is substantially possible in more conventional languages, however the conventional languages have holes in them which can not be filled in by libraries.
For instance, a bog-standard approach in any OO language is to hide the raw constructor and give only mediated access via some other class method (or local equivalent construct). This can allow you to easily enforce constraints like "A CreditCardNumber either had its parity validated OR does not exist". If you then put methods on an object that allow you to only manipulate the object in certain ways that maintain the constraints, there will exist no (direct) way to violate the basic constraints of the object.
This is reasonably powerful, and mastery of this technique is something that I would consider to be core to considering yourself at least a mid-tier professional developer.
However, there are many constraints you can not enforce in conventional languages. You can not enforce via type whether or not a given call will do IO or access global variables in unexpected manners. You can not enforce via type that a given method will only be called in a certain context (key in things like transactional memory, where you'd better be doing your STM things inside an actual transaction or the whole thing breaks down). You can not enforce whether an object will or will not be shared across thread boundaries. And so on, for a wide variety of additional guarantees that can be provided by a stronger type system. In the exciting-but-experimental world of dependent typing, you can enforce at the type system that a number is even or odd and stuff like that.
There are many different additional constraints being explored right now across a wide variety of languages, and while functional languages are leading the way, and there are some solid reasons for that, it isn't just functional languages that can use this... for instance, see Rust, which isn't functional at all in the modern sense but can still guarantee some of the things I said above.
(Rust, for instance, bring a question to the fore that I've been interested in for a while, but haven't had a major language to check it with: Is the important thing about functional programming immutability, or is it controlling mutation carefully? If in practice the latter is really what's important, than it is possible to see a set of "immutable" languages and see them successfully control mutation but accidentally attribute that to the "immutability", because that's the mechanism we happened to be using to accomplish the mutation control. I've already previously explained why I believe Erlang definitely had this problem: https://news.ycombinator.com/item?id=7744109 but with Rust we can explore whether Haskell has the right of the argument, or if Rust-style mutation control will turn out in practice to be sufficient. But it will be years before we can even start forming a decent answer... Rust needs some large scale programs and a body of people with experience writing large-scale Rust programs before we can even start forming a solid answer.)