Types are theorems, programs are proofs.
(The code examples here use idris https://www.idris-lang.org)
To augment testing with a finite number of inputs we write mathematical proofs that demonstrate their correctness on all possible inputs.
The programmer writes the proofs and the compiler checks the proofs as it builds the software.
In this Go Experience Report I am going to make a case for sum types over multiple return parameters.
I wrote a little tool which does some analysis of Go source code:
Interfaces only allow you to model based on method set and they are, by design, open. Any type that satisfies the interface, satisfies the interface. They share some similarities to sum types, but, as far as they do, they are, essentially, infinite sums. While this often desired, there are times when you need to limit the options to a closed set of types.
There's no direct way in Go to say "these types, even though they share no methods in common". You have to use an interface{}, which says nothing—even though you know exactly what you want to say. You have to handle an invalid case at runtime.
There's no direct way to specify only the types in this package. Using an interface with an unexported "tag" method gets you part of the way. There's still nil and embedding and, at every point, those need to be dealt with—or, all too often, ignored.
These cases can lead to trivial errors that could be caught by the compiler, but instead need to be handled by defensive coding and extensive testing. Defensive codin
This is what the [official documentation][1] says about the terminate/2 callback for a gen_server:
This function is called by a gen_server when it is about to terminate. It should be the opposite of Module:init/1 and do any necessary cleaning up. When it returns, the gen_server terminates with Reason. The return value is ignored.
Reason is a term denoting the stop reason and State is the internal state of the gen_server.
Reason depends on why the gen_server is terminating. If it is because another callback function has returned a stop tuple {stop,..}, Reason will have the value specified in that tuple. If it is due to a failure, Reason is the error reason.