Where Do Type Systems Come From? | Hacker News Reader

Where Do Type Systems Come From?

blog.felipe.rs

285 pointsphilix001164 comments

Watch Oregon Programming Language School lectures "Basic Proof Theory" by Frank Pfenning.

https://www.cs.uoregon.edu/research/summerschool/summer15/cu...

Very clean and easy to follow video lectures on the relation between, types, programs, and logical proofs. One does not need functors and monoids to appreciate the beauty of functional type systems. (And to see why such type systems are indeed discovered rather than invented.)

I second this. Frank's material is always thorough and approachable. He's designed and taught many courses at CMU, and his lecture notes for them are never less than impeccable.

It's a common misconception that Russell/Whitehead "invented" type theory. In fact, Frege had already made the very insightful distinction between functional and non-functional types in the 1890s -- this was the key development that Russell based his hierarchy of types on. See "Function and Concept" (1891)[1]. It was a growing and communal sentiment that a (meta-)theory of types would make certain mathematical concepts more palatable.

If anything, I think the conceptual father of type theory is Gottlob Frege, and Alonzo Church was the first to apply it concretely.

[1] http://fitelson.org/proseminar/frege_fac.pdf

It seems to me Frege understood the need in mathematics to talk about many different kinds of thing - numbers, truth-values, functions, and so forth - and to distinguish which kind of thing you are talking about; but not the necessity to use types (or other methods) to avoid circularity. Indeed, it is precisely the mistake Frege made in his attempt to axiomatise logic and mathematics and which led to Russell's paradox, that motivated Russell (and Whitehead)'s theories of types.

Frege certainly articulated a clear notion of what a function is, which is significant.

If you haven't thought much about type systems but want to understand what the big deal is, I wrote a post specifically for you [1]. It draws motivation for wanting a good static type system from first principles.

[1] https://gilbert.ghost.io/type-systems-for-beginners-an-intro...

Nice article. I especially liked:

> program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter.

Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool.

Also, I never thought of "higher-order functions" as breaking into a countable hierarchy of nth-order functions, which is an interesting thought. In Haskell the hierarchy would start off as

    zerothOrderFunction :: a
    firstOrderFunction :: a -> b
    SecondOrderFunction :: a -> (b -> c)
    SecondOrderFunction' :: (a -> b) -> c

In general, an nth-order function is a function which either

1. Takes an (n-1)th order function as an input and returns a simple type.

2. Takes a simple type as an input and returns an (n-1)th order function as an output.

The upshot is that typed programming languages not only catch bugs, but prevent you from legally expressing many non-sensical expressions (analogous to the set theory paradoxes). For example, consider the expression

    (\x -> x x) (\x -> x x)

If you expand this expression, it reduces to itself:

    (\x -> x x) (\x -> x x) == (\x -> x x) (\x -> x x)

In a purely untyped language, this expression would be legal. But what would be its meaning? Arguably, it is non-sense, and should be excluded from the set of legally expressible expressions. The way to do this is through a type system. And indeed, if you typed this statement into a Haskell REPL you would get a type error; this statement can actually be proven to be untypable (IIRC).

On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. It would therefore be interesting if somebody found an expression which was both (i) meaningful and (ii) only expressible in an untyped language. You would then have an argument for untyped languages :-)

> > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter. > Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool.

In case it's not clear, it's just that it eventually ends up with a run time error (the talk about runFunction being a second-order function is just an explanation for why you should expect it to end up with a run time error). The evaluation is

       program3()
    == runFunction(runFunction)
    == runFunction(1)
    == 1(1)
    == Error: func (with value 1) is not a function

Depending on your system, 1(1) is quite sensible, That is applying 1 to a list of parameters just returns the 1st parameter. This is a matter of the semantics that one uses when application is run against any value.

1(1) -> 1

Just because the common idea of application is that it only applies to functions does not mean that application applied to other types is nonsensical and should end up with a runtime error.

If your language allows application to be defined for different types, then the type system should be capable of determining the type that returns from application.

A practical example of a language in which application is valid for integers is Unicon/Icon. Both functions and integers have specific semantics with regards to application. And failure is an option.

I see. The error makes sense now.

    foo :: a -> (b -> c)

Not saying it's wrong, but "foo is a second-order function" is a distinctly minority opinion.

To a useful first approximation, Haskell works as a cartesian-closed category, which basically means we have tuples and that tuples harmonize with functions so that foo behaves just like

    uncurry foo :: (a,b) -> c

which is a first-order function.

So the majority opinion calls foo a first-order arity-2 function.

Here's a bar function that's truly second-order:

    bar :: (a -> b) -> c

In general, the order of a function is the count of parens nesting the leftmost innermost arrow. It is invariant to currying/uncurrying as well as permutation of arguments.

The same counting principle applies to other invariants such as ranks and kinds.

"How high can the order of a function go?" is the question explored in this blog post [0]. Note how the author's definition of order -- essentially the same given here -- got left and right mixed up.

[0] http://math.andrej.com/2006/03/21/interesting-higher-order-f...

I think it is not just a minority opinion, but just plain wrong.

> On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. It would therefore be interesting if somebody found an expression which was both (i) meaningful and (ii) only expressible in an untyped language. You would then have an argument for untyped languages :-)

Here's an example: The W combinator `\f x -> f x x` can be expressed in Haskell but it doesn't work everywhere it should, unlike in an untyped universe:

http://us5.campaign-archive1.com/?u=4937a9a2eb9eee0a26e1e0a2...

In other words, types can sometimes make you lose reuse.

That's amply compensated by types removing massive amounts of junk in the untyped world. If you don't believe me, try hacking in an untyped calculus sometime.

> Here's an example: The W combinator `\f x -> f x x` can be expressed in Haskell but it doesn't work everywhere it should, unlike an untyped universe:

That's an example in one type system, not a feature of all type systems. There's a good argument that typing is more expressive than dynamically typed languages: you can always add a dynamic type to your style system and recover all dynamically typed language features, but you can't go the other way around and recover all the features of a statically typed language. For instance, the performance benefits.

>On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. It would therefore be interesting if somebody found an expression which was both (i) meaningful and (ii) only expressible in an untyped language. You would then have an argument for untyped languages :-)

Any type system will reject some correct program. As a trivial example, consider:

    if( f() ):
        1 + "a"
    else
        1

This is a perfectly fine expression iff the result of f() is always false.

Interesting. It could still be argued this program isn't meaningful (or perhaps "not useful").

At this point, you start hitting a problem from fundamental computation. When are 2 programs equivalent? Is it when they behave equivalently in any implementation or is it when there is a chain of rewriting rules that change one to the other.

The issue with the first definition is 2-fold. What set of implementations are you qualifying over, and what to do with weird programs that crash occasionally. This is similar to what happens in the given example. The program is equivalent to 'return 1' when f is always false. Otherwise, it might crash.

In the second definition, 'return 1' and the given program are just different programs, until you actually substitute an f and continue reduction.

Well, it is a trivial example. In reality, such things would be hidden in the complexity of the code. One could argue that if the correctness of the code cannot be accepted by the type system then it would also be confusing for a human to look at, and should therefor be refactored; which is why (in practice) this is a non issue.

For a less trivial example, consider the expression "f(x) + g(x)" where both f and g can return either a number or a string. It is conceivable that for any given x, they would always return the same type, but a type system cannot detect every such case.

Or consider a program like:

    x = 1
    print_int(x)
    x="a"
    print_string(x)

I have seen code just like this in dynamically typed languages. You can also run into a simmilar situation that is not obviously correct if, for example, x is a global variable while the program is running a state machine. You can then view each state a transitioning the type of x. Determining if such a program is correct would involve knowing each state transition, what type of x is expected when control enters a state, and what type x is when control leaves a state (and a given state might have multiple output (or even input) types. I have seen one program that actually worked like this; and it was not fun to modify.

Of course, a type system is no guarentee that you do not have this sort of problem. For example, you could say, in the first example, that x is a union type of Int and String (and print_int and print_string are defined to operate on such a union). In this case, the program is well typed, but has partial functions, so the type system cannot guarantee that there will not be a runtime error when you call them (it won't, however, be a type error, since the type system missed it).

You could also have x be an untagged union. In this case, I don't see a way of doing any better than undefined behavior.

A completely different type of example, is C code such as:

    *0x01 = 0

which means "set the memory at address 1 to 0", but is poorly typed.

    "f(x) + g(x)"

This example is way too trivial to explain why type systems are generally undecidable. Let's imagine:

    def f/g(x):
      if isinstance(x, str):
       return 6
      elif isinstance(x, int):
       return 'a'

It is decidable for any type of x that is previously known. More importantly, type systems were essentially created to be able to prove whether a given expression is decidable or not.

    x = 1
    print_int(x)
    x="a"
    print_string(x)

This is solved by A-normal form (https://en.wikipedia.org/wiki/A-normal_form). Or by a more general concept that is available outside functional languages, SSA (https://en.wikipedia.org/wiki/Static_single_assignment_form).

You can make a point that this code is hard to modify in dynamic languages, but it is an issue with the code style rather than type systems. For example - IntelliJ IDEA would highlight such Pythonic code as incorrectly typed, since you have changed the type and therefore the variable itself.

I find the general argument against complexities in the type systems such as Haskell to be quite amusing, to be fair. Most of the time you are not dealing with code that is undecidable - and that's why type systems are interesting.

the real world is not strictly typed, i think types are for the compiler rather then humans. Im however a big fan of runtime bound checking so that the program always have a sane state.

> For a less trivial example, consider the expression "f(x) + g(x)" where both f and g can return either a number or a string. It is conceivable that for any given x, they would always return the same type, but a type system cannot detect every such case.

You can encode this quite easily in a language with a dependent types.

for the case of

    x = 1
    print_int(x)
    x="a"
    print_string(x)

the type system could simply instantiate a new variable, x: string, that shadowed the old x: int. this is perfectly valid ocaml, for instance:

    let x = 1 in
    Printf.printf "%d\n" (x + 1);
    let x = "hello" in
    print_endline (x ^ " world")

You could, but that seems like a transformation of the program itself, not a feature of the type system.

the point is that just because two variables have the same name doesn't mean they are the same variable; you need a (name, scope) pair to fully disambiguate them. some languages have the scope of a name be the enclosing function, so that all references to x within a function body are the same x, and the type therefore attaches to (x, function). however that is not the only way to do it; in ocaml the let statement rebinding x introduces a new scope, so that (x, line 1..) is a genuinely different variable from (x, line 3..), and has a new type. you can even say something like

let x = string-of-int(x)

and the rhs will take the value of x (a well-typed integer variable from the previous scope, and the lhs will introduce a new x (a well-typed string variable) in the newly created scope.

this is an orthogonal thing to static/dynamic typing, incidentally; for instance in ruby you can say

    a = 10
    (3..5).each do |a|
      puts a
    end
    puts a

and you will get

the a within the do loop being a new variable that happened to have the same name as the a in the outer scope, but referring to a different actual variable.

Yes, my point is that the fact that "x" refers to two different variables is a feature of the language, not the type system.

    f(x) + g(x)

For any type of x is enumerable. What that means is that for this specific expression, you can enumerate all of the types that x may take, and then enumerate all of the types that a function would return, given the types (if you can). You can then decide whether this expression is true or not.

Now it depends on the implementation of f and g. And type systems, in most of the practical cases - would be able to deal with this.

    x = 1
    print_int(x)
    x="a"
    print_string(x)

The second example is always decidable, if we agree that semantics of '=' are generally a question of equivalence.

I think the argument for untyped languages is their simplicity. There are lots of things that are trivial to express in a dynamic language but that require extra features on the type system to be able to write on a statically typed language (parametric polymorphism, subtype polymorphism, datatype introspection, and so on). Sure, there are type systems for all of these things but it is hard to have a single type system that does everything at once because things quickly become very complicated and type inference gets harder.

Your definition of order is not the standard one!

Usually one would have:

    zerothOrderFunction :: a
    firstOrderFunction :: a -> b
    firstOrderFunction' :: a -> (b -> c)
    SecondOrderFunction :: (a -> b) -> c

After all, the functions firstOrderFunction and firstOrderFunction' are the same up to currying.

The standard definition of order is given here (at the end of the section):

https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#T...

> On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts.

This happens quite often. Take datastructures. It is often very useful to structure different types of data together in a common structure. Now in most cases, you don't know in advance which type will go where in the datastructure, as the data might only be known or derived at runtime.

In fact I'd say dynamic behavior is the major expressiveness loss. Granted, I'm not sure how runtime vs static type system relate to type theory. Anyone can educate?

> It is often very useful to structure different types of data together in a common structure.

"Very useful" often just means: coding a properly typed, easily-understandable solution takes longer than doing it untyped.

I argue that is the case only when using a plain-text editor. When you have a good IDE for a typed-language at hand that can refactor, complete, analyed and follow code on the press of a button, you lose this "advantage" of untyped languages.

How do you define expressiveness? To me, it means saying more with less. Applied to code it means doing more with less work. Which directly translates to productivity gains.

Now, what IDE and language are you referring too? The best one I've used was VisualStudio for C#. While I'd say typing wasn't adding too much overhead in it, its type system is also poor, and it's arguable that it may not really prevent much bugs. Now, it does help make C# faster.

IDEA with Kotlin or Java is fantastic.

It’s partly just coincidence that dynamically typed languages tend to have less expressive type systems. You could run any typechecker at runtime if you wanted. There’s no reason you couldn’t have a Python-like language where the “list” type dynamically keeps track of the types of its elements, function types keep track of the types of their inputs and outputs, and so on, to give you more precise & useful dynamic type errors. That would let you do some interesting things like creating a type from runtime data, such as a database schema.

It’s just that historically people have found it markedly more useful to have that information available statically, because it lets you prove things about your code that hold “for all” cases (universals), not just “for some” that are executed (existentials). And static information can be used for optimisations because of those guarantees—if you have proof, you don’t need a fallback.

Can you explain what you mean by comparing universal and existential quantification to dynamic languages? Existential quantification is often used in statically typed languages and can be valuable in some cases (no pun intended). In Rust, for instance, you can say fn f() -> impl Fn(u8) -> u8 or something similar. This is existential quantification, because you're saying that f returns a type that is some Fn(u8) -> u8. This can expressiveness can be powerful in a type system. I don't see how it relates to dynamic languages.

I’m not referring to existentially quantified types—which are definitely useful & interesting in statically typed languages. What I mean is that with static types you can prove universal properties of functions.

If you give me an unknown function f : ∀T. T → T in a statically typed language, then I know it always returns a value of the same type as its argument. With some assumptions (purity, parametricity, halting) I even know it must be the identity function.

Whereas doing what I’m suggesting in a dynamically typed language, running inference dynamically, I could only recover existential properties: that there are some types for which f returns a value of the same type as its input. So I could recover more and more information (in the form of an intersection type) by calling the function with different inputs:

f : int → int

f : (int → int) ∧ (string → string)

f : (int → int) ∧ (string → string) ∧ (Foo → Foo)

But I could never arrive at ∀T. T → T, because that’s essentially an infinite intersection.

ETA: actually I might not even be able to get this much information; I only know the output type for each input value, not each input type.

I see what you were getting at now, thanks.

You create a reference cell containing an empty list. Because the cell is mutable, it can't have a polymorphic type - it must have a monomorphic one. How do you determine at runtime the type of this cell, before the first time you mutate it?

What I’m suggesting is that you could literally just run HM or another typechecker at runtime. You’d give an empty list the type “list<T>” for a fresh type variable T; appending an integer would introduce the constraint T = int; appending a string would introduce T = string and raise a runtime error. (Or not—it’s up to the typechecker if it wants to degrade to “int|string” or something.)

At runtime, the original program (i.e., the syntax tree, or some other representation from which the syntax tree is recoverable) may well not exist anymore. If you don't have a syntax tree, you can't type-check anything.

Now, you may say “okay, the original program doesn't exist anymore, but my language implementation is a term rewriting engine, so I have a current program that I can submit to the type checker”. Alas, most type checkers, Hindley-Milner included, operate on self-contained program fragments (i.e., not containing unbound variables), so you can't just submit any arbitrary program fragment. And, if you didn't want to type-check your original program, how likely is it that you will want to type-check the entire syntactic representation of the current program state?

Who says you need a syntax tree? You just store a byte of metadata next to each variable with the type. There should be more than enough data from that to recover the parts that you can't store like that and do type inference on them.

Why is that required? There's nothing stopping you from only giving the list a precise type after an element has been added. This mirrors the way statically typed languages with inference handle the same situation (except they wait for evidence that it's being used as a list of Ts, instead of the actual act).

> Why is that required?

Say, because you want to use that reference cell in two different threads.

I think I see what you’re getting at. If I create an empty mutable list and send a reference to it to two different threads A and B, where A adds an integer to the list and B adds a string, then it’s nondeterministic which thread raises a type error.

And degrading the type to a union (int ∨ string) as I mentioned is still nondeterministic even though unions form a lattice—I can recover determinism when writing to the list in both A and B, but supposing A writes first, B writes second, and then A reads expecting only integers, it gets a type error because it hasn’t checked for the string case.

But I’d argue that 1. this is bad form and you want a type error somewhere and 2. you have this problem already with type-changing mutable references in a dynamically typed multithreaded language. (Say just “int” and “string” instead of “list of int” and “list of string”.)

I need a container type that can be empty, because I need the monomorphic type of the cell to be undecided until the reference has been handed out to the worker threads.

If your program doesn't have a race condition, then you're fine. And if it does, then the list being monomorphic is not going to help (try your scenario with a C++ vector or Java ArrayList).

If your standard for a possible programming language that supports concurrency is that no data races are possible, then there's very few languages to be had.

This particular discussion wasn't about ruling out data races (although, of course, that is important too). It was about ruling out trying to read a list of strings from a reference cell containing a list of ints.

You're the one who brought up threads as a reason runtime monomorphisation doesn't work. If access to the list is properly synchronized, then what I proposed works just fine (you get your runtime error in whatever thread accesses the list second). If it's not, then unless you're using a concurrent data structure you're already screwed. The type system will at most change exactly how you get screwed.

What a great piece!

I wish the author would expand on this piece with either more installments or a even short book.

I find myself interested in type systems as it relates to programming language design but I haven't found much middle ground between the basic types described in introductory texts about a language and the opposite extreme heavy academic texts such as the ones the author is breaking down in this article.

Can anyone recommend any other such middle ground resources on type systems and type system theory?

> Can anyone recommend any other such middle ground resources on type systems and type system theory?

I really enjoyed Pierce's Types and Programming Languages. As I recall, he starts with the simple untyped lambda calculus, and builds a motivation for a type system, as well as the type system itself. It then switches to ML (or perhaps OCaml) and shows how features can be built-in to a type system as they're described.

I think it's a good fit - I know you said not heavy academic texts, but I don't think it's too heavy, it's at the level of an introductory undergraduate course. (Beware Advanced Topics in ~ by the same author which probably is on the heavier end, I don't know, I haven't braved it yet!)

What do you consider basic? Algorithm W for ML type inference is pretty basic, but powerful too. Or are you looking for something even more expressive?

What I meant by basic was the description of types provided by a language - usually in an introductory text you might read when learning a new language. I probably didn't articulate that correctly.

But I guess what I was referring to as a "middle ground"qa any resources for learning about types systems written in a similar approachable tone like this article.

This was another article I read recently that I thought was similarly accessible on the subject of types systems:

https://medium.com/@thejameskyle/type-systems-structural-vs-...

So I guess I'm wondering if there exists such a book or series that might allow one to further their knowledge of type systems without requiring university study.

Types and Programming Languages is the go to book, and it's very accessible despite being a textbook:

https://mitpress.mit.edu/books/types-and-programming-languag...

You can find some earlier PDF drafts online if you Google.

I have the book and I must warn people, it is not THAT accessible - this is not evening reading for an hour, this is work.

You'll have to define accessible then. Learning anything takes work.

funny to me, that HN brings up "Godel, Escher, Bach" in the most general of situations but not when someone's specifically asking for it. enjoy! :)

There's another approach, from Boyer and Moore. Boyer and Moore built up mathematics from constructs at the Peano axiom level (zero, add1, etc.) plus recursive functions that must terminate. It's constructive mathematics; there are no quantifiers, no ∀ or ∃. [1] They built an automatic theorem prover in the 1970s and 1980s that works on this theory. (I recently made it work on Gnu Common LISP and put it on Github, so people can run it again.)[2]

In Boyer-Moore theory, all functions are total - you can apply any function to any object. Types are predicates. Here's a definition of ORDERED for a list of number:

    (DEFN ORDERED (L)
      (IF (LISTP L)
          (IF (LISTP (CDR L))
              (IF (LESSP (CADR L)
                         (CAR L))
                  F
                  (ORDERED (CDR L)))
              T)
          T))

If L is not a list, it is considered to be ordered. This makes it a total function, runnable on any input, even though the result for the "wrong" type is not useful. This provides the benefits of types without requiring a theory of types. It's a very clean way to look at the foundations of mathematics. It's simpler than Russell and Whitehead.

When you prove things using definitions like this, there's a lot of case analysis. This gets worse combinatorially; a theorem with four variables with type constraints will generate at least 2⁴ cases, only one of which is interesting. Most of the cases, such as when L is not a list, are trivial, but have to be analyzed. Computers are great at this, and the Boyer-Moore prover deals with those cases without any trouble. But it went against a long tradition in mathematics of avoiding case analysis. That made this approach unpopular with the generation of pre-computer mathematicians. Today, it would be more acceptable.

(It's fun to run the Boyer-Moore prover today. In the 1980s, it took 45 minutes to grind through the basic theory of numbers. Now it takes a few seconds.)

[1] https://www.amazon.com/Computational-Logic-Robert-S-Boyer/dp... [2] https://github.com/John-Nagle/nqthm

If every operation can have any type arguments applied to it and does something sensible with no compiler or run-time error ... good luck debugging, surely.

What happens with OOP? Every class has to understand how to "bark", not only the dog class?

If any class can somehow "bark" without throwing an exception, that may not be in alignment with the programmer's intent, or promote the furtherance of his or her goals in any way.

For intance, the intent may be that the programmer wanted to ask the local variable dog to "bark", but misspelled it as ndog and the integer which counts the number of dogs was asked to bark instead.

There is much value in identifying the problem that an integer doesn't bark.

Boyer-Moore theory has "shells", which are like structures. See page 39 of [1]. Since this is a pure functional language, values cannot be altered. Shells have constructors, a type predicate, and can have restriction predicates on values.

    Shell Definition.
    Add the shell ADD1 of one argument
    with bottom object (ZERO),
    recognizer NUMBERP,
    accessor SUB1,
    type restriction (NUMBERP X1),
    default value (ZERO), and
    well-founded relation SUB1P.

It's not intended that you run programs in Boyer-Moore theory, although you can. It's a proof tool.

[1] https://www.cs.utexas.edu/users/boyer/acl.pdf

I will have to read this to understand what we can prove with this; or rather, what kinds of wrongs in a program under this theory are usefully proved to be false.

---

Ouch; did you see that "overfull hbox" that got rendered out in the first line of paragraph 3 of the Preface? :)

Reminded me of Gödel's incompleteness theorems.

First incompleteness theorem

Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F.

Second incompleteness theorem

For any consistent system F within which a certain amount of elementary arithmetic can be carried out, the consistency of F cannot be proved in F itself.

Honest question. What in the article prompted you to think about Gödel and his theorems? Why were you reminded?

I'm not sure why pier25 was reminded, but Russell's type theory and Gödel's incompleteness theorem are closely related. They both arose in response to the foundational crisis in mathematics [1].

Russell stumbled onto Russell's paradox (among others) and it shook mathematicians' confidence that everything in math was built on top of a perfectly consistent and stable foundation. If you can define a set that it "the set of sets that don't contain themself" then what other kind of crazy talk can you say in math? How do you know proven things are true and false things can't be proven in the face of weirdness like that?

Russell tried to solve the problem by inventing type theory. Types stratify the universe of values such that "the set of sets that don't contain themself" is no longer a valid statement to make.

Meanwhile, Gödel went and proved that, sorry, no, math is not consistent and complete. There are statements that are true but which cannot be proven.

[1]: https://en.wikipedia.org/wiki/Foundations_of_mathematics#Fou...

Probably this part from the article:

> Similarly, type theory wasn’t enough to describe new foundations for mathematics from which all mathematical truths could in principle be proven using symbolic logic. It wasn’t enough because this goal in its full extent is unattainable.

I spent the whole article wondering when Gödel would be mentioned, and was disappointed that he wasn't given that the Incompleteness Theorem was at least partly a response to Russell's work, and because it applies directly to computer systems. The conclusions Gödel reached are asserted in the article but not cited which is weird given the other references.

I was reminded of Godel too. For me, it was the part of the article that described Russell's finding of statements that led to paradox, such as "I am lying." If you're allowed to talk about "the set of all sets", then you can state things that can't be dealt with logically. That reminds me of Godel's Incompleteness theorem.

For one, Godel used the same kind of self-referential statements described in the article ("this proposition is not provable" etc) and used math to create a kind of enumeration of propositions and have the proposition refer to itself.

I share the author's frustration with wikipedia sometimes - people usually go to wikipedia for a distilled, comprehensible description of the subject matter. What he quoted was certainly not comprehensible, even to someone well-educated in CS foundations.

I like it because of it. If what I found in wikipedia was the "easiest" description, I'd find it lacking. It is better to not understand everything on the first read than understanding almost nothing because of lack of profoundity.

I loved this because I have read most of the source material in the context of logic, but never made the lead to type theory in computer science.

Types are close to adjoint functors / adjunctions and partial evaluation. Assigning restricted information to part of a structure to gain knowledge through limitation (math).

The category-theory window onto the world of types only appeals to a small subset of human minds.

For the average programmer you may as well be spouting gibberish because the average programmer will have no way to evaluate the claims (if any) you are making. Note, I am saying that you may as well be and not that you are. Please do not misunderstand me.

Types systems certainly are formal theoretical systems but I personally have come to believe that the majority of coders are ill-served by the mathematical leanings of type theorists.

I'm not sure I can explain myself better than that at the moment.

Do not worry I understand 99% of your message. It's indeed a land far far away from the everyday coding of the majority of programmers. Unless they start digging, which I did. If you take code as data (lisp roots showing) you start to want to reason about it and quickly you end up reading about FP, denotations, different forms of evaluations, the value of metadata (type or else).

Now I believe there's an artificial split between math leaning people and pragmatics, the former end up as PhD, the latter in IT or close. But in reality the average coder could understand and even enjoy the land of abstractions, it's just that the river he swims in isn't flowing there so one has to run against the flow.

Not to say that ideals are the only-tru-way.

I am delighted you responded so positively to what I wrote and didn't take what I wrote negatively which you could easily have done.

Let's for arguments sake say that there are two camps (broadly speaking), the pragmatists as you say and the theorists/idealists let's call them. It reminds me of the difference between someone like Torvalds and someone like Stallman.

Thing is we need both! You're right, the split _is_ artificial. The Linux kernel couldn't wait for someone to come along and create a type-awesome version of C. I mean, Rust seems to be the first attempt to take what type theorists have learned and apply it to a systems programming language. In the meantime software needs to be written and we have the tools we have.

If the fruits of type theory are going to filter through into software development I'm not sure it should come laden down with category theory (as awesome as that is) or the lambda calculus (as mind-bending as that is). I could of course be dead wrong.

A guy tried to make a C-level formal language, even sexp based at first. After years he quit, saying it's probably impossible to have both (he wrote a long long article about the reasons, he didn't leave without explaining every problems in details).

Usually ideas filters in tiny bits, kind like genes. See closures, forever in lisp, but now in every languages while lisp is still niche.

The issue with theorists is that they see the world in abstract algebra / combinatorics, it's not fluff, it's just extremely high level thinking with extremely short notation[1]. It looks like straight BS until you spend enough time seeing that it translates into reality. Say something like prolog, where a few rules give you graph coloring. It's not theory only, it's actual application of different semantics.

[1] also, as in any group, they developped a culture and taste for some things, expressing everything in the form of arithmetic expressions. F^n <= iteration of F n times, it's a loop in average coder lingo.

This was fantastically well stated.

Type theorists are people who understand arrows very well -- as long as those arrows aren't pointers. :)

ba-dum tss! are you here all week?

Sure---if catering keeps that sirloin roast coming for another seven days. Have you tried it?

Type Systems come from Russel - yup. But the notion of Type has an interesting origin in the west as well (I would love to read/understand histories of this concept from other cultures, but I am ignorant for now).

My reading is that it was invented by Scotus as Haecceity ! This was required by Catholic Christianity because of the difficulty that The Creed introduces about the identity of God - there are three entities which represent God, the Trinity - how to account for this? Well; the thisness of God is joined with the thisness of man, the thisness of the creator and the thisness of the thing which is motion (I have never understood The Holy Spirit). You can think of this as multiple inheritance! Theologians then had to account for "why three" as you can carry on making aspects of god with this mechanism infinitely, god the mother, god the lover, god the hunter and so on. But there are three - why? The answer was provided by Scotus's student Occam, entities should not multiply beyond necessity and hence there are three aspects of god because it is necessary for creation that there are.

The fun bit it that this procession of thought is somewhat guessed at because writing things like this down or debating them publically was a quick route to the afterlife via a bonfire!

> The fun bit it that this procession of thought is somewhat guessed at because writing things like this down or debating them publically was a quick route to the afterlife via a bonfire!

Theatre and Philosophy have always been able to have a lively chat with one another

This article was very well written. It finally clicked for me why "hugher-order functions" are named the way they are.

Any more articles in this vein?

"Even though theoretically, type theories and type systems are not enough to prevent all the problems in logic and programming, they can be improved and refined to prevent an increasingly number of problems in the practice of logic and programming. That means the research for better practical type systems is far from over!"

This is great point, and I think it is absolutely worthwhile to put time into researching better, more powerful type systems.

Tony Hoare said[1] that his research into formal systems and his hope that the pr Framing world would embrace these new innovations that increase safety and reliability was futile, but I think what we need is a new approach, with particular care given to practicality and adoptability.

[1] https://en.wikipedia.org/wiki/Tony_Hoare

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

I believe you get an actual interest for type systems when you start using a rich one. Unfortunately, most mainstream languages have very poor type systems. In particular, it will come naturally over time if you start using languages like OCaml, F#, Scala, Rust, Haskell, ...

There’s the technical aspects of the fact that every language has to have some notion of “type”. And seemingly interpreted languages might be JIT-compiled etc. This is of interest if you care about the implementation of languages.

Then there’s the opinions that users of languages with more elaborate, expressive type systems have, like how some people really enjoy Haskell or Elm because they feel that the type system helps them express their ideas clearly, avoid errors, and aids refactoring and maintenance.

If you’re worried about this one, don’t I guess? If you can use dynamic languages to achieve your goals, and you like them, then that’s fine! There are plenty of languages you can play with if you want to get a feel for programming with types. Even Java 8 and C++11 are decent at this point (I’m sure a Haskell programmer is fuming right now).

Then there’s like, a few thousand people in the world who have well-informed opinions on research into the theory of programming languages, the Curry-Howard correspondence between types and proofs. Also a lot of Hacker News posters who have heard these words. Some of them pretend like they know what they’re talking about.

> There’s the technical aspects of the fact that every language has to have some notion of “type”

This isn't true. There are no types in lisp or untyped lambda calculus.

Common Lisp has a primitive type system. Some implementations use that for compile-time type checks:

An integer type I1 from 0 to 65535.

    (deftype i1 (&optional (min 0) (max 65535))
      `(integer ,min ,max))

The function foo gets an integer and returns an I1:

    (declaim (ftype (function (integer) i1)
                    foo))

    (defun foo (i)
      (mod i 65536))

    (defun test ()
      (foo 6712312)       ; okay
      (foo 311212.2))     ; wrong call

Let's compile it in SBCL, a Common Lisp compiler:

    ; compiling file "/private/tmp/test.lisp" (written 08 JUL 2017 11:10:09 AM):
    ; compiling (DEFTYPE I1 ...)
    ; compiling (DECLAIM (FTYPE # ...))
    ; compiling (DEFUN FOO ...)
    ; compiling (DEFUN TEST ...)
    ; file: /private/tmp/test.lisp
    ; in: DEFUN TEST
    ;     (FOO 311212.2)
    ; 
    ; note: deleting unreachable code
    ; 
    ; caught WARNING:
    ;   Constant 311212.2 conflicts with its asserted type INTEGER.
    ;   See also:
    ;     The SBCL Manual, Node "Handling of Types"
    ; 
    ; compilation unit finished
    ;   caught 1 WARNING condition
    ;   printed 1 note

As you can see that it detects the type error.

The type system has been defined for Common Lisp with its first version in 1984. It had been used to allow the compiler to generate optimized code or to do more precise runtime checks. Early on in the mod 80s the CMUCL compiler then added the idea to use these type declarations as type assertions and to check those at compile time.

Actually, there's one type.

If you're going to shove the system into a typed model, then sure there is one type. But then you've kind of missed the point...

If you're going to answer the question of whether a language has types, then you're already trying to see how it can be shoved into types. It's presupposed by the question itself.

You literally have to count the types by analyzing the grammar. So for the lambda calculus, you have lambda=1, halt. So does a single type mean no types or literally one type?

What's the advantage of thinking that 1 type actually equals 0 types? I don't see any, so in my mind, all languages are unityped or have a richer type structure. Whether a richer type structure is desirable is a separate question.

I learned set theory and discrete math from this guy:

http://internethalloffame.org/about/advisory-board/cl-liu

Easily my second favorite instructor, possibly my favorite. I felt pretty prepared to deal with analysis and design in statically typed languages just from that grounding in set theory and logic. Fond of saying things like, "We have a box. What's inside that box? Another box. What's inside that box? We don't care."

Now retired, he was an early proponent of distance learning, so surely some of his stuff is accessible still.

One of the things that's so wonderful about writing software as a profession is that there is a ridiculously huge array of use cases for different languages and styles.

There's nothing wrong with not caring about type systems if they don't make your life or your job better or worse.

As long as you enjoy what you are doing, everything else is optional.

I didn't start caring about type systems until I started running into cases where I really wished for a static one (when I was working on a large system in Python) and later when I was prototyping things where I had to make a lot of guesses in C#. Both situations frustrated me, and then I got to start really caring a lot about type systems.

To a certain extent, I think it's human nature that we often don't really start caring about things that much until we experience real, personal frustration with them. Then we start caring a lot.

The reason you see so many people weighing in on this here on HN, is that many regulars are the kind of person to start feeling pain very very soon and over small inconveniences where other people will just sort of deal with the minor inconvenience and focus on other aspects.

One attitude is not better than the other, nor is one more ideologically pure or a marker of a better programmer or engineer. The only thing it implies is different pain thresholds.

Depending on your area of focus as a developer a low or a high threshold could be either a benefit or a drawback. A language designer needs to have a very low threshold. A front-end developer/designer can afford to have a very high threshold and focus on things besides being provably correct.

One of the things I like the most about software engineering is that there are opportunities for joy and discovery for everyone. And as careers progress, you can easily find yourself caring about different things at different times, and there's nothing wrong with that.

There's nothing to be ashamed of any more than you should be ashamed of preferring strawberry to chocolate ice cream. (Although, in keeping with tradition here on HN, if you say that you prefer strawberry ice cream, you are dead to me and practically Hitler. :).

Type systems /don't/ underly the technology we use every day. The vicissitudes of real computer architectures do -- and those ain't type systems.

I don't think it's common for programmers to have in depth opinions about type systems. And most of the ones who do may not really know what they're talking about.

> I get that these underpin the technology we as programmers use every single day

Is this actually true? Of course Haskell, Idris, etc. leverage type theory, but how much type theory underlies the type systems of widespread practical languages like C# or Java? Can something like C++'s SFINAE be grounded in type theory, or is it just a hack?

C++ metaprogramming might not be pretty, but it's extremely expressive, I'd be surprised if it didn't have some kind of type theoretic background.

To each his own path. Maybe you'll change course, maybe not, maybe type theory will evolve (HoTT comes to mind).

I can't seem to grasp HoTT.

Are there any approachable resources on the subject?

Have you tried reading the articles linked to on this page? http://www.bris.ac.uk/arts/research/projects/homotopy-type-t...

There is an official book which is very well written. I remember that I started to read it several years ago and was surprised that I actually can understand most of the things.

I only read two pages on homotopy so far, I cannot answer that :)

I feel your pain: after bouncing off Haskell many times, I found that Elm was a great entry into a more practical and narrow way of experimenting with the benefits. Now I'm reading through the new Idris book, which has the same practical approach to more complex (to me) concepts.

What languages have you tried? I think once you experience a language with types outside of the run of the mill Java/C#, you will get more excited about it. Ocaml, Rust, Haskell, Purescript, etc. Haskell for me was the one that got me excited about types.

ive only used vbscript and javascript extensibly. when ive tried java and #C ive been annoyed by the verbosity of types. and when looking at haskel or ocaml im just confused. for me types are an optimization or extra documentation for undescriptive naming, like str x, int y, list z. vs. name,age,friends. so i want to know what im missing, will there be less bugs and regressions? will i be more productive ?

> for me types are an optimization or extra documentation for undescriptive naming,

This is one of those things where you should try to reserve judgement about it because your experience is so limited. Modern typed languages often don't even require you to write the type, because of type inference.

> will there be less bugs and regressions? will i be more productive ?

The idea with static analysis is that you're pushing more errors into the type system so it's caught at compile time rather than runtime. Everyone will answer this differently.

IMO a dynamic type system doesn't make you more productive because the same invariants you have from not having an explicit type still exist in the code, they just go unchecked. For example, if I write a function to add 1 to a number, in a dynamic language if I pass a string I'll get some output that is invalid if I'm expecting the result to be a number elsewhere. Types let you encode those invariants. But encoding simple types and primitives is really just scratching the surface, I could ramble on for ages here but you should just dive into a language with a good type system (like Haskell or Ocaml like you mentioned) and stick with it long enough to give it a chance. It's so much more than just being and to say 'int' or 'string'.

Speaking of adding to a number, in some dynamic languages, you can add 3/5 to 7/5 and the result will be 2, of type integer, indistinguishable from the object produced by a literal 2. That 3/5 and 7/5 come from some run-time source, so the result type can't be statically hard-coded to integer or rational or whatever. And so now on the static side you're into variant types and "maybes" and other junk creating an incomprehensible soup which basically Greenspuns dynamic typing in a way that will get your name cursed by subsequent maintainers.

I can't make heads or tails of what your criticism is. Algebraic types are wonderful, I find it difficult to code in a language without them. I'd hardly call it 'junk'.

>I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems.

Not even 1/10th of HN has that. Tons of business types, lowly JS programmers, designers, sys-admin types, old-school programmers in C/C++, etc around.

It's never too late to bother trying. If you think it'll benefit you in life, just go for it and study it.

If. I suspect that smcl can't get excited about type systems because of not seeing the benefit.

For me, types are sets of possible values, plus sets of valid operations on those values. I don't much care where they come from. As far as I am concerned, they are an engineering construct to make programming easier and safer, and are interesting only to the degree that they accomplish those goals. Any connection to pure math is completely incidental; if there were no such connection, it would not make (programming) types any less useful.

Now, math often gives deeper insight into what's going on, and enables you to create more powerful (useful) abstractions. But if the useful abstractions don't correspond perfectly to types as used by mathematics, I don't care.

Yes, precisely.

I'm very interested in theory (by the standards of non-academics). I'm very interested in pragmatic type systems. I've spent a few hundred hours on trying to learn type theory, in the mathematical sense. The only thing I have personally found useful, so far, in type theory, is the notion of sum types and product types. But that's just jargon for things I was able to deduce from a shallow study of many programming languages, so even that has not been that useful to me.

On the other hand, I entirely agree with you, that what a type is to a programmer is a set of values and a set of valid operations on those values. Exactly. That's what types mean when you're working close to the metal ("this value is meaningful as a 16-bit float; if you try to dereference it, the consequences are mightily hard to reason about"). That's what types mean when you're talking about the function signatures of higher-order functions that use generic types. That's what types mean when describing statically-typed variables, and what types mean when describing dynamically-typed values.

I see some signs that a few other people share my interest. For example, using dependent types to e.g. specify that two sequences can only be zipped if they are of the same length; that's a useful type-check, and if it can be determined statically, that's great (that's a toy example, of course). Unfortunately, most of the languages that contain these features seem remarkably impenetrable.

I am very interested in situations where math reveals underlying truths about the universe. Like you, I'm so-far unpersuaded that mathematical type theory is a useful avenue to learning about powerful abstractions about types in programming.

I don't think approaching type systems from the mathematical angle is much help either. When I was learning Haskell, I started to try to learn category theory to develop a better understanding of what was going on. In the end I decided my time was better spent learning Haskell, and not category theory. Where they share words I look shallowly into the mathematical concept, but the understanding I develop is how it relates to me in a programming context. That doesn't mean I don't value that there is a mathematical basis for it though.

> That’s the equivalent of writing type annotations for programming functions. And the goal is avoiding bugs instead of logical contradictions.

mh, given Curry–Howard correspondence, aren't those the same? so the goal is indeed not having logical contradictions?

Yes. But it's a rare programmer, or even a programming language designer, who thinks of well-typed programs in terms of proving theorems.

They are. I avoided introducing an explanation of Curry-Howard isomorphism because I think that would not be very intuitive to many people because the most commonly used type systems have very little power to express logical properties about the program.

I may write another article about this.

It's actually just a belief. Nothing suggests that type systems and type theories can be improved to be practical at preventing bugs. I'd say it's the opposite, even with as much understanding about the nature of bugs as we have today, they don't look very promising, unlikely to make it even into the top ten of other different approaches.

Incendiary though the phrasing is, I'm halfway inclined to agree with you. There's a lot to be said for a solid, simple strong typing system. But some of the more sophisticated type systems that I either seen or read research literature about (I had a colleague who was doing PhD research in 'refinement types') are seem like they are hitting diminishing returns for programmer ease-of-use while catching an ever-diminishing number of bugs.

If you allotted me a finite amount of effort to put a codebase (a) into a strong type system, (b) festoon it with lots of pre- and post-conditions and asserts, (c) run it through every static checker under the sun, (d) build a huge suite of tests, (e) find a way to formally verify critical algorithms in it with (say) Z3, (f) carry out fuzz testing, ... I'd probably say "do the easy stuff from most of these categories" rather than "pick the One True Path and figure that that will save you from all your bugs".

There are type systems that prevent race issues, use after free, and null pointer exceptions.

So saying that they aren't practical at solving bugs is a little disingenuous.

Well... how much of actual software is written using those type systems? Less than 1%? So such type systems might be able to prevent bugs, but in practice, they don't.

Why aren't they used? Probably existing code bases, inertia, and ignorance play a role. I suspect, though, that at least part of the problem is that most programmers find those type systems too hard to use. In that sense, the type systems aren't practical.

And if you're going to blame the programmers for that, well, if your plan for making programming better requires different programmers than the ones we have, your plan isn't very practical, either.

Today less than 1% of all software is written in null safe languages. But I believe Swift has non-nullable types, and it's the promoted language for a really big ecosystem. There's also Rust and Scala, but those have less of a captive audience. I do have high hopes for Rust, which also is data-race safe.

I think Java 8 and optionals show it doesn't have to be that hard, it's just that there's too much old code that relies on nulls for the Java ecosystem to ever be fully null safe.

Use-after-free is solved in a language without manual memory management, so that's actually quite common.

Programmers get comfortable with new ideas over time. Higher order functions and type inference used to be obscure concepts. Today they're par for the course. I don't know if we'll all use dependent types some day, but I think we'll keep getting more powerful types in mainstream languages for a while.

Kotlin is plenty practical. It was born out of a desire for a safer yet practical language on the JVM (provides null safety at the type level). It is at least practical for it be getting gaining lots of traction.

Rust is another good example. It's not very ergonomic, but it is getting better every release.

I think how those two languages do will show whether type systems can me made practical for reducing wider classes of bugs. They seem practical and have the backing to help drive adoption.

> So such type systems might be able to prevent bugs, but in practice, they don't.

Rockets might be able to carry humans up to space, but in practice they don't because only a small set of humans actually get to go.

Isn't that a slightly absurd interpretation of "in practice"?

Why these languages aren't used may have absolutely nothing to do with their technical merits. It's a myth that technical merits is the only consideration for language popularity.

Could you say what type systems those are? Thanks.

To protect against NPEs you need to make nullable and non-nullable types different and forbid the programming from trying to use a nullable value without doing a null check first (doing a null check returns a non-nullable reference in case of success). One example of this is any of the languages with Albegraic Data Types, where it is super easy to create an Option type that encapsulates this concept.

For an example of preventing use-after-free there is the typesystem used in Rust. It is based on the theory of linear types, which lets you have operations that mark a value as "used" and forbid you from using it again after that point. The same system is used to protect against data races because you can guarantee that a value is only accessible from one thread at a time.

Thanks, this should make for some interesting weekend reading.

I'm assuming parent is thinking of Rust. And more generally type systems relying heavily on linear types (I believe).

Rust's borrow checker isn't a type system, is it? Sure, its benefits are similar to a linear type system, but actually it's a separate compiler pass whose internals are described imperatively and don't look type-based to me: https://github.com/rust-lang/rust/blob/master/src/librustc_b...

If anything, I agree with zzzcpan and disagree with swsieber. Types are nice but people oversell them. OO languages appeared at the same time as ML family languages, but one got successful and the other got stuck in the realm of "new ideas".

It wouldn't be possible without an affine (at least) type system such as Rust's.

Affine logic rejects contraction, i.e.

     Γ, A, A ⊢ B
    -------------
      Γ, A ⊢ B

My intuition (so take a liberal dose of salt) is that this pretty directly translates to disallowing reuse: we can't see a type twice and continue (inference) as if we saw it once.

Of course, that's very hand-wavy, and doesn't say (as I believe is the case) that there wouldn't be some other way to proceed through a combination of other rules.

It could be at least argued that type systems aren't very effective at reducing meaningful bugs and/or aren't worth the costs they impose, but you went way beyond that argument. As I see it, the only way you can believe that "nothing suggests that type systems...can be improved to be practical at preventing bugs" is because you have willfully ignored or completely discounted every bit of evidence you've encountered that suggests otherwise.

> It's actually just a belief. Nothing suggests that type systems and type theories can be improved to be practical at preventing bugs

Seems you don't know much about types then. I suggest you look up theorems provers and compcert and the TyPiCal language, as but a few examples.

"Practical" is the key word here, I believe.

A key word that had been disproven many times. The most recent example is Rust, which has a type checker that now type checks many previously unsafe C++ idioms. The other examples I listed are also quite practical, and have been used in high assurance systems.

What are the other approaches for preventing bugs you have in mind that are novel or increasing in application?

We've done testing since the start. Still many bugs. We've done ad hoc modeling (behavior driven) for years with some improvement. Formal methods aren't popular but are successful at least at some (small to the low end of medium) scales or within portions of large scale systems. Type systems can and have been used for codifying concepts from all of these into the program semantics. So I'm not sure how it is that they don't help.

> We've done testing since the start. Still many bugs.

Exactly, as the OP clearly doesn't understand, but every researcher in programming languages does, test can only prove the presence of bugs, it cannot prove their absence. Types can.

what ive found most effective at finding bugs is to have two systems, the data represented in two different type systems, then cross check them on crucial intervals. the second most effective at finding bugs is to check function parameters both when entering the function and when returning from the function, for bound, range, etc. and third... study and understand the code, actually writing code that is easy to coprehend. then tests are very good at preventing regressions. despite this, there will still be bugs though smile so debuability, effective debugging is really important!

I guess you're just ignoring the fact that every single programming language in use today has some kind of type system? Are you clamoring for processors that don't even bother to distinguish between register sizes?

Type systems are a necessary part of computing. One can even define computing in terms of how types are transformed. Types are an extremely primitive and fundamental description of how computation happens, and without them, it'd be hard to imagine how anything could be computed at all, let alone correctly.

Lolwut?

He's right. The current type theory crazy is just another in a long line cargo cult programming fads. First it was pure OOP for everything, then it was pure FP for everything, and now it's types for everything. Yes they can be useful, but it's disingenuous to act like they're a cure-all. Most bugs aren't type related, and you're adding additional mental overhead with these extremely elaborate type systems.

I find that a significant fraction of the bugs introduced to the code bases I've worked on that have dynamic typing are due to issues that even a rudimentary static typing system would prevent at compile time. I'm struggling to grok how a language with no type system might look. Something post-modern and Picasso-esque? To use data in a meaningful way in a program it must be possible to reason about it, and that requires that it have at least some structure.

Assembly languages are untyped. Nothing prevents you from reinterpreting a memory address as a type it is not. (Except possibly alignment issues.)

That's not quite right though, is it? Nothing prevents one from "creative" interpretation of memory in, say, C, either, but it would be difficult to argue C is untyped.

The C type system prevents you from accidental creative interpretation of memory. You wouldn't say Rust is untyped just because of the `unsafe` keyword either.

No such type safety exists in assembly, except that certain opcode-register combinations are prohibited.

Types aren't new. As the article discusses they date back over a century at least in math and logic. Within programming, we've had them in every major language for decades. The first big push for strong and expressive type systems is from the functional programming work which led to the ML family and the work that made Pascal and Ada on the imperative (and later OO variants) side, which dates back some 40-50 years now.

What is "he" right about, exactly? You say "yes they can be useful", but that's not the impression I get from OP. I am also confused because the very quote OP is responding to states that "...type systems are not enough to prevent all the problems in logic and programming...". Do you consider that acting like type systems are a cure-all?

> Most bugs aren't type related, and you're adding additional mental overhead with these extremely elaborate type systems.

Are you? usually I find it to be the reverse - you're leveraging the type system to track some properties for you, so that you don't have to track them mentally. I.e. less mental overhead (though possibly more boilerplate-overhead)

For me, the elaborateness of the type system and it's checker REMOVE the overhead. YMMV, obviously.

I think you misread OP, and also misread the comment he was replying to; or, you just needed an excuse to vent about type systems.

I found Tomas Petricek's essay on "Against a universal definition of 'Type'" very informative. He argues that the word 'type' has shifted shape many times since Frege/Russel, in that the intuition behind them is different. He also argues that multiplicity of definition is a good thing.

http://tomasp.net/academic/papers/against-types/

Nice article about type theory.

> Why there’s so much research around types if perfectly applying them to programming languages is impractical?

Somehow Haskell does this perfectly. Whaddya say to that?

I say, citation needed. Who said "Haskell does it perfectly"?

Not to mention the mental overhead of Haskell (which is also not optimal).

Yeah, what the fuck? Most software engineers just want to get shit done quickly so they can go home to their wife and kids.

If you think this merits a downvote please tell why. Excuse my french.

Types aren't just for programming and philosophy. Strongly Typed Neural Networks are also a thing. https://arxiv.org/abs/1602.02218

TL;DR - Type theory == being careful about the domain a function can be applied in (adding meters to seconds or strings to sets should not be possible).

Don't they teach this stuff in school?

The school I went to barely taught C/C++ and the absolute minimum of PHP, CSS, Linked Lists, and Hash Maps. Very sad that so many actually smart people can't graduate knowing much just doing their course work. Let alone imagine those who lack off a bit and still pass. Unless you're programming on your own, like I was along with a few others, you graduate possibly in debt and completely unprepared.

So no, they never get in to this stuff.

No they don't. Only in some. Only if you're lucky.

We danced around the edges of set theory. Symbolic logic. Combinatorial and sequential logic (especially as applies to logic circuit design). Examples of a few families of type systems, how to use them, and the practical differences between them. We didn't tend to dive deeply into the mathematical underpinnings.

I've never taken a CS class.

Not everybody goes to school, and not everybody that does takes computer science.

Distinctly unimpressed by this post. The author seems to have an axe to grind with mathematicians as a class, which, as we would have been told in school, isn't 'big or clever'.

The whole of programming, nevermind types, perhaps the most mathematical part of modern programming, arises from mathematics. There's some good history here, but the early paragraphs in particular are a display of ignorance if not arrogance.

The author quotes Newton, the very chap who's said to have said he merely stood on the shoulders of giants (to 'see' such insight). Any programmer in the 21st century stands on the shoulders of mathematicians and computer scientists of the 20th,; who were in turn standing on the shoulders of the mathematicians of the 19th centuries.

>"Distinctly unimpressed by this post. The author seems to have an axe to grind with mathematicians as a class, which, as we would have been told in school, isn't 'big or clever'."

I thought it was intended to speak to people who might be intimidated or feel obtuse when they encounter really dense academic texts when trying to learn more about type systems as it relates to programming. As such I really appreciated it.

I didn't think the author was grinding any axes at all, quite the contrary.

I've no problem with that, it was the opening quotation, accompanying graphic, and following paragraph which read - to me, though I appreciate I may not have read it as it was intended - quite disrespectfully toward mathematicians.

Among whom I cannot count myself, for whatever it's worth.

I really don't think they have an axe to grind. What do they say that's incorrect? Their point is that much of what we see as type theory is inaccessible to the average programmer.

When we say that some field is inaccessible, we don't blame the reader trying to understand. At the same time we're not saying that the field is wrong either, but that communication could be improved.

Reply on news.ycombinator.com