10 ms·

Summer of Programming Languages

101 points by platz 12y ago

flebron 12y ago
For anyone who's interested in type theory and programming language foundations and modern development, I've found the talks of these summer schools really interesting and useful. The videos and material are at https://www.cs.uoregon.edu/research/summerschool/summer14/curriculum.html https://www.cs.uoregon.edu/research/summerschool/summer14/cu... , and you can change "14" in the URL to earlier years to see previous material. It's really a highly valuable set of resources.
deleted 12y ago
[deleted]
zak_mc_kracken 12y ago
> 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.
aidenn0 12y ago
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.
- lmm 12y ago
  Academics don't care so much about things like programming speed. And the academic environment focusses on proof; a type-safety property will seem much better than a unit test even when both took the same amount of time and have the same practical value. (For all that, I agree with them though. Maybe the reason programming languages researchers think that is because it's true? Do you have reason to believe they're wrong?)
  - coldtea 12y ago
    >Academics don't care so much about things like programming speed. I don't know. Haskell and OccamL, for one, are much, much faster than Python and Ruby.
    - lmm 12y ago
      Citation needed. The argument for Haskell is usually about correctness; industry perception and my experience is that writing a Haskell version of a program will usually take longer than an "acceptably buggy" Python or Ruby equivalent.
      - deleted 12y ago
        [deleted]
        lmm 12y ago
        All of that's about runtime performance, not programming time.
      - the_af 12y ago
        Well, there's the 1994 US Navy experiment that shows Haskell is a serious contender for rapid prototyping: http://cpsc.yale.edu/sites/default/files/files/tr1049.pdf http://cpsc.yale.edu/sites/default/files/files/tr1049.pdf Of course, there was no Ruby back then. The comparison was against C++, Ada, Awk (!?), something called "relational Lisp" and a variety of in-house languages. Haskell comes just after Lisp in development time, with a mind-boggling 8 hours! (No C++ times were reported... heh heh). The Haskell solution also got top marks in general, not just in development time. As a downside, some of the reviewers didn't understand it because they weren't well-versed in functional programming, and felt some of the Haskell code was "tricky".
noobSemanticist 12y ago
Any ideas why software verification videos are not published in the OPLSS web page?

101 points by platz 12y ago

For anyone who's interested in type theory and programming language foundations and modern development, I've found the talks of these summer schools really interesting and useful. The videos and material are at https://www.cs.uoregon.edu/research/summerschool/summer14/curriculum.html https://www.cs.uoregon.edu/research/summerschool/summer14/cu... , and you can change "14" in the URL to earlier years to see previous material. It's really a highly valuable set of resources.

deleted 12y ago

[deleted]

zak_mc_kracken 12y ago

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

aidenn0 12y ago

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.

lmm 12y ago
Academics don't care so much about things like programming speed. And the academic environment focusses on proof; a type-safety property will seem much better than a unit test even when both took the same amount of time and have the same practical value. (For all that, I agree with them though. Maybe the reason programming languages researchers think that is because it's true? Do you have reason to believe they're wrong?)
- coldtea 12y ago
  >Academics don't care so much about things like programming speed. I don't know. Haskell and OccamL, for one, are much, much faster than Python and Ruby.
  - lmm 12y ago
    Citation needed. The argument for Haskell is usually about correctness; industry perception and my experience is that writing a Haskell version of a program will usually take longer than an "acceptably buggy" Python or Ruby equivalent.
    - deleted 12y ago
      [deleted]
      - lmm 12y ago
        All of that's about runtime performance, not programming time.
    - the_af 12y ago
      Well, there's the 1994 US Navy experiment that shows Haskell is a serious contender for rapid prototyping: http://cpsc.yale.edu/sites/default/files/files/tr1049.pdf http://cpsc.yale.edu/sites/default/files/files/tr1049.pdf Of course, there was no Ruby back then. The comparison was against C++, Ada, Awk (!?), something called "relational Lisp" and a variety of in-house languages. Haskell comes just after Lisp in development time, with a mind-boggling 8 hours! (No C++ times were reported... heh heh). The Haskell solution also got top marks in general, not just in development time. As a downside, some of the reviewers didn't understand it because they weren't well-versed in functional programming, and felt some of the Haskell code was "tricky".

noobSemanticist 12y ago

Any ideas why software verification videos are not published in the OPLSS web page?