[cubefox]

That seems improbable. Pure functional languages are very unpopular according to TIOBE. In particular, interest in Haskell seems to be in decline. Functional features are mostly just an add-on to programming languages with mutable state. By far the most popular language, Python, doesn't even have static typing.

[Fraterkes]

I know powerful typing features are very important for Haskell in particular, but is static typing considered a functional feature more broadly? Most lisps don't have static typing as far as I know. Clojure was one of the main functional languages that actually saw industry use for a while, and it is dynamically typed.

[marcosdumay]

It seems to me that algebraic nominal types are getting strongly attached to functional programming right now. Even on multi-paradigm languages, both idioms tend to come together.

It's not a necessary relation, those things are pretty much independent. Except in that pattern matching and function composition complement each other very well.

[JacobGoodson]

"but is static typing considered a functional feature more broadly"

It might be, but it is not an essential feature. Functional programming is the practice of using pure functions as the primary form of computation and composition. Whether one adds types to this is as relevant as adding types to any other paradigm (imperative, oop, logical, functional, etc)

[Fraterkes]

Right, that was my assumption. I asked because the person I replied to mentioned the popularity of dynamic languages as a data-point for the decline in popularity of functional programming.

[JacobGoodson]

To drive the point a little further, all of those paradigms encompass both statically typed languages and dynamically typed ones.

[ahf8Aithaex7Nai]

That's already been happening for quite some time. Mainstream programming has done little else in recent years than converge toward functional programming.

Also, they wrote "functional," not "purely functional."

By the way, from a formal perspective, imperative programming is an extension of purely functional programming.

[rauljara]

This is true, in that most of the scholarship builds up its proofs starting with the lambda calculus. But there are so many paradigms (Turing machines, SKI combinators, excel spreadsheets) that are equivalent that I’m not at all convinced they had to start with lambda calculus. They just happened to.

Out in the real world, the thing that all programming languages are actually built on top of looks much more like a Turing machine than a collection of composed anonymous functions. But of course if you want to make your programs go really fast, you can’t treat them like Turing machines either. You need to acknowledge that all of this theory goes out the window in the face of how important optimizing around memory access is.

Which isn’t to say one perspective is right and one is wrong. These perspective all exist and have spread because they can all be useful. But acting like one of them is “reality” isn’t all that helpful.

Ps. Not that the parent actually said the formal perspective was reality. I just wanted to articulate this thought I had bouncing around in my head for a while.

[zozbot234]

> Out in the real world, the thing that all programming languages are actually built on top of looks much more like a Turing machine than a collection of composed anonymous functions.

Hardware logic as described in a HDL language is precisely a collection of "composed anonymous functions", including higher-order functions which are encoded as "instructions" or "control signals". We even build stateful logic from the ground up by tying these functions together in a "knot", with the statefulness being the outcome of feedback.

[jove_]

But it's hard to argue the machine at the end is stateless. We can endlessly do this. You can construct lambda calculus with Turing machines and Turing machines in lambda calculus.

There seems to be this weird idea in the functional community that the existence of some construction of one thing in another shows that one of those things is "more fundamental" than the other, when in reality this is often a circular exercise. e.g. Functions can be formalized as sets and sets can be formalized as functions.

Even worse in this specific case, the Church-Turing thesis tells us that they're equivalent, which is the only sensible answer to the question of which is more fundamental. There's an oft quoted phrase of "deep and abiding equivalencies" and it bears pointing out how deep and abiding these equivalencies are. From a formal perspective they are the same. Yes, there's arguments could be made that typed lambda calculus and its relation to logic are important, and that's true but it's not a formal argument at all and I think it's best to be clear on that.

[ahf8Aithaex7Nai]

> You can construct lambda calculus with Turing machines and Turing machines in lambda calculus.

I realize that these models of computation are equivalent. My point was rather that the imperative paradigm collapses into the functional paradigm in practical programming when I disregard the admissibility of arbitrary side effects.

> e.g. Functions can be formalized as sets and sets can be formalized as functions

I can derive functions from set theory in my sleep, and I can kickstart set theory without functions, but I wouldn't know how to define the concept of a function without sets. And even if I did: I can't even specify the characteristic function of a set without resorting to the inclusion relation.

> But it's hard to argue the machine at the end is stateless.

I'm not really that interested in the relationship between the various paradigms and the machine. What interests me most is how well I, as a human being, can write non-trivial programs. To me, it is immediately obvious that the composition of purely functional program units is conceptually simple enough to be done by a child, while unrestricted side effects can very quickly make things very complicated. However, I don't want to get involved in the discussion on this topic. I have accepted that others see it differently, although I find that completely baffling. I don't want to take away anyone's for loops, etc. To each their own.

[cubefox]

> I realize that these models of computation are equivalent. My point was rather that the imperative paradigm collapses into the functional paradigm in practical programming when I disregard the admissibility of arbitrary side effects.

But in practical programming with imperative languages, arbitrary side effects can't be disregarded, so they don't collapse into the functional paradigm. In fact, from a physical perspective, every possible CPU has states, so the most physically fundamental model of computation (something like register machines, or GOTO programs) is imperative and more fundamental than functional models, like untyped lambda calculus. Functional models might be more mathematically elegant though.

> I wouldn't know how to define the concept of a function without sets.

Whitehead and Russell showed how to define functions just in first-order logic with identity, without requiring any set theoretical axioms, by defining an n-ary function via an n+1 place relation. See here top right: https://mally.stanford.edu/Papers/rtt.pdf

This is quite natural, because predicates (properties and relations) already occur in natural language, while sets do not; they are a mathematical abstraction. For example, sets can be empty, or arbitrarily nested, or both arbitrarily nested and otherwise empty, which has no analog in natural language.

> I can't even specify the characteristic function of a set without resorting to the inclusion relation.

If you try to define sets by using functions, functions are in this context assumed to be more fundamental than sets. Then you don't need to define functions. Then the inclusion relation is simply defined via the characteristic function. You don't need to define that function. Just like you, in the reverse case, don't need to define sets, if you want to define functions via sets.

[jove_]

You're looking for Grue's map theory for formalizing sets in terms of functions.

[jghn]

Good point on functional vs purely functional. To the GP, what we're seeing is that more mainstream languages are taking the most popular features from functional languages and integrating them. The combination of Scala & Rust are a perfect example given how ML inspired they are. C# has a bevy of functional trappings.

[HelloNurse]

Haskell is suitable for, and designed for, bleeding edge experiments, not for practical usage. Its low popularity says very little about the "market penetration" of better engineered functional languages.

[cubefox]

There is no other popular functional language either. Except if you count imperative languages which let you, optionally, write functional code, except that in practice most code is imperative.

[instig007]

> Haskell is suitable for, and designed for, bleeding edge experiments, not for practical usage

The notion of practicality depends on what one wishes to practice. You, for instance, are practicing FUD spreading, it's practical for you to say these things without actually doing work with the tools provided.

[HelloNurse]

I tried to learn Haskell, and while the language has merits every library I attempted to use was a problem: at best not documented enough, but more often a half-baked proof of concept.

[bheadmaster]

> By far the most popular language, Python, doesn't even have static typing.

Arguably, Python is statically typed - it's just that it only has one type: object.

[wk_end]

I know Robert Harper has advanced that argument, but I think it's only really interesting for striking a single rhetorical blow: that, uh, actually statically typed languages are trivially more expressive than Python, since Python has one static type and they have as many as you want.

But I think as an actual ontology, as an actual way of understanding and structuring the world, it's obviously quite silly. There's no compile-time (static) type checking phase in Python, because it'd be trivial and therefore a waste of time. Without static type checking, what does it mean to say it's "statically" typed? Moreover, the language has an entirely different, extraordinarily related concept of type which is checked dynamically. Yes, you can say that "Python is a statically typed language with only a single meaningless static type and but also dynamically checked dynamic types", but frankly that's not telling you anything that calling it a dynamically typed language isn't.

From a different angle, you can't program SML or something "monotypically" - just restricting yourself to one type - without effectively building an interpreter for an entirely separate, dynamic language inside of it (you can of course build a statically typed language inside of Python, so if you think that counts you're just stripping the meaning from comparing languages). In that sense, Python's just plain doing something fundamentally different from what "a static language with one type" is.

[zozbot234]

These so-called dynamic types are merely the equivalent of tags in a discriminated union/variant type. Statically-typed languages can easily do the same thing: the argument that this amounts to "building an interpreter" applies to any language implementation.

[remexre]

> These so-called dynamic types are merely the equivalent of tags in a discriminated union/variant type.

That's far more true in a language like JavaScript or Scheme than in an "everything is an object" language like Python; the only reason why you would need a variant type for PyObject is to avoid the circular data structures the actual implementation uses.

If you allow the circular data structures, your dynamic types instead are "merely" a relatively complicated codata type, but it's far less obvious that this is actually what anyone considers to be "merely."