Skip to content

Instantly share code, notes, and snippets.

What would you like to do?

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.

Copy link

anka-213 commented Aug 26, 2016

@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.

Copy link

V1rtuousCycle commented Aug 26, 2016

Thanks. Good clean article.

Copy link

Profpatsch commented Aug 30, 2016

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”.

Copy link

garybernhardt commented Aug 30, 2016

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

Copy link

eduardoleon commented Aug 31, 2016

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

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

Copy link

garybernhardt commented Aug 31, 2016

@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.

Copy link

EvgenyOrekhov commented Sep 7, 2016

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

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

Copy link

garybernhardt commented Sep 10, 2016

@EvgenyOrekhov Nice catch, thanks!

Copy link

stereobooster commented Sep 11, 2016

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

Copy link

JeroenDeDauw commented Jan 9, 2017

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment