Hacker News Reader

Comment by zak_mc_kracken | Hacker News Reader

> 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 theory or the ambitious kind of type system that Haskell has been pioneering for a while. And the fact that Go is seeing some traction is a stark reminder that we still have ways to go.

Still, it's nice to see some of these concepts becoming mainstream (lambdas/closures, fold and functional iteration, phasing off inheritance based polymorphism, etc...).

View on HN

These languages do have very theoretical foundations even though they might not be readily apparent. ML has a rich theory much of which is applicable to both Rust and Swift's type systems.

This is even more applicable to Rust where the system that deals with lifetimes and ownership are based on ideas that evolved out of linear/affine type systems that can track resource consumption.

Funnily enough linear type systems have a direct connection to linear logic, and via the Curry-Howard-Lambek there is another correspondence to symmetric/closed monoidial categories. Even though sometimes it appears like there is no theory behind these languages, Rust has definitely been aggressively importing some cutting edge thinking from programming languages.

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 true for Haskell as well, as he points out, but he is just noting that these well-designed, informed languages are becoming more mainstream.

Also, Rust's type system is more complex than you might expect, involving something called linear/affine types: http://en.wikipedia.org/wiki/Substructural_type_system#Linea...

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.

I recall reading that when Niko joined the Rust project, he kept uncovering places where the type system was unsound and was instrumental in making Rust type-safe. Can anyone confirm?

Well, we basically knew where the problems were, but Niko helped us come up with a way to fix them that was usable (the borrow check).

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.

> 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 out; it would be like working in a language without generics. So I couldn't stand to work in a language that can't express these concepts; I need either higher-kinded types or something equivalent to them.

And for a type system that powerful, I'd want some assurance it was correct. Theoretical underpinnings are not the only way to do that - if it had been in use a while, and had enough tests and experience to give me a decent level of confidence, that would be enough. But for a new language I think the only way I could be confident enough to use it would be if it had this kind of theoretical backing.

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

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

Yes, many of us do. Using Option/Result can often lead to a lot of pain without their accompanying monads, and while you can write the specific ones (there's a try macro for using Option), it'd be much, much nicer to just have monads be possible in the language itself.

However, the Rust team is trying to get 1.0 out the door, and higher-kinded types would be backwards compatible, so I don't think we'll be seeing them for a while. There's also questions about the overhead and syntax that would need to be resolved for them to make it in.

The backwards compatibility argument is interesting. I think it's really compelling, but it's also worth taking into account the pains that the Haskell community has been feeling since standardizing the standard library as insufficiently generic.

I have no idea if a similar problem is possible with Rust, but it'll be interesting to see how HKTs enter the scene if and when they do.

The Rust standard library will exist as an separate entity from the language itself, and can be versioned, updated, and deprecated just as any other library can, without being tied to any specific version of the language.

Bro, do you even liftM? ;)

Reply on news.ycombinator.com