Live data from Hacker News

Summer of Programming Languages

existentialtype.wordpress.com

21–30 of 78 posts

Re: Summer of Programming Languages

#21

> Nowadays serious industrial-strength languages are emerging that are grounded in theory and informed by practice. This seems a bit overly optimistic, but it's nice to see this kind of positive attitude for a change instead of "Why invent yet another language?". I am very excited about Swift and I have some respect for what Rust is trying to accomplish, but none of these languages have much foundation in category th…

The language godfather and access to alternative languages for a given ecosystem play an higher role than how good a language might be.

Hence importance of having Apple and Microsost bringing ML derived languages into the industry.

Re: Summer of Programming Languages

#22
post #9

Why do programming languages researchers seem so enamored with type-safe languages? It seems to be a given in academia that type-safe languages are not just superior, but significantly superior to type-unsafe languages.

Because designing type-safe languages is harder.

However, there is research into untyped/gradually typed languages. See, for example, [1] for combining gradual typing with type inference, and [2] for a list of papers formalizing the runtime semantics of a language that allows both typed and untyped functions.

[1] Gradual Typing with Unification-based Inference [2] http://homepages.inf.ed.ac.uk/wadler/topics/blame.html

Re: Summer of Programming Languages

#23
post #9

Why do programming languages researchers seem so enamored with type-safe languages? It seems to be a given in academia that type-safe languages are not just superior, but significantly superior to type-unsafe languages.

Types are no silver bullet, however one important point missed by all the other replies is that static types check all paths through the program, including rare/untested/error paths.

You can sometimes make up for this with lots of testing and detailed code coverage analysis, but that can be a huge amount of effort, and might be impossible in some cases (for example: how do you easily test that your program behaves well when it runs out of disk space?). Static types can fix this with a lot less effort.

Re: Summer of Programming Languages

#24
post #16

Earlier quoted context omitted.

> but none of these languages have much foundation in category theory or the ambitious kind of type system that Haskell has been pioneering for a while. Is that a requirement? If so, why?

I've never seen a "bolt-on" type system work, and I've used a few (e.g. JSR308). So I think it's something that needs to be built into the language itself. Having used a system with higher-level type constructs I find myself thinking in them. So many complex sequences of operations shake out as something much simpler once you realise the right monad, or arrow, or so on. And it becomes painful to manually expand it ou…

> I need either higher-kinded types or something equivalent to them.

FWIW it seems that many of the Rust developers want this for Rust.

Re: Summer of Programming Languages

#25
post #9

Why do programming languages researchers seem so enamored with type-safe languages? It seems to be a given in academia that type-safe languages are not just superior, but significantly superior to type-unsafe languages.

I would say its because academic researchers don't spend nearly enough time actually using these languages industriously in the worst-case scenarios. If more effort was spent in understanding how, for example, SIL-4 (safety integrity level 4) development is done with non-type-safe languages (hint: code coverage tests, tests, tests..), then there would (imho) be less motivation to continually churn out 'new solutions…

Let's just say that the attitude of IEC 61508 towards software development in general and programming languages in particular is not very spirit-lifting.

At least us software guys have an advantage: the hardware guys will always have to live with failure rates.

But the standard happily declares software to be bug-free, as long as you do the required testing and stuff. ;-)

Re: Summer of Programming Languages

#26
post #17

Earlier quoted context omitted.

I don't necessarily think they are wrong, but I also think that (as with most "silver bullets") type-safety is not without it's shortcomings. For example, consider the exponentiation function. When we raise an Integer to a positive Integer (2^2), the result will always be a positive Integer. You would expect the type of such a function to be: Integer -> Integer -> Integer Except, that's wrong. When we raise an Intege…

Any property that you can actually be confident about, you can encode into the type system. If you care that x ^ (y - z) is an integer, you'd better have some reason to believe that y > z. If you don't care or can't be sure, let x ^ (y - z) return Integer | Rational, and pattern-match for the cases (or treat them as some supertype, Numeric or some such). Or if you really can't figure out the proof but still think it'…

> Any property that you can actually be confident about, you can encode into the type system.

The big theoretical drawback is that you get an unbounded increase in program length. The reason is that programs in a typed language are proofs, and proof length cannot be bounded above by any computable function of proposition length.

The big practical drawback is that we just don't know how to explain proofs to a computer very well.

Re: Summer of Programming Languages

#27
post #22
post #9

Why do programming languages researchers seem so enamored with type-safe languages? It seems to be a given in academia that type-safe languages are not just superior, but significantly superior to type-unsafe languages.

Because designing type-safe languages is harder. However, there is research into untyped/gradually typed languages. See, for example, [1] for combining gradual typing with type inference, and [2] for a list of papers formalizing the runtime semantics of a language that allows both typed and untyped functions. [1] Gradual Typing with Unification-based Inference [2] http://homepages.inf.ed.ac.uk/wadler/topics/blame.html

"Statically-typed" and "type-safe" don't mean the same thing.

"Type-safe" means that the type of a value is always correct. For example, if I have a function of type Int -> String, a type-safe language will not let me pass it a Float argument, no matter what I do. A type-unsafe language might let me, if I can "cast" the value to a new type without changing its representation (ie. it's still a Float, but the type-checker now thinks it's an Int).

Type-safe languages are preferred over type-unsafe languages, since they avoid all kinds of problems like undefined behaviour.

"Statically-typed" means that every variable, function argument, return value, etc. is associated with (usually one, "principle") type. These may be written explicitly, inferred, etc.

"Dynamically-typed" means that all values use the same static type. This type is usually a recursive sum of lots of useful types, for example (in pseudo-Haskell):

    type UniType = I Int | L [UniType] | F (UniType -> UniType) | O (Object UniType) | E Error | ....
Dynamically-typed languages are type-safe, but in a trivial way: there's no way for a value to have the wrong type, since there's only 1 type!

Many users of dynamically typed languages don't realise that static types are being used "behind the scenes", because:

* All of their code has the same type, so there's no need for any annotations, inference, type-checking or compilation. Many believe it's because there are no types, rather than the fact these have been made trivial.

* Sum types and recursive types aren't widely known, especially to those using dynamic languages who don't need to care about types at all. Hence, many make the assumption that "I don't know how to type this code" implies "this code is untypeable" and refer to such things as 'dynamic behaviour'.

* Many dynamic languages are implemented in languages with unsafe, anemic type systems, like C. Since 'dynamic behaviour' can't be represented safely in these languages, it's implemented unsafely, reinforcing the assumption that dynamic languages aren't type-safe.

* Other dynamic languages are implemented in themselves, which hides the UniType underlying it all.

* A few dynamic languages are implemented in languages with strong, safe type-systems, where the UniType is explicit and obvious, but most users stick to the dynamic language and never look at the implementation.

* Many languages confuse terminology by using the word "type" to refer to tags (the "I", "L", "F", "O", "E", ... in my UniType above); for example "if (get_type(x) === "int") {...}" instead of "if (get_tag(x) === I) {...}", but this doesn't make sense: types don't exist at runtime and even if they did the "get_type" function would always return the same thing (the UniType). The fact that many languages represent tags as strings doesn't help either!

* Dynamic languages allow any variable to contain any value, but most of the time only a small part of this domain is expected. This causes most functions to be partial, but whenever this partiality is encountered, one of two things happens: a) the program fails with a "runtime type error", which is incorrect and doesn't make sense, b) the language supplies an error value in response, and is regarded as doing something "unsafe" or "untyped", when in fact error values are perfectly valid (I've tagged them with "E" above) and it's the programmer's fault for not handling all of the possible cases they (implicitly, via UniType) asked for.

The work you've linked to is about selectively weakening the types in a program, so rather than having the whole thing be unityped or the whole thing use distinct types, instead we can write code both ways, then automatically strengthen/weaken the types and lower/lift the functions, so that they interoperate. The types are always safe, but the unityped part will have many more partial functions than total functions.

In contrast, we can't (yet) make a type system "gradually safe", since a single unsafe cast can break anything else ("ex falso quodlibet"). It would require some kind of para-consistent logic, which I've never seen in type theory. The difference is that 'gradual types' let us say "Any" instead of "Int", whereas unsafe types let us say "X" instead of "Int", for any "X".

Re: Summer of Programming Languages

#28
post #9

Why do programming languages researchers seem so enamored with type-safe languages? It seems to be a given in academia that type-safe languages are not just superior, but significantly superior to type-unsafe languages.

There are also PL researcher who are enamored with dynamic languages. Alan Kay probably doesn't care much about static types.

Re: Summer of Programming Languages

#29
post #22

Earlier quoted context omitted.

Because designing type-safe languages is harder. However, there is research into untyped/gradually typed languages. See, for example, [1] for combining gradual typing with type inference, and [2] for a list of papers formalizing the runtime semantics of a language that allows both typed and untyped functions. [1] Gradual Typing with Unification-based Inference [2] http://homepages.inf.ed.ac.uk/wadler/topics/blame.html

"Statically-typed" and "type-safe" don't mean the same thing. "Type-safe" means that the type of a value is always correct. For example, if I have a function of type Int -> String, a type-safe language will not let me pass it a Float argument, no matter what I do. A type-unsafe language might let me, if I can "cast" the value to a new type without changing its representation (ie. it's still a Float, but the type-chec…

Well, to people like Bob Harper, there is no such thing as a dynamic "type" (they are tags instead). The argument over terminology appears on comp.types every once in awhile. Then there are people into dynamic languages who swear they have more than one type and actually check these types at run type. Then the static type theorists say...you are just checking tags, and the DL people are like...what's the difference?

Re: Summer of Programming Languages

#30
post #9

Why do programming languages researchers seem so enamored with type-safe languages? It seems to be a given in academia that type-safe languages are not just superior, but significantly superior to type-unsafe languages.

>Why do programming languages researchers seem so enamored with type-safe languages?

For the same reason people like unit tests. Only with mathematical rigor, checked by the compiler, and inspecting all aspects and code paths.

Post reply on HN