HN Theater @HNTheaterMonth

I suggest a combination of theory (videos/books/papers) and practice.

For practice; I highly recommend learning Haskell. If you are new to functional programming then learning Haskell is challenging and frustrating but as with any new topic the key is to not give up but keep probing. A good recent development is lot of mainstream languages are beginning to include functional paradigms such as lambda, closures etc., For example Java introduced lambda expressions, Javascript has had them for a while now. But from a first-principles stand point Haskell is as good as it gets so please do learn and code in Haskell if not at work then at least side projects.

For theory I've found following material super useful.

0. This[0] is an incredibly awesome lecture where Phil Wadler takes us on a whirlwind tour of computer science. He talks us through different foundational structures on which almost everything (hardware and software) about computer science is built. I watch this lecture once every few months :-). It helps you build up context and ground various topics.

1. The one and only SICP. Book[1] and lectures[2].

2. Automata theory[3]. This isn't an easy course but gets to the heart of the matter i.e., the meaning of "function" and what how can it be mechanically "computed".

3. Category Theory is where lot of active research is happening in CS theory. This is a very good lecture series[4]. The pace may seem a bit meandering but don't be put off. Bartosz is a gifted teacher and works incredibly hard to disseminate knowledge. For evidence just look at a recent post on HN[5] about an article he published.

[0] https://www.youtube.com/watch?v=aeRVdYN6fE8

[1] https://mitpress.mit.edu/sites/default/files/sicp/full-text/...

[2] https://www.youtube.com/watch?v=-J_xL4IGhJA&list=PLE18841CAB...

[3] http://ce.sharif.edu/courses/94-95/1/ce414-2/resources/root/...

[4] https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbm...

[5] https://news.ycombinator.com/item?id=26991300

⬐ bidirectional

That post is by a completely different Bartosz.

⬐ vishnugupta

Darn! All these days I thought they were the same! Thanks for correcting me!

⬐ vishnugupta

> For evidence just look at a recent post on HN[5] about an article he published. > [5] https://news.ycombinator.com/item?id=26991300

Ignore this part because the one I referred to is a different person! Though they are both terrific :-)

just to note this talk briefly alludes to another subject, the Curry–Howard isomorphism, something Philip Wadler had similarly given a talk about at Lambda Days (2016) titled 'Propositions as Types'[1] (slides [2] and the video recording[3]).

[1]: http://www.lambdadays.org/lambdadays2016/philip-wadler

[2]: http://www.lambdadays.org/static/upload/media/14562260715188...

[3]: https://youtu.be/aeRVdYN6fE8

⬐ rocqua

That youtube lecture was really interesting.

The very ending was awesome as well!

> Neither is static typing. It's a layer of protection, much like tests.

Not true. The curry-howard correspondence shows the relationship between typed programs and proofs. I recommend you watch a Phillip Wadler talk about this: https://www.youtube.com/watch?v=aeRVdYN6fE8

Note: This doesn't mean that type systems can prove _all assertions_ about a program, but type systems do indeed work as provers.

> I don't think that's necessarily true. You still need to write tests with or without static typing. Those tests you need to write anyway will catch type errors in a dynamically typed language that a statically typed language picked up at compile time..

This isn't necessarily true unless you test for all inputs (which tends to be infeasible in most cases). A type system can reject inputs by virtue of their lack of conformance to a type, which eliminates the need to test them.

> The question is whether you need to write more tests and whether the greater number of tests offsets the greater amount of code you need to write to statically type your code.

I don't have any evidence to support this (if someone does or has proof to the contrary, I'd love to see it referenced here), but I believe there is almost no overhead imposed by a static type system with type inference.

> Ditto for types.

I acknowledged this above, you just removed that part from the quote. In practice I've never had a bug with the type system (that I'm aware of), while I've seen hundreds of bugs from incorrect test assertions.

⬐ crdoconnor

>Note: This doesn't mean that type systems can prove _all assertions_ about a program, but type systems do indeed work as provers.

Type systems can verify certain properties about code much like a test does, but that's far from being a mathematical proof of program correctness (especially since compilers have, you know, bugs).

>This isn't necessarily true unless you test for all inputs (which tends to be infeasible in most cases).

No, it's necessarily true. The vast majority of type errors I experience get picked up during TDD. A small minority reach production.

It's very easy these days to write tests that cover an enormous range of inputs and outputs (e.g. see quickcheck).

I'd estimate that maybe 5% of errors I experience in production are type related (in a dynamically typed language). That's offset against quicker development time (which also eans ease of fixing the other 95%).

>I believe there is almost no overhead imposed by a static type system

I think that's wishful thinking.

>In practice I've never had a bug with the type system (that I'm aware of)

Which type system have you never had a bug with? I've dealt with several buggy, crappy type systems?

>In practice I've never had a bug with the type system

I've seen plenty of bugs caused by picking the wrong type.

>I've seen hundreds of bugs from incorrect test assertions.

So have I. Different types of bugs though. The kind which static typing doesn't help eliminate.

⬐ knucklesandwich

> No, it's necessarily true. The vast majority of type errors I experience get picked up during TDD. A small minority reach production.

I'm not trying to argue against your experience (or persuade you against it, for that matter). Only making a point that it is possible for you to have type errors that go uncaught by unit tests unless (unless you run those tests against all values).

> It's very easy these days to write tests that cover an enormous range of inputs and outputs (e.g. see quickcheck).

Quickcheck takes advantage of types to narrow the inputs for generative tests, whereas dynamic languages have to content with any possible input.

>> I believe there is almost no overhead imposed by a static type system > I think that's wishful thinking.

Here's a couple ways I think you actually waste more time in dynamic languages:

1. Type checks. Sounds almost tautological, but it's true. Any time you see someone using the type() function in python, you're branching in code for something a compiler could take care of for you.

2. Redundant validation, specifically against a purely functional language that is statically typed. Since types encode facts about data and functions encode theorems, statically typed languages only require one test to verify the assumptions in a theorem. In other words, if there is one function creating values of type Foo with an integer attribute "foo" and it insures that "foo" is 0, I never need to check if foo is 0 anywhere in production code. I only need to check that in a single test of the constructor. In practice I find this means I need to write a lot less tests with a statically typed language, and generally a lot less branches in code.

3. Documentation comprehension. I can't count the number of times I've read a javascript library's documentation only to be thoroughly confused about what kinds of values can be passed to a function legally. Since the language provides no way to enforce this, it seems to encourage a culture of negligence about documenting what invariants of data are required to hold. Furthermore I rarely get a descriptive exception informing me what the issue is, rather I get a type error about a missing attribute or something.

4: Boilerplate code. Fixed data schemas mean you can generate efficiently executing code to perform tasks like serialization, client libraries, etc. Take a look at servant: https://haskell-servant.github.io/ Because haskell is statically typed, the type system makes it trivial to generate an HTTP server, a client, and a swagger API docs page all from a couple types. This can be done for certain things in dynamic languages, but since it requires introspection it will almost definitely be slower (and in some cases that may make it impractical to use).

5. Refactoring. Dynamic types are notoriously a pain for editors. Values can be changed ad hoc in ways that make it very difficult to change names without some smart regexes. Refactoring in statically typed languages is a breeze with a sufficiently smart editor/ide. Find and replace is generally two clicks away and is guaranteed to find all occurrences and replace them safely.

6. Condition checking. Pattern matching is not exclusive to statically typed languages, but it is much more common in them. Static type systems also allow for exhaustivity checks that a dynamically typed language cannot perform.

In general I think the things people claim are time consuming about statically typed languages are based on older languages that are lacking richer type system features. Things like:

1. Omnipresent type annotations. In haskell you almost never have to specify one of these (in fact you can get near 0% of these if you turn off the monomorphism restriction). The most common use of type annotations in for function signatures, which I find are nice to have for documentation purposes anyways.

2. Inability to perform generalizable code. A lot of people base this on experience with languages like Java, which is unfortunate because the state of the art is much farther ahead. There are many "dynamic feeling" generalizations you can get out of newer statically typed languages. For instance, you can easily generate a "falesy" abstraction similar to python or javascript through haskell typeclasses. Typeclasses, functors, etc. are all examples of statically typed features that allow you to write abstract code over disparate sets of types.