Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The limits of type theory: computation vs. interaction

researchblogs.cs.bham.ac.uk

Post reply on HN
Print view View original

41–50 of 70 posts

Re: The limits of type theory: computation vs. interaction

#41

Post by cousin_it »

dragonwriter wrote: post #39
cousin_it wrote: post #37

Earlier quoted context omitted.

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 (May…

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

Yes, I agree. But that difference is irrelevant and distracting to people who just want to do effectful programming. A computation that's allowed to call handlers A and B should be always convertable to a computation that can call handlers B and A. There's no point in using a more general abstraction (monads) that doesn't give you the operations you need.

Re: The limits of type theory: computation vs. interaction

#42

Post by cousin_it »

danghica wrote: post #38
cousin_it wrote: post #37

Earlier quoted context omitted.

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 (May…

I agree with monads, not so sure about algebraic effects. Having to define the effect feels like "simulation" to me. It's OK for a meta-language, but to me it feels wrong for actual effectful programming.

Can you explain your wish in more detail? I feel like you might have a point, but I'm having trouble verbalizing it for myself :-(

Re: The limits of type theory: computation vs. interaction

#43

Post by muraiki »

"To me this is one methodological weakness of type theory, the commitment of having types for all terms in the language. Why is that? Types are designed to facilitate composition, but the natural unit for program composition is not the term but the function, or even the module. It makes sense to assign types to modules — it is methodologically consistent. But how we calculate these types could conceivably be more flexible, allowing a global perspective within the unit of composition. Types, as properties at the interface could be calculated using the entire arsenal of (decidable!) logics and static analyses."

I admit to not being that familiar with type theory (I've done a little Scala but most of my FP experience is in Clojure) but when I read this my gut reaction was: "Isn't that kind of what Go is doing?"

Meaning that in Go, the focus of compositionality isn't on basic types and the functions that act on them (see Go's lack of generics) but rather the focus is on getting different modules to agree on "what should be done to some stuff" using interfaces. This is putting interaction first but also getting compositionality in a "generic" way given that interfaces in Go are implemented implicitly.

Re: The limits of type theory: computation vs. interaction

#44

Post by sold »

pron wrote: post #22
jfoutz wrote: post #20

Earlier quoted context omitted.

Far and away the most obvious is null checking. It's not a big deal in a thousand line program, but as things grow, the need to always remember to check for null becomes a real problem. Related to null, you only get one null. the classic assoc problem. if i lookup a key in a hash, does the hash have the key, or is they value of the key null? Optional/Maybe is just wonderful for this case. Semantic meaning of common t…

You don't need a rich type system for null safety. Something like what Kotlin offers[1] is more than enough (in fact, I think it's better than what languages with far richer type systems offer). My point isn't that types are not helpful -- they are extremely helpful. My point it that on the continuum between no types and "types try to prove everything", there is a point that is the most useful, and that point is prob…

> in fact, I think it's better than what languages with far richer type systems offer

Can you explain why? I don't know Kotlin, but from this page it seems to divide types into nullable and non-nullable (correct me if I'm wrong). Is it possible to have a type "T??" that has three possibilities - "null", "wrapped null" and "T"? If not, this approach will not help in the assoc problem mentioned by the parent poster.

Re: The limits of type theory: computation vs. interaction

#45

Post by pron »

mafribe wrote: post #40

Maybe the author plans to write about it in later parts of the article, but it's misleading to assume that (1) there is no work on types for interacting processes and (2) that types always have to be based on some underlying ideas form functional programming. Much recent research in programming languages is about types for interacting processes. The most well-known, but by no means only example are the session types…

> it's misleading to assume that ... types always have to be based on some underlying ideas form functional programming.

One of FP's more annoying achievements is somehow convincing people that it's the only way to make programs more verifiable or more "mathematical". Imperative, stateful computation can be (and is) just as mathematical (whatever that means) and just as verifiable as pure-FP (it must be constrained in some ways, but not as extreme as requiring complete referential-transparency).

It's good to learn about applying types to process calculi. I wasn't aware of that work at all.

Re: The limits of type theory: computation vs. interaction

#46

Post by mafribe »

pron wrote: post #45
mafribe wrote: post #40

Maybe the author plans to write about it in later parts of the article, but it's misleading to assume that (1) there is no work on types for interacting processes and (2) that types always have to be based on some underlying ideas form functional programming. Much recent research in programming languages is about types for interacting processes. The most well-known, but by no means only example are the session types…

> it's misleading to assume that ... types always have to be based on some underlying ideas form functional programming. One of FP's more annoying achievements is somehow convincing people that it's the only way to make programs more verifiable or more "mathematical". Imperative, stateful computation can be (and is) just as mathematical (whatever that means) and just as verifiable as pure-FP (it must be constrained i…

   Imperative, stateful computation [...] is [...] as [...] verifiable as pure-FP
Exactly. When you verify your programs using some kind of program logic you realise that you have to keep track of all relevant data anyway.

The condescension towards languages like C/C++ and Java that some FP extremists have shown is probably one of the reasons for the rift between working programmers and PL theory. Fortunately, things are much better now, with most new languages (e.g. Scala, Rust, Clojure) bridging both worlds.

    applying types to process calculi. I wasn't aware of that work at all.
Maybe "A Gentle Introduction to Multiparty Asynchronous Session Types" http://goo.gl/FeVLv3 could be an introduction?

Re: The limits of type theory: computation vs. interaction

#47

Post by eli_gottlieb »

mafribe wrote: post #46
pron wrote: post #45

Earlier quoted context omitted.

> it's misleading to assume that ... types always have to be based on some underlying ideas form functional programming. One of FP's more annoying achievements is somehow convincing people that it's the only way to make programs more verifiable or more "mathematical". Imperative, stateful computation can be (and is) just as mathematical (whatever that means) and just as verifiable as pure-FP (it must be constrained i…

Imperative, stateful computation [...] is [...] as [...] verifiable as pure-FP Exactly. When you verify your programs using some kind of program logic you realise that you have to keep track of all relevant data anyway. The condescension towards languages like C/C++ and Java that some FP extremists have shown is probably one of the reasons for the rift between working programmers and PL theory. Fortunately, things ar…

>The condescension towards languages like C/C++ and Java that some FP extremists have shown is probably one of the reasons for the rift between working programmers and PL theory. Fortunately, things are much better now, with most new languages (e.g. Scala, Rust, Clojure) bridging both worlds.

Look, if you want to build a whole language around Hoare logic, go ahead. We just think it's ugly.

Re: The limits of type theory: computation vs. interaction

#48

Post by pron »

sold wrote: post #44
pron wrote: post #22

Earlier quoted context omitted.

You don't need a rich type system for null safety. Something like what Kotlin offers[1] is more than enough (in fact, I think it's better than what languages with far richer type systems offer). My point isn't that types are not helpful -- they are extremely helpful. My point it that on the continuum between no types and "types try to prove everything", there is a point that is the most useful, and that point is prob…

> in fact, I think it's better than what languages with far richer type systems offer Can you explain why? I don't know Kotlin, but from this page it seems to divide types into nullable and non-nullable (correct me if I'm wrong). Is it possible to have a type "T??" that has three possibilities - "null", "wrapped null" and "T"? If not, this approach will not help in the assoc problem mentioned by the parent poster.

The "assoc problem" is completely separate from null safety (it also demands a solution in a language without null).

Kotlin's handling of null safety is especially nice because of Kotlin's guarded casts. I.e. if you have a variable x of type A and B [2]: http://kotlinlang.org/docs/reference/java-interop.html

Re: The limits of type theory: computation vs. interaction

#49

Post by mafribe »

eli_gottlieb wrote: post #47
mafribe wrote: post #46

Earlier quoted context omitted.

Imperative, stateful computation [...] is [...] as [...] verifiable as pure-FP Exactly. When you verify your programs using some kind of program logic you realise that you have to keep track of all relevant data anyway. The condescension towards languages like C/C++ and Java that some FP extremists have shown is probably one of the reasons for the rift between working programmers and PL theory. Fortunately, things ar…

>The condescension towards languages like C/C++ and Java that some FP extremists have shown is probably one of the reasons for the rift between working programmers and PL theory. Fortunately, things are much better now, with most new languages (e.g. Scala, Rust, Clojure) bridging both worlds. Look, if you want to build a whole language around Hoare logic, go ahead. We just think it's ugly.

I'm not sure I can follow you here. What is ugly, Hoare logic? What does it mean to "build a whole language around Hoare logic"? What in your opinion are the alternatives to Hoare-style program logics that are general-purpose enough to work for arbitrary programming languages?

Re: The limits of type theory: computation vs. interaction

#50

Post by pron »

eli_gottlieb wrote: post #47
mafribe wrote: post #46

Earlier quoted context omitted.

Imperative, stateful computation [...] is [...] as [...] verifiable as pure-FP Exactly. When you verify your programs using some kind of program logic you realise that you have to keep track of all relevant data anyway. The condescension towards languages like C/C++ and Java that some FP extremists have shown is probably one of the reasons for the rift between working programmers and PL theory. Fortunately, things ar…

>The condescension towards languages like C/C++ and Java that some FP extremists have shown is probably one of the reasons for the rift between working programmers and PL theory. Fortunately, things are much better now, with most new languages (e.g. Scala, Rust, Clojure) bridging both worlds. Look, if you want to build a whole language around Hoare logic, go ahead. We just think it's ugly.

You don't need to build a "whole language" around any kind of logic for it to be sufficiently verifiable. Types are useful, but it's not necessarily an all-or-nothing question. There are non-type-based verification tools (symbolic execution and deduction), and tests complete the picture. A language that doesn't let you write a program unless you yourself have worked hard to prove to the compiler that it's correct may be more trouble than it's worth. Verification does not necessarily have to be a part of compilation, and it does not necessarily require the proof to be spelled out in code.
Post reply on HN