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

91–100 of 171 posts

Re: Where Do Type Systems Come From?

#91

Post by jholman »

AnimalMuppet wrote: post #10
Kenji wrote: post #6

Earlier quoted context omitted.

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…

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.

Re: Where Do Type Systems Come From?

#92

Post by zem »

gizmo686 wrote: post #87
zem wrote: post #79

Earlier quoted context omitted.

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

  3
  4
  5
  10
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.

Re: Where Do Type Systems Come From?

#93

Post by evincarofautumn »

catnaroek wrote: post #90
evincarofautumn wrote: post #88

Earlier quoted context omitted.

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?

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

Re: Where Do Type Systems Come From?

#94

Post by gizmo686 »

zem wrote: post #92
gizmo686 wrote: post #87

Earlier quoted context omitted.

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

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

Re: Where Do Type Systems Come From?

#95

Post by acchow »

naasking wrote: post #81
acchow wrote: post #74

Earlier quoted context omitted.

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

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

Re: Where Do Type Systems Come From?

#96

Post by mden »

bogomipz wrote: post #77
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.

Could you say what type systems those are? Thanks.

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

Re: Where Do Type Systems Come From?

#97

Post by cel1ne »

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

Re: Where Do Type Systems Come From?

#98

Post by cousin_it »

mden wrote: post #96
bogomipz wrote: post #77

Earlier quoted context omitted.

Could you say what type systems those are? Thanks.

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

Re: Where Do Type Systems Come From?

#99

Post by ufo »

bogomipz wrote: post #77
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.

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.

Re: Where Do Type Systems Come From?

#100

Post by dannyobrien »

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.

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