Hacker News Reader

Comment by tomp | Hacker News Reader

It's not about functional programming languages per se, it's just that a lot of core/academic PL research often focuses much more on concepts than on implementation, and languages with strong type systems (all of which are functional, in part also because OO/subtyping is hard to reason about formally) are ideal for encoding these concepts.

There is, however, a lot of research about implementation going on using other languages as well. Most GC research, for example, is done using JVM and Java programs. For this particular paper, it would be really hard to choose a different platform, though, because GHC is one of the rare industrial runtimes that offer lightweight threads.

View on HN

> (all of which are functional, in part also because OO/subtyping is hard to reason about formally)

OO/subtyping is NOT orthogonal to functional, nor is it inherently at odds with formal reasoning. OCaml has both imperative and functional objects; Haskell, Mercury, and Coq (a formal logic language) all support typeclasses, which subsume most of OO and provide subtyping.

Additionally, strong typing has little to do with formal reasoning as well (see: Lisp/Scheme/the lambda calculus). What makes functional languages amenable to formal methods is that they are functional and therefore referentially transparent. Mathematical proofs carry no implicit concept of "state"; hence if you are trying to prove anything about code in, say, C, you need to augment the code with explicit state and remove all non-local effects. (See: the Why language, which attempts to bridge this gap.)

Algebraic/generalized-algebraic type constructors used by most functional languages don't hurt either, as they allow programs to construct complex terms without relying on lower-level stateful abstractions such as memory allocation.

hence if you are trying to prove anything about code in, say, C, you need to augment the code with explicit state and remove all non-local effects. (See: the Why language, which attempts to bridge this gap.)

Actually, you just need to augment your model with notions of state, which is standard in operational semantics. It can just be harder to prove things in a complex model, so theorists prefer simplification when possible.

Not inherently, no, but practically, yes. The type system of, say, Java, isn't even formally sound; overridden functions can be covariant in parameter types, which would not be permissible in a proper subtype-based type system such as OCaml's.

Ah yes, I forgot about Java's failings in this area.

> all of which are functional, in part also because OO/subtyping is hard to reason about formally

OO subtyping is hard to reason about formally in formal systems designed for FP...news at 11! I jest.

The reason FP does so well academically is that no one knows how to rigorously evaluate something that isn't theoretical (since FP is close to math anyways) or performance-based (most other PL work).

The Haskell crowd is also very creative so they do a lot of cool stuff. However, many of their ideas are transferrable to other languages without the FP ideology.

The OO people have something to offer also, but we've been kind of muted lately.

>> OO subtyping is hard to reason about formally in formal systems designed for FP...news at 11!

Well. Even systems like L2 (which are not functional) find subtyping difficult. It becomes difficult in the presence of overloading and overriding.

I believe there's a nice book called Foundations of Object Oriented Languages which dissects the problem in depth.

Pierce's TAPL, also, and Harper's Practical Foundations. There's also some things i've seen about how scala does it, but I'll have to dig for them

http://www.cs.cmu.edu/~rwh/plbook/book.pdf

See also the DOT calculus[1] (Dependent Object Types) being the basis for a new foundation for scala's type system

[1] - https://github.com/namin/dot

OO subtyping is hard to reason about formally in formal systems _in general_.

And yet, is-a and has-a relationships predominate natural language. Well, it makes sense: natural language is hard to reason about formally also.

The problem isn't that `is-a` is hard, it's the divergence of `is-subtype-of` and `is-subclass-of`. Take a look here, I think it explains it rather well. http://okmij.org/ftp/Computation/Subtyping/

I would argue that nominative subtyping is natural (basically sub-classing), since it matches our ability to assign arbitrary meaning and relationships to words, which is incredibly useful when having a conversation. Ya, maybe a set isn't exactly a bag, but close enough. Birds mostly fly, but penguins don't, we can deal with that.

But the main problem with subtyping, nominative or structural, is how it messes up Hindley-Damas-Milner style type inference. But that shouldn't be surprising that an FP theory for type inference wouldn't work well for OOP.

Exactly. And low-level concurrency research (snapshot algorithms, n-cas) is usually done in C or Java, and so on.

BTW, Java has lightweight threads, too: https://github.com/puniverse/quasar (I'm the main author)

Eh... what exactly is "lightweight" about your threads?

As far as I see you still use the same, standard JVM threads everyone uses, combined with a thread pool.

What am I missing?

The fact that it's not using standard JVM threads? His blog post describes how everything works: http://blog.paralleluniverse.co/post/49445260575/quasar-puls...

This blog post is extremely vague and handwavy.

Looking into the actual source code didn't reveal anything “special” either, so I'll just call bullshit on these claims.

Feel free to prove me wrong.

I don't know what you mean by "special" (nor do I understand which "claims" you have issue with), but these are true lightweight threads. We use runtime bytecode transformation to create continuation, so that we can suspend and later resume a call-stack. These continuations are then scheduled on a thread-pool. It works exactly like it does in any other lightweight thread implementation AFAIK, except that in languages such as Erlang or Haskell, these continuations are created by the compiler or by the runtime, while in Quasar they're created with bytecode transformation. The JVM doesn't support continuations out of the box, but its instrumentation mechanism allows you to implement them in a library. It isn't any more, or less, special than lightweight threads in Erlang or Haskell.

No, these are true lightweight threads (implemented on top of an OS-thread pool, just as they are in Erlang and, I suppose, Haskell). You can have hundreds of thousands or even millions of these on a single machine. They can block for IO or for any other kind of synchronization (message passing etc.), just like regular threads.

Are they preemptive?

Absolutely. Currently fibers (lightweight threads) may only be preempted when performing a blocking operation (IO or waiting on some synchronization mechanism). We will implement time-share based preemption if we see a need for that.

whenever i hear "lightweight threads" my PTSD from experience with Java "green threads" comes back. Of course, my rational mind understands that many years have passed and things may in other runtimes be implemented differently and there are many benefits vs. native, yet ...

This has little, if any, to do with that. These lightweight threads are implemented pretty much exactly as they're implemented in Erlang or Go.

Potentially stupid question: Would they not use Clojure or Scala rather than Java?

Doesn't matter really. For the GC research I mentioned, they usually just change one of the JVMs, so what they care about is only bytecode. Then, you need real programs to test on (improvements in throughtput, pause times, fragmentations, etc), which usually means Java programs but really doesn't matter.

Reply on news.ycombinator.com