5 ms·

> Nowadays serious industrial-strength languages are emerging that are grounded in theory and informed by practice. This seems a bit overly optimistic, but it'

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

gnuvince 12y ago
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?
- pcwalton 12y ago
  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).
namanbharadwaj 12y ago
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#Linear_type_systems http://en.wikipedia.org/wiki/Substructural_type_system#Linea...
- innguest 12y ago
  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_system 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.
jonnybgood 12y ago
> 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?
- lmm 12y ago
  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.
  - Dewie 12y ago
    > I need either higher-kinded types or something equivalent to them. FWIW it seems that many of the Rust developers want this for Rust.
    - steveklabnik 12y ago
      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.
jroesch 12y ago
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.
pjmlp 12y ago
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.

gnuvince 12y ago

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?

pcwalton 12y ago
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).

namanbharadwaj 12y ago

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#Linear_type_systems http://en.wikipedia.org/wiki/Substructural_type_system#Linea...

innguest 12y ago
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_system 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.

jonnybgood 12y ago

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

lmm 12y ago
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.
- Dewie 12y ago
  > I need either higher-kinded types or something equivalent to them. FWIW it seems that many of the Rust developers want this for Rust.
  - steveklabnik 12y ago
    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.

jroesch 12y ago

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.

pjmlp 12y ago

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.