5 ms·

It's late, so while I'd like to bite more, I'll just take this one on: > other than that our mathematical exploration is guided by our human minds I think tha

by tel 11y ago

It's late, so while I'd like to bite more, I'll just take this one on: > other than that our mathematical exploration is guided by our human minds I think that's exactly it. I'm not honestly a good enough philosopher to be clear on how I feel about the origins of mathematics. So, blurrily, I'll just state immediately that I think they are an embodied thing (I am no Platonic dualist). In that sense they are not constrained by our language but instead our language is continually growing to be so strong as to admit the vagaries of our thoughts. And this is why I like PFP: because it endeavors to capture a wider world than just algorithms—although it is one which places algorithm at its core by accepting the need to build and witness over placing trust in the completeness of the universe. This justification is wildly impractical, of course. I can't even from this perspective recognize the smell of practical—so the closest I can come is to say that I think Church's Thesis, if it is even true, taught us something really interesting: that it's quite easy to represent all functions (nat -> nat). Since this encompasses nearly everything we can "practically" witness we're playing in a giant, easy sandbox (this is not me saying that programming is easy, of course!). So there ends up being a lot of degrees of freedom on how we accomplish our giant, easy tasks. If you want to eliminate them then you must take aim at harder tasks---and that is exactly what PFP does do. Or at least what the research apparatus attached to PFP does. So out here is a wild ride to the core of human expression. That's one that I want to ride.

pron 11y ago
> and that is exactly what PFP does do True, but 1/ with so far very little to show for it (it is easy to make easy programs easy; no one has seen PFP make hard programs easier) and 2/ I am far from convinced (although I haven't explored other avenues myself, as PL is not my field) that there aren't other approaches which do the same and are more compatible with how we think. I think that other than the happy "coincidence" that is Curry-Howard, I see nothing in LC to suggest that it is the "right" way to model computation, and CH itself is just a form of verification (that requires programmers to prove their programs). Maybe it's the right way to do verification and maybe it isn't. Suppose Hoare logic approaches proved to be easy. Would people still see LC as promising? I think it's seen as promising just because verification is easier -- not because there is evidence to suggest it's the right way to express unverified algorithms -- but nobody has quantified the cost/benefit of various verification techniques (both formal and informal). Other than the mathematical results which are to be expected to be found under this powerful lamppost, I see little evidence to suggest PFP is even on the right track. PFP has had one obvious achievement, though: thanks to PFP, there's a lot of research into type systems, some may prove to be very useful even in imperative languages (like Rust, although that language is also far from being proven, either, but I have a feeling we'll learn of its effectiveness -- or lack thereof -- much sooner than we will of Haskell's :)) But I find that achievement rather disappointing compared to those of the algorithmic CS disciplines (distributed databases, machine learning, JITs). I do recognize that PL has a much harder time proving the worth of its results. A machine learning algorithm could be implemented in any language. Producing and then getting people to adopt a new language, in contrast, is extremely expensive, as it requires not only implementing the new work, but porting man-decades of work. But sympathy aside, as someone in the industry, I view PL research as that CS discipline that's supposed to concentrate most on the human side, yet contributed least to to our industry's achievements (while making more noise than most other CS disciplines). And this is where I'd like to circle back to the original post and the discussion of whether PFP people are arrogant or not. I don't know too many PFP people with major achievements in the industry, but I don't suppose they are any more or less arrogant than others. I do, however, find it annoying (and ridiculous) to be accused by some PLers of having an anti-intellectual stance or refusal to try new things simply because I'm very skeptical of new languages. I and others like me are very quick to adopt new algorithms, but new languages are not only extremely costly to adopt -- they have so far delivered precious little more than big promises (but oh, do they love making those promises!). So if I were to describe PL researchers and PFPers in particular, I'd say they overpromise and under-deliver more than the rest of academic CS, and have certainly had the least impact on the industry. I can suggest (with little knowledge of actual facts) that the reason for that is that PL, as a UX discipline, should be most accommodating to human psychology, but in practice it is often as uncompromising as any other pure-theoretical field.
- tel 11y ago
  I'm interested as well in alternative ways to do this kind of thing which are more "psych friendly" though I don't have any warm leads at the moment. I don't think of CH as being a way of doing verification, as you mention it's not even a very good way of doing that necessarily, but instead a note that human reasoning can be accurately transcribed in types. The formal verification angle on this is just window dressing. Also LC is not even seen as the "right" way. It's obviously too simple. But it is at the core of other more "right" ways because it as a notion is very composable. PFP is an important part of this research because it's got the most complete type theories. Impure arrows can be modeled too, but they're harder. Nice impure models share more similarity with PFP than with standard imperative programming, too. I suppose in my mind PFP has had tons of victories... but they're just not in the domain that you're looking in. That's fine, I believe some will exist there someday. I'm not actually much of one to proselytize for PFP in industry ;) And on arrogance I am completely with you. When people get a little power it goes to their head and if you make a transition from "practical" imperative programming to "mathy" FP you feel like you just leveled up a lot. Then you ignore that "mathy" imperative programming (and "mathy" OO for that matter) exist and are healthy and probably have a lot to share, too. That's sad. Finally, I agree with the idea that at least somewhere in PL there ought to be a UX discipline (see my writing elsewhere around types as UX for more on this) but I am also pretty convinced that this is not the entirety of PL research. Types should be studied even if it is conclusively proven that humans cannot stand their UX. Why? Because they are as powerful a language for expressing formal thought as humans have yet invented. We'll figure out the UX someday, but if we step away from the seat of utility then we'll have lost something vital.
  - pron 11y ago
    > but instead a note that human reasoning can be accurately transcribed in types Is that human reasoning or logic? :) > But it is at the core of other more "right" ways because it as a notion is very composable. It is and it isn't. Where it counts, it's got some composability problems, like with composing monads. Moand transformers are way too high-order for me to follow (or care to learn to follow) -- remember, NASA said first-level and second-level pointer indirection are fine, but not third-level; I think this applies to high-order functions, too. OTOH, "scoped" continuations[1] compose perfectly, while still being statically typed and explicit about which "monad" they're in[2]. > Nice impure models share more similarity with PFP than with standard imperative programming, too. I totally believe that, but from the programmer's perspective, that is completely irrelevant. That's something we want to stay hidden, left to those doing PL research. Give us the results -- we really hope we don't need to learn how you got there :) > Then you ignore that "mathy" imperative programming (and "mathy" OO for that matter) exist and are healthy and probably have a lot to share, too. Considering that 99% of algorithms are expressed imperatively and invented by imperative programmers, I'd say that's likely true. People doing DB, numerical/scientific computation, machine learning, distributed computing and concurrency research work mostly in C, Java and Matlab -- not Haskell or Idris. > Types should be studied even if it is conclusively proven that humans cannot stand their UX. Why? Because they are as powerful a language for expressing formal thought as humans have yet invented. We'll figure out the UX someday, but if we step away from the seat of utility then we'll have lost something vital. I totally agree! [1]: Scoped continuations are nested continuations that allow functions to pause at each level of the scope (think how nested try-catch blocks work with different exception types) -- I'll post my talk when it's available online. [2]: Think Java's checked exceptions.

by tel 11y ago

pron 11y ago

> and that is exactly what PFP does do True, but 1/ with so far very little to show for it (it is easy to make easy programs easy; no one has seen PFP make hard programs easier) and 2/ I am far from convinced (although I haven't explored other avenues myself, as PL is not my field) that there aren't other approaches which do the same and are more compatible with how we think. I think that other than the happy "coincidence" that is Curry-Howard, I see nothing in LC to suggest that it is the "right" way to model computation, and CH itself is just a form of verification (that requires programmers to prove their programs). Maybe it's the right way to do verification and maybe it isn't. Suppose Hoare logic approaches proved to be easy. Would people still see LC as promising? I think it's seen as promising just because verification is easier -- not because there is evidence to suggest it's the right way to express unverified algorithms -- but nobody has quantified the cost/benefit of various verification techniques (both formal and informal). Other than the mathematical results which are to be expected to be found under this powerful lamppost, I see little evidence to suggest PFP is even on the right track. PFP has had one obvious achievement, though: thanks to PFP, there's a lot of research into type systems, some may prove to be very useful even in imperative languages (like Rust, although that language is also far from being proven, either, but I have a feeling we'll learn of its effectiveness -- or lack thereof -- much sooner than we will of Haskell's :)) But I find that achievement rather disappointing compared to those of the algorithmic CS disciplines (distributed databases, machine learning, JITs). I do recognize that PL has a much harder time proving the worth of its results. A machine learning algorithm could be implemented in any language. Producing and then getting people to adopt a new language, in contrast, is extremely expensive, as it requires not only implementing the new work, but porting man-decades of work. But sympathy aside, as someone in the industry, I view PL research as that CS discipline that's supposed to concentrate most on the human side, yet contributed least to to our industry's achievements (while making more noise than most other CS disciplines). And this is where I'd like to circle back to the original post and the discussion of whether PFP people are arrogant or not. I don't know too many PFP people with major achievements in the industry, but I don't suppose they are any more or less arrogant than others. I do, however, find it annoying (and ridiculous) to be accused by some PLers of having an anti-intellectual stance or refusal to try new things simply because I'm very skeptical of new languages. I and others like me are very quick to adopt new algorithms, but new languages are not only extremely costly to adopt -- they have so far delivered precious little more than big promises (but oh, do they love making those promises!). So if I were to describe PL researchers and PFPers in particular, I'd say they overpromise and under-deliver more than the rest of academic CS, and have certainly had the least impact on the industry. I can suggest (with little knowledge of actual facts) that the reason for that is that PL, as a UX discipline, should be most accommodating to human psychology, but in practice it is often as uncompromising as any other pure-theoretical field.

tel 11y ago
I'm interested as well in alternative ways to do this kind of thing which are more "psych friendly" though I don't have any warm leads at the moment. I don't think of CH as being a way of doing verification, as you mention it's not even a very good way of doing that necessarily, but instead a note that human reasoning can be accurately transcribed in types. The formal verification angle on this is just window dressing. Also LC is not even seen as the "right" way. It's obviously too simple. But it is at the core of other more "right" ways because it as a notion is very composable. PFP is an important part of this research because it's got the most complete type theories. Impure arrows can be modeled too, but they're harder. Nice impure models share more similarity with PFP than with standard imperative programming, too. I suppose in my mind PFP has had tons of victories... but they're just not in the domain that you're looking in. That's fine, I believe some will exist there someday. I'm not actually much of one to proselytize for PFP in industry ;) And on arrogance I am completely with you. When people get a little power it goes to their head and if you make a transition from "practical" imperative programming to "mathy" FP you feel like you just leveled up a lot. Then you ignore that "mathy" imperative programming (and "mathy" OO for that matter) exist and are healthy and probably have a lot to share, too. That's sad. Finally, I agree with the idea that at least somewhere in PL there ought to be a UX discipline (see my writing elsewhere around types as UX for more on this) but I am also pretty convinced that this is not the entirety of PL research. Types should be studied even if it is conclusively proven that humans cannot stand their UX. Why? Because they are as powerful a language for expressing formal thought as humans have yet invented. We'll figure out the UX someday, but if we step away from the seat of utility then we'll have lost something vital.
- pron 11y ago
  > but instead a note that human reasoning can be accurately transcribed in types Is that human reasoning or logic? :) > But it is at the core of other more "right" ways because it as a notion is very composable. It is and it isn't. Where it counts, it's got some composability problems, like with composing monads. Moand transformers are way too high-order for me to follow (or care to learn to follow) -- remember, NASA said first-level and second-level pointer indirection are fine, but not third-level; I think this applies to high-order functions, too. OTOH, "scoped" continuations[1] compose perfectly, while still being statically typed and explicit about which "monad" they're in[2]. > Nice impure models share more similarity with PFP than with standard imperative programming, too. I totally believe that, but from the programmer's perspective, that is completely irrelevant. That's something we want to stay hidden, left to those doing PL research. Give us the results -- we really hope we don't need to learn how you got there :) > Then you ignore that "mathy" imperative programming (and "mathy" OO for that matter) exist and are healthy and probably have a lot to share, too. Considering that 99% of algorithms are expressed imperatively and invented by imperative programmers, I'd say that's likely true. People doing DB, numerical/scientific computation, machine learning, distributed computing and concurrency research work mostly in C, Java and Matlab -- not Haskell or Idris. > Types should be studied even if it is conclusively proven that humans cannot stand their UX. Why? Because they are as powerful a language for expressing formal thought as humans have yet invented. We'll figure out the UX someday, but if we step away from the seat of utility then we'll have lost something vital. I totally agree! [1]: Scoped continuations are nested continuations that allow functions to pause at each level of the scope (think how nested try-catch blocks work with different exception types) -- I'll post my talk when it's available online. [2]: Think Java's checked exceptions.