Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Where Do Type Systems Come From?

blog.felipe.rs

Post reply on HN
Print view View original

81–90 of 171 posts

Re: Where Do Type Systems Come From?

#81

Post by naasking »

acchow wrote: post #74
currymj wrote: post #38

Earlier quoted context omitted.

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…

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

Actually, there's one type.

Re: Where Do Type Systems Come From?

#82

Post by didibus »

georgewsinger wrote: post #52

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…

> 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?

Re: Where Do Type Systems Come From?

#83

Post by naasking »

AnimalMuppet wrote: post #53
swsieber wrote: post #28

Earlier quoted context omitted.

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 pract…

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

Re: Where Do Type Systems Come From?

#84

Post by bogomipz »

naasking wrote: post #80
bogomipz wrote: post #68

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 articl…

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.

Re: Where Do Type Systems Come From?

#85

Post by ianamartin »

smcl wrote: post #2

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.

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. :).

Re: Where Do Type Systems Come From?

#86

Post by krallja »

sidlls wrote: post #41
chroem- wrote: post #22

Earlier quoted context omitted.

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 requi…

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

Re: Where Do Type Systems Come From?

#87

Post by gizmo686 »

zem wrote: post #79
gizmo686 wrote: post #66

Earlier quoted context omitted.

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…

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.

Re: Where Do Type Systems Come From?

#88

Post by evincarofautumn »

didibus wrote: post #82
georgewsinger wrote: post #52

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…

> 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 fac…

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.

Re: Where Do Type Systems Come From?

#89

Post by charlieflowers »

igravious wrote: post #24
pier25 wrote: post #4

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…

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

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.

Re: Where Do Type Systems Come From?

#90

Post by catnaroek »

evincarofautumn wrote: post #88
didibus wrote: post #82

Earlier quoted context omitted.

> 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 fac…

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 typ…

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?
Post reply on HN