News for hackers. Stuff that matters.
Re:Type Theory and Functional Programming (1999) [pdf] by cubefox on Wednesday October 01, 2025 @06:19AM (#45436125)
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.
Re:Type Theory and Functional Programming (1999) [pdf] by Fraterkes on Wednesday October 01, 2025 @07:31AM (#45436522)
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.
Re:Type Theory and Functional Programming (1999) [pdf] by JacobGoodson on Wednesday October 01, 2025 @09:03AM (#45437212)
"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)

Re:Type Theory and Functional Programming (1999) [pdf] by Fraterkes on Wednesday October 01, 2025 @09:24AM (#45437430)
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.
Re:Type Theory and Functional Programming (1999) [pdf] by JacobGoodson on Wednesday October 01, 2025 @02:58PM (#45441778)
To drive the point a little further, all of those paradigms encompass both statically typed languages and dynamically typed ones.
Re:Type Theory and Functional Programming (1999) [pdf] by marcosdumay on Wednesday October 01, 2025 @11:42AM (#45439086)
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.

Re:Type Theory and Functional Programming (1999) [pdf] by ahf8Aithaex7Nai on Wednesday October 01, 2025 @07:03AM (#45436349)
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.

Re:Type Theory and Functional Programming (1999) [pdf] by rauljara on Wednesday October 01, 2025 @07:51AM (#45436644)
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.

Re:Type Theory and Functional Programming (1999) [pdf] by zozbot234 on Wednesday October 01, 2025 @08:24AM (#45436841)
> 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.

Re:Type Theory and Functional Programming (1999) [pdf] by jove_ on Wednesday October 01, 2025 @09:47AM (#45437685)
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.

Re:Type Theory and Functional Programming (1999) [pdf] by ahf8Aithaex7Nai on Wednesday October 01, 2025 @05:54PM (#45444002)
> 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.

Re:Type Theory and Functional Programming (1999) [pdf] by cubefox on Thursday October 02, 2025 @10:28AM (#45450078)
> 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.

Re:Type Theory and Functional Programming (1999) [pdf] by ahf8Aithaex7Nai on Thursday October 02, 2025 @04:30PM (#45455145)
> But in practical programming with imperative languages, arbitrary side effects can't be disregarded, so they don't collapse into the functional paradigm.

I'm sorry to have to say this so bluntly, but I think you understand as well as I do that in a language such as C#, it is entirely possible to write large amounts of purely functional yet useful code, just as you would in Haskell. That's why it's possible in SICP to wait until Chapter 3 to introduce the special form set!. That is the issue I was concerned with.

> from a physical perspective

I already mentioned that this is not the perspective that interests me. I don't care at all about the physical substrate for computation.

Thanks for the paper. I might take a look at it, although I've already been given a good tip elsewhere with map theory. I'm not convinced by the claim that properties and relations occur in natural language but sets supposedly do not.

The last paragraph isn't very helpful either. I'm not sure who is misunderstanding whom here, but we don't need to hash it out. This isn't a conversation I'm enjoying.

Re:Type Theory and Functional Programming (1999) [pdf] by jove_ on Thursday October 02, 2025 @10:34AM (#45450176)
You're looking for Grue's map theory for formalizing sets in terms of functions.
Re:Type Theory and Functional Programming (1999) [pdf] by ahf8Aithaex7Nai on Thursday October 02, 2025 @03:00PM (#45453905)
Thanks! It seems that in metatheory, one can resort to type theory in order to avoid having to fall back on set theory in a circular manner. Unfortunately, I don't know anything about that, but I'll take a closer look at it.
Re:Type Theory and Functional Programming (1999) [pdf] by jghn on Wednesday October 01, 2025 @08:18AM (#45436794)
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.
Re:Type Theory and Functional Programming (1999) [pdf] by bheadmaster on Wednesday October 01, 2025 @06:33AM (#45436186)
> 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.

Re:Type Theory and Functional Programming (1999) [pdf] by wk_end on Wednesday October 01, 2025 @07:07AM (#45436380)
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.

Re:Type Theory and Functional Programming (1999) [pdf] by zozbot234 on Wednesday October 01, 2025 @08:29AM (#45436888)
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.
Re:Type Theory and Functional Programming (1999) [pdf] by remexre on Wednesday October 01, 2025 @08:55AM (#45437119)
> 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."

Re:Type Theory and Functional Programming (1999) [pdf] by HelloNurse on Wednesday October 01, 2025 @11:51AM (#45439205)
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.
Re:Type Theory and Functional Programming (1999) [pdf] by cubefox on Wednesday October 01, 2025 @02:29PM (#45441352)
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.
Re:Type Theory and Functional Programming (1999) [pdf] by instig007 on Wednesday October 01, 2025 @05:42PM (#45443888)
> 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.

Re:Type Theory and Functional Programming (1999) [pdf] by HelloNurse on Thursday October 02, 2025 @03:37AM (#45447172)
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.