The halting problem forbids the existence of oracles which can decide with certainty in some finite time that an arbitrary program will halt. Loosen any of these qualifiers and the problem is not necessarily undecidable. Loosening the "arbitrary program" restriction, the problem of analyzing the termination of a subset of programs which doesn't encode looping or recursion constructs ( i.e. simply typed lambda calculus ) is trivially decidable. A totality checker like in Agda can decide whether some programs halt given a set of restrictions on the program.
> I thought the point of monads was that they provide a mechanism for introducing side effects gracefully into a pure language
That's roughly a description of the IO monad, which is a specific monad. The IO monad is really a degenerate case, and most monads ( List, Cont, Maybe, Writer, State, ... ) have nothing to do with effects.
Half the problem of talking about monads is that in their full generality they're really just a description of a trivial algebraic structure that doesn't really impart much intuition. Monads just get a lot of press because they're one of the simplest examples of a structure that can't be compressed easily in terms of common experience. There's nothing I can point to in our our everyday experience and say "monad" is like this.
data Datum = S String | D Double
lst :: [Datum]
lst = [S "a", D 3.14]
In Python we'd have to write the logic to handle both cases and fail with an exception or do an instanceof check. In Haskell we'd do this by pattern matching on the sum type.
case (lst !! 42) of
S n -> -- handle string
D n -> -- handle number
Inference is orthogonal, I mean that a records don't have a distinct type in the type system. So structurally the following types are the same in Haskell, except one elaborates out a selector function.
data Foo = Foo { name :: String }
data Foo = Foo String
What row polymorphism does is give use first-class record types that give us a measure of structural typing so that records with the "same" fields can be used in the same type and "larger" records can inhabit "smaller" types if the fields subsume. So we can write down a function like:
foo :: forall r. { a :: Int, b :: Int | r } -> Int
foo x = x.a + x.b
The current proposal doesn't give us this. But we can still simulate it even if it isn't in the language.
From the talks I've seen Gundry usually tends to qualify comments about OverloadedRecordFields by saying it's not traditional row polymorphism ( i.e. Record { name :: String | r }) ). It doesn't allow row extension or row restriction as first-class constructs in the type system. Although we can build these things as secondary features on top of the language as many libraries currently do though.
Have to figure it takes 10-20 years to grow an industrial strength language. It takes a lot of faith in an idea or stubbornness ( probably both ) to go through that struggle. I admire people with that kind of dedication and I wish exploring the language design space wasn't such an enormous investment.
If I recall from Linus Torvald's biography, he took advantage of his 8 years at university to write his first prototype of what would later become the Linux kernel. Sounds like the Finnish system liberated him to work to pursue important work without having to worry about basic economic concerns.
This discussion is just going to reduce down to a runtime tag vs formal type definition. This particular article is using the term type to mean formal type, and my comment is also under this assumption. Under that definition Ruby does have a null type system. That's not a moral judgement of it's design, it's just a fact that follows from the definitions.
You're putting words in my mouth by implying I denigrated Ruby as unsafe using a much stronger definition of safety. Ruby is type safe under the article's definitions, but I suggest that this claim doesn't carry much information content because a conclusion about the null type system is such a weak claim, like a claim about the null set.
> As such, we can think of these languages as type safe according to the null type system
I think a term like vacuously type safe is a good description of what Python/Ruby are under this set of definitions. So as to distinguish from languages where type safety actually means something slightly stronger than "all syntactically valid programs are accepted by the null type system".
No, HM algorithm has terrible worst case complexity, but the worst cases don't correspond to programs humans write and generally it works perfectly in practice.
> I mean, how can you even try to ask people to improve their communication skills, when you say that people that do not think programming is math is because they have the wrong notion of math?! I just don't see how you are going to convince anyone of anything with that level of condescension.
You're projecting a level of condescension onto Gershom's words that just isn't there and makes no sense within the context of the article. His point is that the "debate" about programming/mathematics is largely one of semantics and consists of well-intentioned people arguing from a different set of definitions. I'd hardly consider this to be a controversial statement, much less condescending.
Historically I think Haskell will be very important as the substrate on which a lot of the next generation of dependently-typed languages (Idris, Agda) are bootstrapped on top of. It's a niche use admittedly, but it's hard to understate how great Haskell is for writing modern functional compilers.
STM is not a great fit for this kind of problem, there's no need for all the transaction machinery if the problem is embarrassingly parallel. In an ideal world what you want is threads which just split the work sections like they do in C/C++/Haskell.
If you're holding a global mutex every 100 instructions while context switching between CPU bound tasks, then yes, the GIL does suck. There are a class of IO-bound problems where threading/evented models in Python can be used effectively but that's not the class of problems the author is talking about here.
If you're working on CPU-bound tasks with NumPy/SciPy using threads then you have to think very hard to make sure most of the critical sections are hitting the NumPy calls in C which release the GIL. It's not a great reliable way to program. The way the author describes is basically the only pure-Python way of achieving parallelism for this kind of problem.
Unidirectional inference in the presence of subtyping is undecidable in the general case. Languages like Haskell and OCaml don't have this problem because they don't include subtyping precisely for this reason.
What you're saying is like arguing that the Japanese should switch from Kanji to Latin characters because more people worldwide use them. That's the language, it's not going to change. It's just silly to criticize Haskell/Japanese for not being immediately understandable without study.
mtl has been around for a while now and using any the monads from the mtl transformers library is very inferrable, although like any inference it returns the most general type possible and it's generally just good practice to forward declare the type.
example = do
a <- ask
modify (+ a)
b <- get
tell [b]
GHC correctly infers:
example :: (Num s, MonadState s m, MonadReader s m, MonadWriter [s] m) => m ()
Indeed, the discipline of computer science is really the study of computation and the ideas we want to convey from a first language are things like abstraction, recursion, proof by induction, equational reasoning, sequential/parallel time-complexity. It's much easier to address these foundational concepts in a functional setting (Scheme, SML, etc) and then once undergrads know how to formally reason and do proofs about their programs introduce other languages.
It is helpful and appropriate to point out bugs, and his comments did help fix the Typeable exception problem in GHC 7.8. But he doesn't go through the usual tracker and mailing list to report these things. He goes off and writes these angry blog posts and extrapolates small defects to justify sensationalist claims about the whole language. On one hand you have a respected PL researcher, on another you have a guy who is like the axe-grinding "Zed Shaw" of functional languages.
I've read his papers and I own his books, so I'm not entirely unfamiliar with his contributions to the field. But I also find his criticism of Haskell to be at best detached from reality and a "holistic" view of the programming profession as a union of theory, engineering, and community. Especially when he's arguing for the use of pure academic languages like Agda or antiquated ML-dialects that haven't seen active development in 15 years, over a productive language like Haskell. In an industry where regression languages like Go and Javascript are seeing wide adoption, I think his grandstanding does a lot more harm than good.
There is a strong argument to be made that software profession does have some resemblance to pop music culture. "[Pop culture] it has nothing to do with cooperation, the past or the future — it's living in the present." Alan Kay 'made this rather salient observation a while back and the more I think about it the more truth I find in it.
> Generally, to finally provide my personal take, I think that Harper is dead right so long as you consider programming languages to be "means of expression". I think that's an interesting POV on languages generally and it's not totally at odds with the more everyday POV that languages are "tools for creation".
That's a very concise way of putting it. My personal issue with a lot of what Harper writes is not that it's technically wrong per se, but it only makes sense if one is discussing programming languages purely from first principles. Harper seems really taken aback by the popularity of Haskell compared to SML in the functional programming space, and yet can't seem to wrap his head around the reason for the adoption is not so much about having ideal PL semantics but the fact Haskell has an industrial-strength cross-platform compiler with meaningful answers to modern problems ( FFI, concurrency, package management ). Haskell is rather unique in that it has a community that seems interested in building a language as both a "means of expression" and "tools for creation" and we've made some compromises between the two, no doubt. A lot of Harper's comments ( and many PL theorists ) seem to completely casually gloss over the gritty compiler engineering as if it's just beneath them, and that guys like SPJ and Simon Marlow are just wasting their time working on faster runtime systems and optimizations when he thinks they should be working on foundational "Holy Trinity" problems.
It's a technical term so the colloquial definition has little relevance to it's use in computing. You can read the definition in TAPL or PFPL.
> tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
The dynamic typing folks don't care to provide a definition of types and overload the term to mean many things, the static typing folks have a rigorous one.
Types are the world's most popular verification technique. The whole intent of types is to automate many of the proofs required to guarantee the correctness of the program rather than having the human operator get bogged down in verifying the details themselves. Now yes, you can't verify all aspects of the program but types can still get you quite a distance of the way there at comparatively very little cost compared to more heavy formal verification techniques.