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

51–60 of 70 posts

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

#51

Post by mafribe »

pron wrote: post #50
eli_gottlieb wrote: post #47

Earlier quoted context omitted.

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

I agree that it is good separate programming and verification. Otherwise the programmer is forced by the compiler to worry about correctness and termination from Day 1.

Moreover, Cury-Howard based approaches really work only for a restricted form of programming: pure and total functions.

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

#52

Post by igravious »

paganel wrote: post #32
Retra wrote: post #24

Earlier quoted context omitted.

That 'table' problem is not that complicated once you understand the notions of 'approximation' and 'continuity'. A table with three legs is just a better approximation to what is meant by "table" than one with two, or worse than one with four. It basically leads to things like this: http://en.wikipedia.org/wiki/Domain_theory

And then I might respond (like many others did) that an "approximate" table is not a "real" table at all, i.e. we're back to step one of the problem. The way I like to look at it is that Aristotle's logic principles and all that followed (including the concept of "continuity") is a very nice and especially very usefull Domain Specific Language which helped us, humans, fly rockets to the moon and build iPhones (we wou…

If it's any consolation(?) I agree with you.

Plato's theory of Forms says: we can see around us many examples of horses. What makes them all horses? Why, the ideal form of a horse. Plato, I believe, then claims that these forms are perfect and timeless and the the actual world is inhabited by imperfect reproductions of these forms. Apologies to scholars of Plato.

Aristotle's Categories, while superficially, quite different I think is tackling the same problem. His most universal abstract categories try to answer the question, "what is it that all things regardless of their nature have in common?". And so his 10 (suspicious that, that 10) categories. His categories are very much rooted in language, as in they map readily onto parts of speech.

Both are ontological investigations. Both probe the essence of what it means to be something. And so on to the present day. Even though Russell was attempting to resolve a paradox in set theory what I think he actually did was answer the question, "what is a thing (any thing) in essence?" and I think the answer is, for our purposes, a term (instance) of a type (form).

It is not at all obvious how following these ancient investigations leads us to the door-step of type theory but all indications seem to point to it. You seem to have thought about this a good deal. I'd be interested in what you think. I've left out a _lot_ of detail but I hope what I've said is useful to somebody.

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

#53

Post by dllthomas »

paganel wrote: post #3

I'm in a no way a computer-science expert, just a mere programmer, but by the looks of it this discussion all boils down to the (quite big, I'd say) impedance mismatch between real life ("computer programs" in this article) and us, as humans, trying to understand said life and applying rules to it (by in this case applying "type theory"). For example, looking at this: >>> 0 if 1 else 'a' made me remember one of me ol…

"I'd ask how come the word's essence (its "transformation" from a String to an Integer) changes depending on the type of action we intend to apply on it?"

I think the problem is viewing "type" as "essence". Type is all about how we intend to use it, and which invariants we wish to enforce.

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

#54

Post by dllthomas »

cousin_it wrote: post #41
dragonwriter wrote: post #39

Earlier quoted context omitted.

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

This is handwavy and wrong.

Imagine we have two effects that need handling. One is "failure" - terminating the computation and propagating the fact of failure. The other is "emit", producing some value for an external process.

If I combine these two, the question arises as to the behavior of "emit 3; fail" - does it emit or bury the 3? Depending on the circumstance, either could be useful, and it's a tremendous difference that is neither irrelevant nor distracting.

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

#55

Post by Dewie3 »

muraiki wrote: post #43

"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 fle…

Yeah, Go has interfaces. Just like any sane, decently modern statically typed language. And it uses it to declare interfaces between things. A great concept, like the idea behind abstract data types -- defining data types by what operations can be performed on them.

But what is so special about Go's approach to interfaces? The only special thing I see is that interfaces are implemented implicitly, which I see more as a "implicit over explicit" decision rather than anything having to do with composition per se. Yet people keep raving about it.

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

#56

Post by muraiki »

Dewie3 wrote: post #55
muraiki wrote: post #43

"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 fle…

Yeah, Go has interfaces. Just like any sane, decently modern statically typed language. And it uses it to declare interfaces between things. A great concept, like the idea behind abstract data types -- defining data types by what operations can be performed on them. But what is so special about Go's approach to interfaces? The only special thing I see is that interfaces are implemented implicitly, which I see more as…

Well, I think that perhaps what makes Go different is not only interfaces, but interfaces as part of a larger package -- meaning the "not quite OO" approach it brings, in contrast to a language like Java's interfaces and general design philosophy.

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

#57

Post by YellPika »

eli_gottlieb wrote: post #28
userbinator wrote: post #16

Earlier quoted context omitted.

I also would argue that the design of CPUs such that any sequence of bits could be loaded in any in any register and interpreted depending of the current context, instead of having typed registers is not a shortcoming but a fundamental feature. It makes code small and elegant. Indeed, the fact that digital data is fundamentally "untyped" and its meaning depends entirely on interpretation is the entire reason why comp…

From a type-theoretic perspective, a language can be either logically consistent by means of strong normalization xor Turing-complete. The untyped lambda calculus is the smallest, most elegant functional language on the right half of that fork. It's also not strongly normalizing, so you can't prove theorems with it -- oh well!

> From a type-theoretic perspective, a language can be either logically consistent by means of strong normalization xor Turing-complete.

This is a common misconception. A counter-example: take System F, add an `IO` monad, and add a function `fix : forall a. (a -> a) -> IO a` for general recursion. Our language is now Turing-complete, but remains consistent since any falsehoods produced by `fix` can't escape the `IO` type, e.g. you can prove `fix id : IO _|_`, but not `_|_`.

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

#58

Post by [deleted] »

dllthomas wrote: post #54
cousin_it wrote: post #41

Earlier quoted context omitted.

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.

This is handwavy and wrong. Imagine we have two effects that need handling. One is "failure" - terminating the computation and propagating the fact of failure. The other is "emit", producing some value for an external process. If I combine these two, the question arises as to the behavior of "emit 3; fail" - does it emit or bury the 3? Depending on the circumstance, either could be useful, and it's a tremendous diffe…

[deleted]

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

#59

Post by cousin_it »

dllthomas wrote: post #54
cousin_it wrote: post #41

Earlier quoted context omitted.

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.

This is handwavy and wrong. Imagine we have two effects that need handling. One is "failure" - terminating the computation and propagating the fact of failure. The other is "emit", producing some value for an external process. If I combine these two, the question arises as to the behavior of "emit 3; fail" - does it emit or bury the 3? Depending on the circumstance, either could be useful, and it's a tremendous diffe…

If I understand algebraic effects correctly, the computation "emit 3; fail" might emit or bury the 3 (or do something even more strange) depending on which effect handlers you pass to it. Keeping effect handlers outside of computations is what allows for commutativity etc.

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

#60

Post by danghica »

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…

Indeed, I was going to talk about session types in a follow-on post :) Well anticipated! Cheers!
Post reply on HN