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

151–160 of 171 posts

Re: Where Do Type Systems Come From?

#151

Post by evincarofautumn »

leshow wrote: post #141
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…

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…

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.

Re: Where Do Type Systems Come From?

#152

Post by leshow »

z3t4 wrote: post #148
leshow wrote: post #142

Earlier quoted context omitted.

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

Re: Where Do Type Systems Come From?

#153

Post by evincarofautumn »

catnaroek wrote: post #145
johncolanduoni wrote: post #131

Earlier quoted context omitted.

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

Re: Where Do Type Systems Come From?

#154

Post by ufo »

gizmo686 wrote: post #57
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 :-) Any type system will reject some correct program. As a trivial example, consider: if( f()…

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.

Re: Where Do Type Systems Come From?

#155

Post by leshow »

evincarofautumn wrote: post #151
leshow wrote: post #141

Earlier quoted context omitted.

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…

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 see what you were getting at now, thanks.

Re: Where Do Type Systems Come From?

#156

Post by catnaroek »

evincarofautumn wrote: post #153
catnaroek wrote: post #145

Earlier quoted context omitted.

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

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.

Re: Where Do Type Systems Come From?

#157

Post by johncolanduoni »

catnaroek wrote: post #145
johncolanduoni wrote: post #131

Earlier quoted context omitted.

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.

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.

Re: Where Do Type Systems Come From?

#159

Post by johncolanduoni »

catnaroek wrote: post #156
evincarofautumn wrote: post #153

Earlier quoted context omitted.

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…

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

Re: Where Do Type Systems Come From?

#160

Post by catnaroek »

johncolanduoni wrote: post #157
catnaroek wrote: post #145

Earlier quoted context omitted.

> Why is that required? Say, because you want to use that reference cell in two different threads.

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