Types, and Why You Should Care [video]
youtube.com
youtube.com
"The Problems of Programming"
Domain Complexity
Misconception
10x
Place Oriented Programming
Weak support for information
Brittleness/Coupling
Language model complexity
Parochialism/context
weak support for Names
Distribution
Resource utilization
Runtime intangibility
Libraries
Concurrency
10x
Inconsistency
Typos
There are some type systems, for example Rust's, which integrate RAII into the language as a first class concept and are able to address some of the upper level concerns like concurrency and place oriented programming. In general, however, there are many problems on this list where more complex type systems doesn't help, or even makes it worse.[0] https://twitter.com/stuarthalloway/status/926065084652228609 [1] https://www.youtube.com/watch?v=2V1FtfBDsLU
This slide is not a comment on the frequency of these problems, because typos are definitely one of most if not the most frequently occurring issue in the day-to-day work of most developers, and I'm sure Rich Hickey realizes that.
Rather, this slide is a comment on what he defines as the "severity" of these problems, and one of the important manifestations of severity is the cost of getting these wrong.
With the exception of certain business domains where getting things perfectly right the first time is paramount, such as financial transactions and safety/security-critical programs, the cost of typos and inconsistencies is generally minuscule because they're practically costless to debug and fix. In fact, they often cost so little that we end up instinctively fixing typos and inconsistencies countless times throughout our day to day development processes, often without ever even making a conscious effort to identify and fix them. Even if the occasional typo makes it past our tests and into production, these issues are almost always trivial to debug and fix (and if they're not, and you don't happen to be in of these domains where getting things right the very first time is paramount, then oftentimes that can be the smell of some deficiency in your deployment/monitoring setup, or a manifestation of some other more subtle, but more severe problems listed on the slide, such as brittleness/coupling, place oriented programming, weak support for concurrency/names, etc).
Of course, being able to outright eliminate these entire classes of errors is a legitimate benefit of a static type system, and Rich Hickey acknowledges this benefit later in the talk. If you're in one of those business domains where you absolutely cannot afford to let typos and inconsistencies sneak their way into your production systems because the they'd be disproportionately costly to fix, or result in consequences that you're not willing to accept, then static typing can be very useful for providing those safeguards.
However, I think he also brings up an important point that static type systems and the act of flowing types around in your system is often a significant source of coupling, and that coupling is a much more severe problem when it comes to maintaining a piece of software over the long term. So it's important for each team to assess that tradeoff carefully in order to gauge if they're willing to take on that additional level of coupling in exchange for eliminating the possibility of typos and inconsistencies from reaching production.
This way you do not use concrete types in the construction, you link things with requirements on/between the parameters.
Please take a look at the Expression Problem: https://en.wikipedia.org/wiki/Expression_problem
This thing is an essence of question how to design low coupled system when initially high coupling is expected. There are solutions for most languages and, probably, for your statically typed language of choice (from statically typed languages).
Needless to say I really don't agree with that list, as history shows the inconsistency, typos, lack basic units and the ability to express them in a computation etc., have been more catastrophic than he believes them to be. And these issues cannot really be fixed without a proper type system, that will not allow stuff like that to get into production.
And a good type system cannot be optional, e.g. clojure's spec, There are number of studies that show that will power, is not enough, there needs to be and environment - a type system - that helps to avoid and catch mistakes.
I also question the value of taking too much stock in outliers. How many of us will be working on the next Mars orbiter?
From the list you cite, only three of 10 errors are caused by "typos", "lack of basic units" and type errors.
And this is just a particular list.
Recalling Rich Hickey list, the things that cause more problem in code, from worst to less damaging:
Domain Complexity
Misconception
10x
Place Oriented Programming
Weak support for information
Brittleness/Coupling
Language model complexity
Parochialism/context
weak support for Names
Distribution
Resource utilization
Runtime intangibility
Libraries
Concurrency
10x
Inconsistency
Typos
I'm pretty sure that if we compile a list of real-life cases where the major reasons of failure according to Rich Hickey have caused trouble, the list of examples would be immense, compared to "typos".https://docs.julialang.org/en/stable/manual/types/
Although it's "untyped" (in the sense of the video), because it's strongly typed, there are plenty of nonbrittle optimizations that are performed by the compiler on account of the type system, and the result is something that's often within 1~1.5x speed of C.
At the same time, I had to write my own numerical system and because of Julia's type system i could immediately plug it into the standard library's matrix algebra and fast fourier transform algorithms and do comparative analyses out of the box. You can even do exotic things -- I was testing some reed-solomon encoding and created a galois field type, and the standard library matrix solve algorithm worked out of the box on my custom type.
Has good lessons for python, R, and Matlab. Seriously anyone who does anything with vectors should watch this.
Moving to a different environment where those techniques are no longer as effective will result in lower productivity for a while. Moving to an environment where those techniques can no longer be used (no type-checking, no ability to unit test) results in frustration, bargaining and hopefully acceptance, but the end result is that everyone stays on their side of the fence depending on whether they identify as "relies on type-checking to ensure correctness".
By the way, funny how sometimes, we get something out of bargaining (TypeScript because there is no type-checking in JavaScript, Selenium because there is no unit-testing in graphical user interfaces).
Just a basic example of two dynamic languages: In Python I can get a lot done and really don't miss types at all. In JS otoh, I feel lost until I pull in TypeScript to tame it, the language makes it even hard to think clearly without types, like, "is that an object or a dict" or "is it a map? from what to what?" etc. For most usual programmer mistakes that would be type errors in typed language, Python still throws a meaningful and debuggable runtime error, whereas JS carries on an breaks much further from the cause of the problems, leaving you to debug WTF after WTF...
And static typing is great, as long as it doesn't require you to type variables and anonymous or small utility functions/methods... eg. it sucks without inference!
Some languages work better with types, some don't gain much from them...
No wonder, because Python has types (well … most everything does; but Python isn’t unityped [1]). It’s even relatively strongly typed. It’s just not statically typed (what the video calls “typed”).
That said, I do miss static type checking in Python, and a lot of the tooling and methodology around Python (pylint, TDD…) are a direct consequence of that lack of static checking.
— You seem to be aware of this but the distinction between “has types” and “has static typing” is actually fairly important. APIs in general often take advantage of Python’s extensible type system.
[1] See e.g. https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...
E.g. a tag might tell us that some object is a function. But to know how many arguments it has, whether some are optional, and so on, we have to inspect fields beyond the tag.
"And this is precisely what is wrong with dynamically typed languages: rather than affording the freedom to ignore types, they instead impose the bondage of restricting attention to a single type! Every single value has to be a value of that type, you have no choice! Even if in a particular situation we are absolutely certain that a particular value is, say, an integer, we have no choice but to regard it as a value of the “one true type” that is classified, not typed, as an integer."
[1] https://docs.python.org/3/whatsnew/3.6.html#pep-526-syntax-f...
Static checking gives you basic unit testing. TDD is far more expansive than unit testing. Static checking is not going to integration test your app for you.
Well-typed programs should not go wrong. Python programs can crash at runtime due to simple type errors (expected integer but got a string). A crash is a crash, from a theoretical point of view it matters not that the error is prettier than a segmentation fault. Python is not strongly typed, it just has good error messages.
> Some languages work better with types, some don't gain much from them...
When you have proper type inference (which has been around for literally decades), what advantages do dynamic languages really have? I don't see any significant benefits personally. If you you're having trouble justifying at compile type a property holds, more than likely you've got a bug that's going to bite you later.
The advantage of dynamically typed languages is that you are not glued to one specific proof language and don't have to provide proofs for trivial properties, or one-off programs you only need to run once. There are some type systems that attempt to provide similar benefits, e.g. success typing puts the burden of proof on the compiler which will only reject a program if it can prove that the program is incorrect [1]. But as far as I know, that approach has not been included in any mainstream programming languages.
That describes any dynamic language that does type inference. Type is taken into account for diagnosis and better code, but not as an excuse for rejecting the program just because it isn't fully analyzed.
Do you have any realistic concrete examples of this? I find this happens very rarely myself (maybe once every few thousand lines of code) and just involves adding a small amount of code along the lines of "throw 'Unexpected error' // this should never happen because ...".
> The advantage of dynamically typed languages is that you are not glued to one specific proof language and don't have to provide proofs for trivial properties, or one-off programs you only need to run once.
For me, type errors for where you've mixed up e.g. string, number or object variables or where you've forgotten to check if a variable is null/undefined before you use it are incredibly common compared to the rare times the type system gets in your way. You would have to (and most wouldn't) write many automated tests to catch all those potential errors if you weren't using a type system for similar robustness. Throwing all that away because of the rare case the type system obstructs you doesn't make any sense to me.
I still think if you're regularly writing code that is hard to justify to a mainstream type checker you're more than likely doing something very wrong and writing code that is hard for others to understand. I'd love to see a realistic counterexample.
However, I like to use Python for small single-purpose utilities, and in those cases I don't even bother with the optional type annotations, let alone checking them with mypy. Since those programs are so simple that a handful of test cases is enough for 100% path coverage, if the program runs correctly on one case, it's almost guaranteed to run correctly for all others. (Similar to Haskell's "if it compiles, it runs".) Statically checking for type correctness would be pointless, because you can just run the program to find out. It then becomes quite natural to e.g. apply type-modifying transformations in-place, which most type checkers wouldn't allow, since they assume a single fixed type rather than a progression of different types during different stages. (You can get around that, of course, but it requires constantly recreating essentially identical objects to give them a new type.)
For an example of a project (not written by me) where the type checker's rejection of a correctly working program precluded the use of a type checker, see http://www.oilshell.org/blog/2016/11/30.html
I agree for small utilities and code that's acting as glue between layers that it's convenient to have languages that are loose with what they accept because you can usually manually and exhaustively QA them and because you have no other choice when connecting languages without static type systems. Once you have a large and complex app though, strong typing makes you so much more productive that I honestly can't understand how anyone could argue against strong types.
Dialyzer, the optional static typing system that is of part of the Erlang distribution, is based on success typing. Here is an accessible introduction:
Type inference is compatible with dynamism.
Infer all you want. Optimize and diagnose, just don't strip type from my objects, please, and don't say I can't try running something because it wasn't completely checked.
You can quickly prototype by repl-ing around half-working pieces of code until you get to something that you can conceptualize. Sometimes you start from "how to" knowledge, but you don't really have the "what is" knowledge. You "know how to make it work" but you don't yet have any idea of "what it actually does". You'll get to that stage, but you need a prototype you can play with in the meantime.
Mathematicians have the hardest time groking this, so I give them the example of drawing an ellipse: let's say you start with a "working definition" of "an ellipse is that ovalishy thinggy that I get by dragging a pencil on a loop of string tied to two nails set at some distance". You know how to produce it, you want to play with it, but have no idea how to define it yet.
A dynamic language gives you the higher level equivalent of being able to "draw the damn ellipse even if you have no idea what it is"... later you can look at the code for drawing the ellipse and extract from it that "aha, it is what you get by constraining the sum of distances from 2 points to be constant!".
But some people (like me), are not very good at abstract thinking, so we need to play with half-formed stuff on screen, like "let's do this api call" and "do that and that to the returned data" and "pass it to the other thing" that "maybe someone forgot to document" and "see what it does"... and reverse engineer the abstractions from working code and maybe later properly generalize them.
I've never seen a static language with a good interactive prototyping experience so far. Though I'm playing with OCaml/Reason now, and its REPL seems quite powerful, though the language is more verbose/pedantic than I'd like it...
Which is a great thing.
It could be solved by having a `string.get_iterator()` method (or `string.iterator` `@property`) for when you want to iterate over chars of a string to make it obvious (in the usual pythonic style). But probably this would break too much backward compatibility and only catch a few very easy to track bugs anyway.
Ironically, Javascript almost got this right with `string.charAt()`, but then it shoot itself in the foot by also adding `[]` operator access in its typical "let's add more ways to do it to be sure at least one of them is bound to be wrong in some context" style...
String iteration yielding individual characters as strings is debatable.
A function or method having no way to specify that a parameter must be a list of string, then acting strangely when passed a single string is a problem that types can help with.
F# does this amazingly well. Rust and Scala to a certain degree.
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;
}
Is there a bug here? Well, that depends on the intent. Did we really intend to add an int to an int*?Even Haskell's type system can't tell what you intend:
increment i = i + 11;
Did we really intend to add 11 rather than 1, or is that a typo?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;
}
I think your example is flawed. The real problem here is that you're allowed to add an int to an int* with +. int* is not be of type int, and should therefore require some sort of cast to make it possible to add an int to it. Either that, or require a different operator/function to add to a pointer, e.g.: int* increment(int* i, int step)
{
return prt_add(i, step);
}
Not all type systems are equal, and how the type system interacts with the language is important.To be clear, my question is, how would you reasonably catch the typo with types in the following Haskell function?
increment x = x + 11;
...noting that this typo is reliably caught by a unit test. def test_increment(x):
assertEqual(increment(x), x - 1)
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. def test_increment(x):
assertEqual(increment(x), x - 1)
This isn't a trick question. You run the test, and see that it fails.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
This is admittedly overkill, but the point is you really should only be testing inputs and outputs in a test, not doing calculations.> 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)
I won't paste the full test here because this is part of a larger function, but rest assured I'm not duplicating the definition of the function in the test.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;
How would you catch this bug via a reasonable usage of the type system? Noting that a unit test catches this bug trivially.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)
Note that the only explicit type in the entire program is the `:: Integer` annotation on the upper bound for randomRIO. Without that annotation the program would be underconstrained, since the input to `volume` can a list of any type with Ord and Num instances.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 you pass f() a class/object that doesn't have a `name` property of type string, the compiler would catch your error.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
Clojure.spec is cool, but I don't see how that is incompatible with static typing. You can still have libraries that check more complex properties at runtime.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)
Using those keywords you can define maps which specify shapes of data: (s/def ::person (s/keys :req [::first-name ::last-name ::email]
:opt [::phone]))
Functions have their own separate specifications. Here's one that accepts a person and an acctid: (s/fdef add-to-account
:args (s/cat :person ::person :acctid ::acctid)
And must be called like this: (add-to-account {::first-name "John" ::last-name "Smith" ::email "john@smith.com"} 12345)
If you tried calling it with an illegal argument and it's instrumented you will see an error: (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 %)
Here's the difference. What if I have another function that just accepts an email: (s/fdef lookup-user
:args (s/cat :email ::email)
And another which looks up by last name: (s/fdef lookup-user-by-name
:args (s/cat :last-name ::last-name)
And now imagine if you wanted to accept either an email or last-name (notice it does not match our person spec). Attempting to use interfaces would quickly get out of control. You'd have to create an interface for every single property and extend interfaces to form arbitrary groups of properties.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.
Maybe there'll be a "safe" subset of the pip/npm registry that will only let typed APIs in, to promote the concept.
As a side-note: is there data on how many dependencies there are of framework on npm, on average? If it's anywhere past two, I'd say that the extra time spent typing is more than compensated by the time saved by the user of the API.
This video will blow your fking eardrums out because at the 4:37 minute mark, the presenter switches on his microphone system and the input source of the video changes to be about 400% what it was previously.
The fact that nobody has mentioned this is a pretty strong indication that none of these people have actually watched this video.