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

71–80 of 171 posts

Re: Where Do Type Systems Come From?

#71

Post by dvt »

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

Re: Where Do Type Systems Come From?

#72

Post by ky3 »

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

Re: Where Do Type Systems Come From?

#73

Post by swsieber »

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…

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.

Re: Where Do Type Systems Come From?

#74

Post by acchow »

currymj wrote: post #38
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.

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.

Re: Where Do Type Systems Come From?

#75

Post by naasking »

bykovich2 wrote: post #67
naasking wrote: post #43

Earlier quoted context omitted.

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

Re: Where Do Type Systems Come From?

#76

Post by rntz »

dvt wrote: post #71

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

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.

Re: Where Do Type Systems Come From?

#77

Post by bogomipz »

swsieber wrote: post #28
zzzcpan wrote: post #13

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

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.

Could you say what type systems those are? Thanks.

Re: Where Do Type Systems Come From?

#78

Post by naasking »

ky3 wrote: post #72
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. 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 do…

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

Re: Where Do Type Systems Come From?

#79

Post by zem »

gizmo686 wrote: post #66
georgewsinger wrote: post #61

Earlier quoted context omitted.

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

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")

Re: Where Do Type Systems Come From?

#80

Post by naasking »

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