The limits of type theory: computation vs. interaction

The article isn't loading for me right now, but I thought I'd mention co-inductive types and how they relate to "interaction".

In Coq, co-inductive types are used to model infinite objects like (never-ending) streams or (non-terminating) program executions.

  Inductive List (A: Set): Set :=
  | Nil: List A
  | Cons : A -> List A -> List A.

  CoInductive Stream (A: Set): Set :=
  | SCons: A -> Stream A -> Stream A.

  Fixpoint len {A: Set} (x: List A): nat :=
    match x with
     | Nil => 0
     | Cons _ y => 1 + len y
    end.

  CoFixpoint ones : Stream nat :=
    SCons nat 1 ones.

If you want to talk about how systems interact with the world, you can use bisimilarity relations to prove "these two systems interact with the world in the same way".

You can also use co-inductive types to embed the temporal logic of actions (TLA) in Coq; TLA is the language Leslie Lamport works with for "Specifying Systems".

* http://www.labri.fr/perso/casteran/RecTutorial.pdf

* http://www.amazon.com/Specifying-Systems-Language-Hardware-E...

* http://en.wikipedia.org/wiki/Bisimulation

> Why then do you think at a certain point they start hurting

Oh, it's just a guess, but partly because of Haskell and its success at being continuously rejected by the industry for two decades now (it was touted as the next big thing when I was at university over 15 years ago). There have been few if any languages of Haskell fame that have clearly tried to break out of academia and have had so little use in the industry.

And the problem is less with types themselves but with the referential-transparency-everywhere and non-strict-evaluation approach. The result is that Haskell allows -- nay, demands -- a lot of reasoning about the program upfront at the expense of reasoning about it as it runs, with a debugger and a profiler (because of the complicated execution model). I also think Haskell places an unreasonable burden of thinking about the types vs. the algorithm an domain.

As to Scala, because it's such a "multi-paradigm" language, it's pretty hard to know exactly how it's used in the industry. There are certainly those that use it anywhere between Haskell-like with scalaz to Java-like only without having to write constructors and getters (in fact, Spark is written, I believe, closer in the latter style). But even if Scala is to be counted as an advocate for rich typing, its success record is pretty spotty (and, again, I wouldn't blame that necessarily on the type system).

I could, of course, be very wrong. One thing is certain: what a type system can do is a comp-sci question; how useful it is is a psychological question, and trying to argue about the usefulness of type systems (or any programming approach) as if it were a mathematical problem is just silly.

> We've certainly never reached that "certain point" where they start hurting.

I think Haskell is beyond that point, although I still believe a language with a type system as sophisticated as Haskell's might not be (because getting more for the same price might be worth it). By that I mean that Haskell types -- just like the article said -- waste a lot of mental power in the wrong places (i.e. on proving trivial stuff). I don't know what that imagined language would look like, but it would probably have some effect types (and like the author of the article has noted, there's a huge difference between being able to simulate effect systems and effect systems controlling actual effects).

Not all type systems allow for subtyping. In particular, Hindley-Milner does not. Nor, as far as I'm aware, do any of the consistently-typed proof languages (like Agda, Coq, etc.)

People keep getting it wrong because monads are the wrong abstraction. The right abstraction is algebraic effects. They correspond much more directly to "interactions", because the types of effect handlers are exactly the types of allowed "interactions". As a bonus, algebraic effects commute with each other, while monads usually don't. (For example, there's a gratuitous difference between Maybe (List a) and List (Maybe a), and people who want to program with effects shouldn't have to think about such differences.)

There was a great quote saying that when you get something almost right but not completely right, you have to explain it to people over and over again. IMO people should pay more attention to that quote, it applies to monads perfectly.

> For example, there's a gratuitous difference between Maybe (List a) and List (Maybe a)

In what sense is the difference "gratuitous"? Seems to me its a pretty significant, meaningful difference and that the two types represent radically different things.