I find the (implicit) premise that you might not already care about types hard to believe... Migrating a JavaScript project of any complexity to typescript almost always reveals errors "for free" because of the typing. Certainly any experience hacking on python would also teach you the lesson of declaring your types ahead of time.
Is this old-fashioned thinking? Are types the SQL of yesteryear (in the context of the crazy rush to "web scale" mongodb)?
It feels like I already know what is going to go in where, and having to type it is just a waste of time.
That said, when I have to work with APIs that can not guarantee their data integrity throwing in a quick @flow annotation of top of the file, and taking the time to write out what is optional has proven very valuable to make sure my functions, and subsequent code is not going to throw.
Another reason I like flow more is because I don’t need to convonce my team to use it, I can just use it myself, and then delete it after I am done writing my code.
int* increment(int* i, int step)
{
return i + step;
}
Even Haskell's type system can't tell what you intend:
increment i = i + 11;
A unit test would clarify the intent of both these functions, and catch both bugs fairly reliably (if they aren't the intended behavior).
Ultimately I think TDD and types guarantee different things, and both are useful/needed.
Proving Programs Correct Using Plain Old Java Types, http://lambda-the-ultimate.org/node/5387
Obviously you have to be willing to use types to express intent, but even if you're willing, types are limited in what kinds of intent they can express.
int* increment(int* i, int step)
{
return i + step;
}
int* increment(int* i, int step)
{
return prt_add(i, step);
}
To be clear, my question is, how would you reasonably catch the typo with types in the following Haskell function?
increment x = x + 11;
def test_increment(x):
assertEqual(increment(x), x - 1)
def test_increment(x):
assertEqual(increment(x), x - 1)
If you write the wrong test or the wrong type AND the wrong implementation, they won't help you, but the point of both types and tests is that you have to make two mistakes for a bug to get into production. It's possible that in your test, I could have made the same error in the implementation of `increment`, but it's a great deal less likely than making that error in just the implementation or just the test.
And to be clear, I'm not saying any of this as a "types versus unit tests" thing. I've specifically said that both are useful and needed for reliable software.
> The answer to your question is, you can't. In this case the implementation is the specification. You're going to have to set a more meaningful challenge.
You totally can catch this bug with some type systems (Coq, for example), it's just much easier to catch this bug with a unit test in most languages.
I think that your boss would probably disagree with you that this bug is not meaningful if it makes it into production. You don't get to pick and choose which bugs are meaningful because they don't support your views.
def increment(x):
return x + 1
def test_increment():
assert increment(0) == 1
assert increment(1) == 2
assert increment(42) == 43
assert increment(-5) == -4
> Therefore, I think your point would be better demonstrated using a more complicated example.
The example is a simplification of a bug I came across last year:
available_date = datetime.date.today() + datetime.timedelta(days=11)
The intern who wrote the code didn't know how to use mocks to mock out `today` so they didn't write a test, resulting in this bug. I remember this case because I use it as an example to teach mocks.
I simplified my original example to make it clearer, but I think you'll see that this real-life bug suffers from the same difficulties if you try to verify it with a type system, but is (fairly) easy to test.
EDIT: Actually, the relevant bits of the test were fairly simple (from memory so please excuse errors):
@unittest.mock('datetime.date.today')
def test_available_date_set_to_tomorrow(self, today):
today.return_value = datetime.date(1984, 4, 20)
[...]
ticket_claim = claim_ticket(user, voucher)
self.assertEqual(
ticket_claim.available_date,
datetime.date(1984, 4, 21),
)In other contexts without polymorphic types, like with C, I'd wrap the input and output types in custom structs that expose trusted operations. The more minimal the better. It's definitely more cumbersome without polymorphism, but you do what you can for the code that's mission critical.
increment x = x + 11;
In C, my first thought would be to define a static value representing ONE, checked via static_assert, and then the increment function becomes input + ONE.
I'm a bit out of my comfort zone with this one so I may be wrong, but wouldn't that require a lot of coding to define type level naturals for all the possible values of X?
> In C, my first thought would be to define a static value representing ONE, checked via static_assert, and then the increment function becomes input + ONE.
Okay, but do you agree that in this case a unit test would be a better solution?
I'm not saying this as a types versus unit tests sort of thing. I'm saying both are needed tools for writing reliable software.
Not for your simple example. See [1] for more info. There are a number of packages that do the work for you.
[1] https://wiki.haskell.org/Type_arithmetic
> Okay, but do you agree that in this case a unit test would be a better solution?
Depends how mission critical the property is. Even simple increments and offsets might deserve some type-level encoding if they are core, mission critical properties.
For other things, tests are fine, although I recommend property-based testing frameworks like QuickCheck, Hypothesis, etc. which test logical properties against a large range of input values instead of a static set of values encoded into your tests.
On the other hand, I don't see that they'd actually be useful for catching this error in any way people are likely to use, although I'd be interested to see attempts...
On the third hand, the way I'd actually implement this in Haskell is probably `succ`, so typo would be caught during compilation. But of course you can construct alternative examples.
To my mind, types and tests are very much complimentary - ideally tests check that your solution gives correct answers at some points in your domain, while types help make that space more uniform (so if it's correct at some points it's more likely correct at others). There are some practical cases where the types sufficiently constrain things that checking any actual points is redundant, but that's not the common case.
Yeah, this is my ultimate point, and I worry that some people have misunderstood my intent. I'm not criticizing types: I think they're a very important tool. I'm saying that types don't handle every kind of possible error. And conveniently, tests often cover the kinds of errors that types don't (and vice versa).
It’s a one-liner in Haskell (two if you count the DataKinds pragma):
data Nat = Z | S NatRegardless, even with Java's limited expressiveness you can encode some powerful propsitions, as the paper I linked shows.
The paper you linked uses Java's type system for a mechanized proof, meaning...you probably don't want to be writing that out by hand.
I think that's overstating it a little too. You don't have to use the dependent types, at their core, Coq and Agda are still functional languages and you can just stick to algebraic sums and products and still enjoy type inference. Most people aren't using these languages for general purpose programming because a) poor tooling, and b) because they are explicitly marketed as research languages.
Strong/weak types and dynamic/static types are really two different spectrums. People conflate strong types with static types and weak types with dynamic types, but they aren't really the same thing.
Static/dynamic just has to do with whether the types are checked at compile time or run time. Examples: Static: C, Haskell. Dynamic: Javascript, Python.
Weak/strong has to do with what kinds of checks the type system does. A strong type system is capable of checking a lot of different things for you. Static types are often stronger, but not always: for example, C is statically typed but its type system checks hardly anything: int* + int is perfectly valid. A list of programming languages from weakest-typed to strongest-typed might look something like: JavaScript, C, C++, Common Lisp, Perl, Scheme, Ruby, Python, Java, C#, OCaml, Haskell.
Static types are nice for projects which will grow large and where bugs are a big problem, but I think for the average HN person, static types aren't really necessary.
Strong types, on the other hand, are extremely useful. Even in a dynamically typed language, they aid in debugging a lot, because type errors occur much closer to where they're caused. In Python, for example, `"foo" + 42` immediately fails. But in JavaScript, you don't get an error until much later, perhaps when your webpage is mysteriously displaying "foo42".
Of course, there's a small cost to strong types: in the case where I actually do want to append a number to a string, I have to do `"foo" + str(42)`. But I think people tend to overstate this cost because it's visible. But if you look at the big picture, typing five extra characters takes a lot less time than debugging almost anything.
"This doesn't have a formal meaning, therefore it's not useful" is quite a logical leap you've got there.
I've got over a decade of professional programming experience in which "strong types" is a useful enough concept to help me do my job. "Soundness" certainly gives stronger guarantees, but it's more than I've needed.
I'm not aware of "expressiveness" having a formal meaning, but my informal definition has functioned for me so far.
It means that everyone defines strong and weak in their own way, which has happened in every type system debate I've seen over the past 15 years.
> "Soundness" certainly gives stronger guarantees, but it's more than I've needed.
Soundness is exactly the metric you need. Either you can rely on your type system not to lie to you, or you can't.
Programming language expressiveness means "Felleisen expressiveness". It's a metric approximated by source code compression, which is why the great programming shootout includes gzip metrics for source programs.
Okay, that's fair. Part of the reason I gave examples and defined the spectrum I was talking about was to address this problem, because I know people don't necessarily know what I'm talking about.
import Control.Monad
import Control.Monad.Tardis
import System.Random
-- A solution for the Trapping Rain Water problem employing
-- the bidirectional state ("Tardis") monad.
-- https://www.geeksforgeeks.org/trapping-rain-water/
volume hs = sum . flip evalTardis (0, 0) . flip traverse hs $ \h -> do
x <- min <$> getPast <*> getFuture
modifyForwards (max h)
modifyBackwards (max h)
pure (max 0 (x - h))
main = replicateM_ 20 $ do
n <- randomRIO (3, 10)
hs <- replicateM n $ randomRIO (0, 10 :: Integer)
putStrLn $ show hs ++ " => " ++ show (volume hs)
There's also the self-documenting aspect of strongly typed languages: for instance, if I look up the documentation on a javascript API, I have to hope function parameters have been specified well, otherwise I just have to guess what should be passed in or dig through the source. With a strongly typed language I probably get that information as part of the autocomplete hint.
And good type systems can be powerful tools. In Swift for example, the protocol system is powerful enough that I'm sure it results in writing less code overall, not more.
Python has the dynamic typing problems, but is better because it has a somewhat strong type system. It will tell you when it's wrong, but often too late (oh this function only gets called wrong once every 100h on my server, thank you for telling me now that it went wrong). And sometimes different types can duck into the same function (e.g. string and list are both iterable).
So yeah, Python suffers from the same issues when you want to scale your code, but it's A LOT less bad than JavaScript.
Concrete example: Common Lisp is very strongly typed. So it almost never automatically converts from type to another, except when it makes total sense (i.e. the square root of -1 will return a complex number).
So, if there is a type mismatch, it will be caught (at runtime) raising an exception. Now, you would think "yeah but my statically typed language will check this BEFORE the code runs". Yes, but in Lisp, the exception doesn't terminate the execution, it enters a mode in which the system asks you what to do next.
Thus, what you do is, you go back to the source code, to the function with the error, you correct that specific function, compile that specific function (which happens almost instantly), and then resume execution of your program. This means that the previously "invalid operation" will be run again but with the new definition of your function, thus the code will continue running without said bug.
So, all in all, it's very nice to use...
For user-facing code running at scale catching more errors at compile-time still sounds better to me.
In particular OOP is very much helped by static types.
Clojure would a better example of a dynamic language that would not be improved by adding static typing. Namespaces, functions and immutable data (as well as pervasive use of data instead of wrapping it in classes) lessens the downsides I bump into continuously when doing javascript development.
This is what allows reuse.
- The vast core library of functions that manipulate those data structures can be used for everything in your program, cos it's all data.
- Most clojure libraries take and/or return data, reducing the need for clumsy adaptors, or even worse not being able to get at the data you need cos the library writer was really enthusiastic about encapsulation of everything they thought was of no use to consumers.
- You don't have a person class, you have a map with a first name and last name. Now the function that turns first + last name into full name can be reused for any other map with the same keys. (A rather spurious example, but a real one would take a large codebase and an essay to describe)
I can only recommend watching some of Rich Hickey's talks, particularly these ones, they're not entirely about types, but they express the above ideas much better than I can:
- Simple made easy https://www.infoq.com/presentations/Simple-Made-Easy
- Effective programs https://www.youtube.com/watch?v=2V1FtfBDsLU
- Are we there yet? (this one is more about OOP, but unless you're using something like haskell, idris etc its relevant for your type system of choice) https://www.infoq.com/presentations/Are-We-There-Yet-Rich-Hi...
What about this can't be done with types? Simple parametric-polymorphism gets you pretty far. Row types allow you to handle "maps as records" in a type-safe way. The rest is just having support for some kind of ad-hoc polymorphism so that you can re-use your functions on that small set of types (type classes, ML-style functors, interfaces, protocols, etc.).
I'm familiar with the advantages of type systems (my progression was Java -> Haskell -> Idris) but I found my personal productivity (even in larger systems built in a team) was best in clojure. I didn't feel that the guarantees given to me by the type system were worth the mental overhead, a lot of people feel differently (you amongst them I'm guessing :p)
As a closing point, if I were to ever build something that truly had to be Robust in a "someone will die if this goes even slightly wrong" way, I would reach straight for Idris and probably something like TLA+. However most of my development revolves around larger distributed systems communicating over wires, still resilient but in a different way. Mainly I use clojure.spec in core business logic and at the edges of my programs, for generative testing and ensuring that the data flowing through the system is sensible.
Also I personally find that to be too much overhead and ceremony in return for some type checking at compile type, as opposed to spec checking at runtime.
What do you mean by "data-oriented language"?
In the same way you can do immutable and functional stuff in java, it's not going to mesh with the rest of the ecosystem or language around you.
https://news.ycombinator.com/item?id=16414942
This is all application specific, but for the types of apps I've worked on (large enterprisey OO apps) you often need various bits and pieces of domain data across different methods. So given some function, you either pass in DomainClass1, DomainClass2, DomainClass 3 (using a couple of properties of each) or you define a new class SomeSubsetOfPropertiesClass solely to call that single method. In the former case, the types do not serve as documentation for the reader as it's not clear what shape of the data is required for the function. In the latter case you're duplicating code (the properties and their types) and the class really has no meaning except as a struct to call that method.
Now that I've been working with Clojure for a little bit I find I'm able to write much more concise, testable functions and calling them is dead simple since I can work with the raw data, transforming it into the shape I need.
An example in TypeScript:
interface Named {
name: string
}
class Person {
name: string
age: number
// constructor here
}
function f(obj: Named) {
// do something with obj.name
}
const joe = new Person('Joe', 25)
// Compiles, even though Person has an extra `age` field
// Person is structurally compatible with Named
f(joe)
If I change the type of "Named" to have the fields `firstName` and `lastName` of type string, accessing any other property inside `f` (like `obj.nonExisting`) or passing objects that don't have those fields.
Even better than that, you don't need to use classes, you can use "normal" JS data structures. Extending the last example:
const john = {
name: 'John',
age: 25
} // No class involved
f(john) // compiles
const alice = {
age: 25
firstName: 'Alice',
lastName: 'Jones'
}
f(alice) // compile-time error
EDIT: > Also, Clojure.spec allows you to be much more precise about properties. For example, it must be [...] non-nil [...]
TypeScript also handles nulls in the type system:
function f(x: string | null) {
if (x != null) {
// tsc knows that inside this if, x can't be null
return x.length
} else {
console.log(x.length) // this doesn't compile, x is of type null here
}
} (def email-regex #"^[a-zA-Z0-9._%+-]+@[a-zA-Z0-9.-]+\.[a-zA-Z]{2,63}$")
(s/def ::email-type (s/and string? #(re-matches email-regex %)))
(s/def ::acctid int?)
(s/def ::first-name string?)
(s/def ::last-name string?)
(s/def ::email ::email-type)
(s/def ::person (s/keys :req [::first-name ::last-name ::email]
:opt [::phone]))
(s/fdef add-to-account
:args (s/cat :person ::person :acctid ::acctid)
(add-to-account {::first-name "John" ::last-name "Smith" ::email "john@smith.com"} 12345)
(add-to-account {::first-name "John" ::last-name "Smith" ::email "abc123"} 12345)
ExceptionInfo Call to #'scratch.core/add-to-account did not conform to spec:
In: [0 :scratch.core/email] val: "abc123" fails spec: :scratch.core/email-type at:
[:args :person :scratch.core/email] predicate: (re-matches email-regex %)
(s/fdef lookup-user
:args (s/cat :email ::email)
(s/fdef lookup-user-by-name
:args (s/cat :last-name ::last-name)
Clojure has classes and types. How can it be untyped?
Machine language is untyped.
Well, that's a matter of opinion, even by long-term Clojure veterans. There is a reason Core.Typed was developed, though it hasn't been maintained recently. The fact that Rich felt the need to give the keynote at the last Clojure conference about the dynamic vs static issue shows that it is still a highly debated topic within the Clojure world.
- The aforementioned keynote highlighting the various reasons Rich chose to make it dynamic.
- CircleCI (one of the major users and propronents of core.typed) dropping it.
- The introduction of spec as an alternative for some of the reasons people use type systems (its certainly not a drop in replacement and doesn't intend to be).
- Spec allowing different kinds of verification not possible with a type system on its own.
Many of the comments on this page show why Rich gave the keynote. Because the same advantages of type checking are put forward as a reason to not use clojure over and over. They're not wrong, static typing has advantages, but I see little acceptance of any tradeoffs (or even acceptance that such tradeoffs exist: concretion of information, coupling of distant components by shared types etc etc etc I'm just paraphrasing the keynote).
He was highlighting the value proposition and tradeoffs of: being data-oriented, being dynamic and clojure.spec niceness. He felt the need to do this because he clearly felt that some people who were wavering about clojure were unsure why it was dynamic: "can't we have all this great stuff AND static types". He wanted to say "yes quite possibly you could, BUT here's the reasons why I didn't add types".
There are plenty of functional programming languages that believe static typing is a significant added value even under these conditions.
My main point was that dynamic typing should be judged by it's best implementations, not by JavaScript. For example, I would not judge static typing by Java or C++.
JS in particular is a very bad example of a dynamic language, the other "very bad" example being classic PHP.
This, mostly, because of weak typing.
Many of the problems attributed to C, a statically-typed language, are also due to weak typing.