61–70 of 70 posts
Earlier quoted context omitted.
How can you compare that code with the Python one liner in the original article? It's interesting, of course, but it's not "easy to work with".
He explicitly gives standard machinery like the a boolean type and natural numbers, presumably to show more clearly what the parts are built up from. You probably wouldn't need to write all of that to use HList at a later point.
> Each monad indicates one particular kind of interaction, such as using memory or perform input-output. NO NO NO. Stop. It was cute when people got this wrong in 2010; now it's just ignorant to pretend to know enough about Haskell to tell us something about it and still get this so wrong. There is no inherent connection between monads and statefulness; none whatsoever. Monads just happened to be a useful abstraction…
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…
Earlier quoted context omitted.
> But I also think they may help up to a certain point and then start hurting. The problem is, this has never been put to the test. You're right that the current cutting-edge of types in programming haven't been put to the test yet. Scala and OCaml and Haskell all get varying degrees of industry use, but it's nothing compared to C++, Java, Python, etc. So it's clear that we haven't even almost gotten to the point whe…
> 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 indu…
When you are encoding your logic in types the distinction between types and "the algorithm and domain" is very blurred if not the exact same thing. I wouldn't want to be programming in any other language if I knew very little about the domain.
Earlier quoted context omitted.
> 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 indu…
> I also think Haskell places an unreasonable burden of thinking about the types vs. the algorithm an domain. When you are encoding your logic in types the distinction between types and "the algorithm and domain" is very blurred if not the exact same thing. I wouldn't want to be programming in any other language if I knew very little about the domain.
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…
Do you know of any introduction to algebraic effects that is more programming-focused than theoretical?
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!
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…
There is no such thing as an "approximate table" per se, just things that can be approximately described by the word "table". It makes no sense to talk about a 'real table'. Every thing that exists is real, whether you call it a table or not.
I'm also confused why you'd think the concept of continuity is blurry on this issue. Continuity means that similar inputs give nearby outputs, and this is perfectly consistent with how computation works: if you construct two results through similar algorithms, they will have closely related types. Types become a measure of similarity of different computations, and thus you can use them to group things with similar linguistic structure, and thus similar meaning.
Either way, Aristotle and Plato were both ancient people with not even a tenth the information we have today, so I wouldn't consider them authorities on any part of this discussion.
I'd disagree with the two statements: > People who think they understand something about the theory of programming languages, including me, tend to agree that what Python does is wrong. > In fact you can program heterogeneous lists in dependently typed languages, but it’s unreasonably complicated. Here's some Agda code that shows that both heterogeneous if statements and lists make sense and are easy to work with in…
How can you compare that code with the Python one liner in the original article? It's interesting, of course, but it's not "easy to work with".
Earlier quoted context omitted.
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.
Earlier quoted context omitted.
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`…