I bet the 10000 Ruby guys are gonna create a big, unmaintainable, broken mess. Even Java's primitive type system would be a big help when it's about software development at scale.
Yes yes, TDD :)
I think Rust and Swift and Elm strike the right balance between developer productivity and a strict type system that actually improves the quality of production software.
Those are not the kinds of problems a type system is intended to solve. Those are problems of data, not of types.
The amount of boilerplate in a Java program is pretty low if you aren't trying to abuse or work around the type system. It certainly is not 10x what you end up with in Ruby or Python. Java 8 has made significant improvements, but it wasn't that bad before in many cases.
Instead of trying to work around Java's type safety, you should learn to use it properly. Good programmers think about types whether or not they are forced to by the language, so the restrictions imposed by Java should not be burdensome -- in general, you should already be mentally applying some of those restrictions to your code so you can avoid passing the wrong types around.
Java's boilerplate comes from lacking type inference and from having a type system that is too weak, not one that is too strong: I'd argue that people's love for dynamic languages without type systems is cause by how people's idea of what types are, and what they do for you, come from Java and old C++, as opposed to something more powerful.
Many people misunderstand the option type in Java. It was created to make stream processing easier. It was not intended for general use, as in other languages.
Regarding illegal arguments, they are unavoidable in any type system. Suppose you defined a function that splits a string into an array of n-grams, to which you pass the string as well as int n. If you pass an n which is greater than the length of the string, no type system will help you figure out what to do. It's just an invalid/illegal argument, and you will either have to decide what to return for that case (maybe an empty array, or even... null), or throw some kind of exception.
Regarding illegal arguments, have a look at something like Idris, which has a type system with "dependent types". The Wikipedia page has an example[0]; types can have values, so you can express a "pairAdd" function that accepts two vectors, each vector requiring the same length.
I guess "types" and "compile-time checks" are sometimes used interchangeably. I absolutely think tools (such as compilers) should be leveraged to provide as much assistance as possible; whether that comes in the form of types, or some other mechanism that resembles types.
[0] https://en.wikipedia.org/wiki/Idris_(programming_language)#D...
Go for example, half-straddles this world too.
I can half-see the benefit of being able to know if something produces an error term (annoying in Python when you're trying to be thorough with exception handling) but conversely there's so few situations I encounter where a function can't error that it's practically irrelevant - what does it matter to me that some set of functions can't throw, if every bit of IO, network and disk before them can and will at some point?
I hope you can see how this is pretty much the same as checking if a variable is null. It takes just as much work, and has the same outcome.
This means the language allows you to define areas of your program that are null-safe, and areas where nulls are expected.
Compare to languages where you must remember to check null on every use of a null variable. I guarantee I can pick any Java codebase and find a method where arguments to that method, or a class's properties, are not checked for null on every use. How do I know that the use is safe? Usually by coding conventions; maybe immutable instances represented by values set only in a constructor, although what's to stop null being passed in?
In cases where the value could be missing, the type is change to Maybe and the caller is forced to handle the null case. They can still avoid explicit checks using various combinators (>>=, fmap, liftA2 etc.) which propagate empty Maybe values. Explicit matching on Maybe is fairly uncommon in languages which support it.
1. the large number of values that you now know definitely have a value, and you can access without fear that they don't.
2. the helper functions for Maybe that let you deal with optionality in various ways; the possibilities are extensive and useful. null doesn't give you any help, and generally any helper syntax is limited to one or two possibilities.
3. Code cannot fail due to trying to access a null pointer accidentally. Functions that definitely return a value (ignoring severe issues like OOM, etc.) is a somewhat useful property.
Let’s say your application tracks users, and each user needs to have at least one address. On top of that, they must flag one address as their default address, which is used when sending them formal communication, but usually they can pick which address they want to use. (Most people have one address which is their default).
The Java code to pick out a user’s default address is simple enough:
class User {
// ...
public Address getDefaultAddress() {
for (Address address : getAddresses()) {
if (address.isDefault()) {
return address;
}
}
throw new AssertionError("User has no default address");
}
}
Then one day we receive a change request from a client. Some users move around a lot, and have no permanent address, and they’d like it to be changed from at least one address to at least zero addresses. Basically, make it so users don’t have to have an address anymore.
How does this affect our getDefaultAddress function? It has to handle the case where users have no addresses, because if that’s the case, then they’ll have no default address, either.
The easiest way to do it is just return null instead:
public Address getDefaultAddress() {
for (Address address : getAddresses()) {
if (address.isDefault()) {
return address;
}
}
// no default address
return null;
}
Or we can use Optionals:
public Optional<Address> getDefaultAddress() {
for (Address address : getAddresses()) {
if (address.isDefault()) {
return Optional.of(address);
}
}
// I know I could use Java 8 streams here, just go with it :)
return Optional.empty();
}
This is precisely what happened to us. Changing the method to return null resulted in lots of breakage from code that we forgot to add null checks to and code written afterwards using the old signature by accident. Changing it to return an Optional meant we were forced to update everything, otherwise it wouldn’t compile. No runtime bugs. No developer slip-ups. That’s why I’m in Team Optional.
nGram : {l : Nat}{n : Fin l} -> Vec l Char -> n -> List (Vec n Char)
"nGram" is the name of the function
"{l : Nat}" means l is a natural number
"{n : Fin l}" means n is a finite number smaller than l
"Vec l Char" is the first argument, declared as a
vector of characters, with length l
"n" is the second argument (previously declared as
a finite number smaller than l)
"List (Vec n Char)" is the return type, a list which consists
of vectors of characters where each vector is of length n
http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWo...
The first is more about programming in Agda while the second goes into how dependently typed languages relate to logic. Together they provide sufficient definitions of Nat, Fin, Vec and List to declare the nGram function.
If you're unfamiliar with ML-style syntax the above definiton probably looks weird, but can be written in a pseudo-java style like this:
List<Vec<N,Char>> nGram<Nat L,Fin<L> N>(Vec<L,Char> input_string, N n){}[1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
Dependently typed languages allow for type-level functions (actually they erase the separation between type-level and value-level). This is why you can define a type like "Fin n" meaning a number smaller than n. "Fin n" is a function that takes one argument "n" and returns a type that limits its values to the set of (natural) numbers smaller than n.
Arguably, Agda is more often used as a proof assistant, rather than as a programming language (although I've had the pleasure of watching Ulf Norell implement a limited programming language interpreter in Agda, using non-total functions, which was quite nice.) But Idris is a serious effort to create a language that's both dependently typed and performs decently when used as a regular programming language.
If you want to see some real world examples of using dependently typed languages, I would suggest looking at the CompCert C Compiler[0]. It is a C Compiler that's been formally verified using the Coq proof assistant, which is a precursor to both Agda and Idris. Coq is as far as I know the first dependently typed language.
To be fair, programming in a dependently typed language usually requires more effort upfront, but the ability to encode properties that are usually considered runtime errors into the type system does seem like an interesting future for programming languages.
[0] http://compcert.inria.fr/compcert-C.html
(edit: shout out to the excellently named sibling commenter "curryhoward", IMHO one of the most interesting results in programming language technology and type theory research!)
Idris allows you define types whose definition depends on a value - these are called "dependent types". This allows you to define a type such as "a pair of integers, where the second integer is greater than the first".
So, in your example, you could define an immutable String type that stores its length as a fixed value. Then, you define a function that accepts a String of length "len", and a Num (or Integer) with a value that must be less than "len". The type signature might look something like this (if I understand the syntax correctly):
ngram : String len val => Num (a <= len) => Vect Num StringTherefore, there cannot possibly be a way to avoid the problem I described in my example, unless your program exists in a a closed world where there are no inputs, and the values of all variables are defined before compilation.
The word "total" invokes the totality checker[0] which will report an error if the function doesn't cover all possible cases or cannot be (automatically) proven to not enter an infinite loop.
(Also, bear in mind languages like Haskell use "lazy" or "non-strict" evaluation by default, where values aren't evaluated until they're actually needed; kiiiinda like Streams?)
I'm certainly not an expert on Idris, but I imagine dependent typing provides two benefits:
1) The type signature (which is separate from the implementation; kind of like an Interface in Java) can enforce constraints on your implementation. So, if you define a function with type sig of "Int a => Int b => (a + b)", your implementation must ensure that the returned value is equal to the sum of the two inputs.
2) You can look purely at the type signature to understand what a function is doing. Looking at that type signature above, I can see I want to use that function for addition, not multiplication.
Anyway, I'm absolutely not doing justice to these ideas (mostly because I'm not well acquainted with the languages). If you're curious at all, I would highly recommend taking a course on functional programming as a minimum; once I realised that names are meaningless in code, you start seeing everything as reducible to very similar type signatures, which makes you yearn for a language that lets you write your boilerplate once, in a polymorphic way (beyond generics).
That would make many practical, real-world programs noncompilable. Any program which accepts data via API calls, or even reads strings from STDIN, cannot know what values are going to be passed to it before it runs. Compilers cannot predict the future.
This statement is false. I recommend reading about dependent types, which enable exactly what you claim is impossible.
It's true that in every mainstream language, the type system is not powerful enough to reason about types that "depend" on values, such as the type of MxN matrices, sorted lists, prime numbers, etc. But don't limit your sense of what is possible by your experience with mainstream languages; most have rather limited type systems compared to what we know is possible in theory.
That is a true statement for any program that accepts input, strictly speaking. The halting problem is unsolvable.
The halting problem cannot be solved in general, but some programs can be proven to halt (or not halt). That's how the first few Busy Beaver numbers were found.
For something more substantial: a correct program that implements a regular language recognizer will always halt eventually on any input, because it always makes progress and doesn't have any nonterminating loops. It consumes the whole input and stops.
The hard part is proving you wrote it correctly, but that's what coq et al are for.
Analogous statements are true for programming in a dependently typed language.
https://www.infoq.com/presentations/Null-References-The-Bill...
In Common Lisp if you declare an argument to be a string, it is an error to pass NIL. You have to declare the type to be "(or string null)". That's exactly what the Option type provides.
Please tell me how it works, then. I guess you could easily find a counter-example.
First things first. Optional arguments are handled by &OPTIONAL and &KEY parameters, which can be used to provide defaults values as well as a flag indicating whether the argument is provided. The most used default value is probably NIL. NIL belongs to the SYMBOL, NULL, LIST and BOOLEAN types and their supertypes (ATOM, SEQUENCE, T). If you really want, you can include it in a custom type too. For most uses, the type (OR NULL U) is regarded generally as an optional U. This is consistent with the definition of generalized boolean and lists (a list is an optional cons-cell). If some corner cases, you have to use another sentinel value or use the third binding in &OPTIONAL and &KEY argument bindings. This is hardly a problem if you have a type U such as (TYPEP NIL U), but for most useful cases, (TYPEP NIL U) in fact returns NIL.
Here below I define a function FOO which accepts a string and prints it:
(defun foo (x) (print x))
(declaim (ftype (function (string) t) foo))
(declaim (ftype (function (or null string) t) bar))
(ignore-errors (foo nil))
NIL
#<TYPE-ERROR expected-type: STRING datum: NIL>
;; Does not print anything else
(ignore-errors (foo nil))
NIL
;; prints "NIL"
Break 1 [2]> (declaim (ftype (function (string) t) foo))
NIL
Break 1 [2]> (defun foo (x) (print x))
FOO
Break 1 [2]> (foo "hello")
"hello"
"hello"
Break 1 [2]> (foo nil)
NIL
NIL
Break 1 [2]>
There were no errors. The function accepted nil and printed it. You must have some other type restrictions going on than what you mentioned. The output is the same whether I put the declaim statement before or after defun foo.
(defun foo (s)
(check-type s string)
(print s))