types.markdown

This document has moved!

It's now here, in The Programmer's Compendium. The content is the same as before, but being part of the compendium means that it's actively maintained.

no popular type system can actually express our HighFive type above

In case anybody is interested, you can express this in Flow.

@yogthos “Baking a proof into the solution leads to incidental complexity.”

The programmer has a responsibility to produce the proof, whether it's baked in the code or written on a separate piece of paper. I know which is easier to keep in sync, manage using version control, etc.

That being said, the usability of dependent types still leaves a lot to be desired.

@eduardoleon

You only have to prove that your code runs for the cases that actually exist in the application. Static typing requires you to provide a proof for all cases, including those that are unreachable.

In case anybody is interested, you can express this in Flow.

I was surprised to find this wasn't the case in TS. Had always thought it was since it does support string literal unions, just not more mixed unions of literals.

Flow has some nice features and is improving rapidly. It makes for a very interesting study of what is possible when typing a highly dynamic language long after its creation. I've been pleasantly surprised at the very complex types we can express.

Another point, which I haven't thought about before: objects in most OOP languages are "dynamically" typed i.e. they carry type definition at runtime to be able to do method calls on them. Unless you thought that something like Rust can be treated as OOP. It depends on how you define OOP.

@garybernhardt the most good about this article is the fact that it doesn't try to go too strict with some definitions, so it doesn't mislead and generally tends to be true at big scale. Like your writing style. Thanks

@yogthos No idea how other people use static typing, but at least the way I use it, one of the main points is not to have unreachable cases in the first place. If I have unreachable control flow paths, it means that I have to refactor my code. Designing your program so that it expresses exactly what you mean and nothing else is very good mental exercise and discipline.

@yogthos (cc @eduardoleon)

I would take issue with that in the sense that "cases that actually exist in the application" is an assertion, which doesn't have a grounding in proof. You may write test cases to show that a finite number of things cannot happen, but you are not giving a general solution, only a specific one. At some point, your safety will rest on a human assertion "this cannot/will not happen". Humans have proven to be quite unreliable at that without tools - proofs being a very useful one.

@kolektiv Agreed. That being said, I find it ugly to have to prove that certain paths are unreachable. If you're doing things right, unreachable paths simply don't exist in your code.

Another way to put it is that I like my programs to be proofs in minimal logic, not because I don't believe in the validity of the principle of explosion (of course I do!), but rather because I find it beautiful to prove things without relying on mathematical sledgehammers.

@hugows

• So someone else here mentioned pandoc as one piece of software that's out there.
• Facebook use Haskell and have posted publicly about their use of it.
• A bunch of banks and financial institutions use it.
• git-annex is written in Haskell.

One thing that works somewhat against it when it comes to visibility is that my my estimation a fair chunk of those using it professionally are building service backends and websites, which aren't particularly great for publicity. As opposed to say something like Docker where the publicity for Go is really public and loud.

@eduardoleon - very much agree with you. One of the goals for me in a type system is to make undesirable or invalid states unrepresentable. The smallest algebra I can implicitly define which represents my desired program and nothing else is the right thing. Thanks for the mention of minimal logic, not something I've looked at in depth before. One for my reading list.

@stereobooster: You can write OO without runtime tagging, but you lose reflection. Haskell also has runtime tagging: that's essentially what that Typeable snippet above is doing.

While program expressions are best typed at their most general, at runtime values can be tagged with their most specific types. It's possible (but not obvious or easy) to have the runtime types be similar or even a subset of the compile time types which creates a strong linkage.

@tiborsaas None of those arguments are really about static vs dynamic types.

1. [Short code] I have found no evidence that static types necessarily causes more code, especially when you have automatic type inference, so you don't actually have to write any type signatures yourself. In some cases you actually need less code since the types carry some of the information needed.
   For example: QuickCheck (an automatic property tester) is a pain to use in Erlang, but it's fully automatic in Haskell, since it can figure out what kind of input to use automatically from the types.
   Furthermore, you'll usually need more unit tests to compensate for the lack of types, which is usually a lot less compact than the corresponding type annotations.
2. [Javascript example] You can just as easily have automatic coercion (aka. "Weak types") in a statically typed language as in a dynamic one. That is a completely different question.

See also, the blog post about common fallacies in the dynamic vs static types debate, that was quoted in the article: https://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wrote/

@yogthos No one is forcing you to prove anything just because you are using a static language. If anything, the compiler relieves you of the burden of proof, by doing the heavy lifting for you.

If you want to, you can encode many complex properties in the types and have the compiler verify them for you. This is obviously more difficult the more complex properties you try to enforce.

If you don't want to do that, just write code similar/identical to what you would have written in a dynamically typed language and get some simple proofs (compatible types, no missing methods, etc.) for free.

Thanks. Good clean article.

no popular type system can actually express our HighFive type above

data HighFive = Hi | Five

I call bullshit. Unless you have a very interesting definition of “popular” or “types”.

@Profpatsch The constructor Five is not the integer 5. Likewise, the constructor Hi is not the string "hi".

@Profpatsch I would've just given him the type Bool.

@garybernhardt Any singleton is as good as any other. They're isomorphic.

@eduardoleon Integers are a set of values containing 5 and others. Strings are a set of values containing "hi" and others. HighFive is the set of values {5, "hi"}, and each of those values also exists within one of the Integer and String sets. A value taken from HighFive is exactly equal to the same value taken from Integer or String, can be compared against it, etc.

This is not an idea that's directly expressible in Haskell; or, as far as I know, in any actual type system. People have told me that it's expressible in TypeScript, but I'm skeptical.

This example is clearly confusing. But, interestingly, the only people who have objected to it have shown that they know an ML-descended language. I suspect that people with no formalities to fall back on pass right over it without a problem. There are sets of values. Some sets intersect with other sets. It's not a big deal.

Of course, all of this is arguing the color that we should paint a yak at the bottom of a rabbit hole. This is the introductory paragraph of a 3,500-word article; a paragraph that contains no details about any formal mathematical system or software system.

@garybernhardt It should be add instead of f in this Haskell example:

f :: Num a => a -> a -> a
add x y = x + y

@EvgenyOrekhov Nice catch, thanks!

There is Complexity Zoo. Does anybody aware of similar resource for type systems?

Is there a list of languages by type system power like the one at the end of this gist, but then with more languages? There is the Comparison of programming languages by type system on Wikipedia, though this does not have the categorization used in the gist and cannot really be sorted.