Summer of Programming Languages • Hacker News Board

Re: Summer of Programming Languages

#71

Post by the_af » Mon, Jul 07, 2014, 9:34 PM UTC

fit2rule wrote: post #20

aidenn0 wrote: 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…

"Fact is, if you can't trust your language because of its type system, you develop tools to build that trust around your particular application of the language. If that is 'too much work for you' .. then by all means, avoid the work by reinventing the wheel."

But aren't those tools (that can build trust) something that could be built-in & available to all users of the language, therefore avoiding "reinventing the wheel"? Why would you want to do by hand something that can be automated?

Re: Summer of Programming Languages

#72

Post by the_af » Mon, Jul 07, 2014, 9:45 PM UTC

tormeh wrote: post #65

steveklabnik wrote: post #48

Earlier quoted context omitted.

> it's also much simpler and faster for the programmer to write one function with one return type, and later modify it to add a return type if the requirements change. How is this different? When you compile, your compiler will say "Hey, the requirements have changed, your code is wrong here, here, here, and here," and you modify those things, and you're done.

....and then you've forgot what you were actually trying to solve.

What is the alternative? You change the code, the behavior gets changed but the compiler doesn't warn you. At this point you have two possible paths:

1- You wrote tests which start failing. You must now spend time changing them. You don't manage to avoid working in order fix your safety net (be it static type checking or your test suite).

2- You didn't write the right tests, and don't notice the change in behavior. The program later fails in production.

Re: Summer of Programming Languages

#73

Post by lmm » Mon, Jul 07, 2014, 10:15 PM UTC

tormeh wrote: post #65

steveklabnik wrote: post #48

Earlier quoted context omitted.

> it's also much simpler and faster for the programmer to write one function with one return type, and later modify it to add a return type if the requirements change. How is this different? When you compile, your compiler will say "Hey, the requirements have changed, your code is wrong here, here, here, and here," and you modify those things, and you're done.

....and then you've forgot what you were actually trying to solve.

I find the type system a great help with remembering what I was actually trying to solve. I can "start at the end" and then work backwards, solving one compile error at a time until there aren't any left, at which point I'll know I've done what I wanted to.

Re: Summer of Programming Languages

#74

Post by frowaway001 » Tue, Jul 08, 2014, 9:12 AM UTC

seanmcdirmid wrote: post #44

freyrs3 wrote: post #41

Earlier quoted context omitted.

It's a technical term so the colloquial definition has little relevance to it's use in computing. You can read the definition in TAPL or PFPL. > tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.

Type is pretty much used by most programmers to mean "type" as it is stated in the dictionary; so dynamic type checking is not a misnomer to them. Only type theorists are diligent about the colloquial definition, but they can only really use it like that when talking to other type theorists.

Well, if the other person doesn't at least understand that much, speaking to them is probably a waste of time anyway.

Re: Summer of Programming Languages

#75

Post by seanmcdirmid » Tue, Jul 08, 2014, 10:21 AM UTC

frowaway001 wrote: post #74

seanmcdirmid wrote: post #44

Earlier quoted context omitted.

Type is pretty much used by most programmers to mean "type" as it is stated in the dictionary; so dynamic type checking is not a misnomer to them. Only type theorists are diligent about the colloquial definition, but they can only really use it like that when talking to other type theorists.

Well, if the other person doesn't at least understand that much, speaking to them is probably a waste of time anyway.

Yes, perhaps type theorists are best talking to other type theorists and not people who actually program.

Re: Summer of Programming Languages

#76

Post by innguest » Tue, Jul 08, 2014, 1:21 PM UTC

namanbharadwaj wrote: post #6

zak_mc_kracken wrote: post #4

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

A language shouldn't need to have a foundation in category theory in order to be "grounded in theory and informed by practice." I think that Bob's (the OP's) is merely saying that the design of languages such as Rust and Swift has been strongly influenced by developers well-versed in type theory (the foundation of programming languages) as well as software development (the point of programming languages) -- this is t…

I'd find it hard to justify nowadays understanding that there's a lot useful in Type theory but then ignoring Category theory. Even Object Orientation can be related to CT as coalgebras.

The type system in Haskell is not complex and that's a reason to like it. Everything derives from 6 simple rules:

http://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sys...

Simplicity in a type system makes it very expressive - contrast with complex, concrete type systems which do not allow e.g. Church numerals or linked lists to be represented within it.

Re: Summer of Programming Languages

#77

Post by kluge » Tue, Jul 08, 2014, 2:40 PM UTC

andolanra wrote: post #58

tibbe wrote: post #38

Earlier quoted context omitted.

There are cases you cannot really exclude by testing. For example, guaranteeing that certain function never receives a null value.

It is true that some things you just need to test, but nullability isn't actually one of them. Many languages—including SML, Haskell, Rust, and Swift—encode nullability in the type system, so those languages can guarantee at compile-time that functions never receive null values.

You read the comment backwards. It was saying exactly that nullability of the argument is something that can be guaranteed by a type system but you can't write a test that makes sure of it.

Re: Summer of Programming Languages

#78

Post by frowaway001 » Fri, Jul 11, 2014, 2:43 PM UTC

seanmcdirmid wrote: post #75

frowaway001 wrote: post #74

Earlier quoted context omitted.

Well, if the other person doesn't at least understand that much, speaking to them is probably a waste of time anyway.

Yes, perhaps type theorists are best talking to other type theorists and not people who actually program.

Agree.