3 ms·
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 t
by 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.
- tel 11y agoI don't see any meaningful distinction between human reasoning and logic, tbqh. As I stated earlier, your stacks of scoped continuations are exactly equivalent to monads but, depending on how you restrict them, a little less flexible. I don't mean this to say something trivial—I mean it to say that every composition problem solved in each place is identically solved in the other. I'm confident that your 99% claim holds historically to various degrees, but not completely. Plenty of mathematical algorithms were (a) constructive and (b) first formulated declaratively. We have spent the last 30-50 years describing many more algorithms at a much more furious pace at a time where publicity depended deeply upon using an imperative language... so historical explanations have that going for them.
- pron 11y ago> As I stated earlier, your stacks of scoped continuations are exactly equivalent to monads but, depending on how you restrict them, a little less flexible. But they compose better, not requiring monad transformers while still being type-safe. For the continuation to decide on which scope to pause on is like a monadic function returning a monadic value of a monad not directly enclosing it, but one or more levels up.
- pron 11y ago> Types should be studied even if it is conclusively proven that humans cannot stand their UX. I'd like to add that while I agree 100% with this, from the perspective of the industry, abstractions exist to increase code reuse, assist in code maintenance, and help verification: in short they exist to reduce the cost of development, and -- from a non-research perspective -- that is the only metric by which they are judged. Of course, that is not to say that types shouldn't be studied for pure research, or even that that research might not lead down the line for significant cost reductions.
- tel 11y agoI agree, but am pretty excited by the opportunity that such research will have outsize long-term benefits.