I think it's time to elevate the function into the same status as the number.
A number is ultimately founded on sets. A number is a most basic way to structure sets. Every number can be made out of pure sets (and later on, from tuples of sets-as-numbers)
At the moment, functions are also founded in terms of sets. But I think that mathematics can be constructed based on functions instead of sets. As far as I understand, this can be done using simple type theory; but I still have some studying to do about STT.
In any case, my point is that most mathematics since around the 18th century are not really working with numbers, but with functions as if they were numbers.
relations are also defined in terms of sets: As a sets of pairs, e.g. an element of a set like {x ,{x,y}} is just the pair (x,y), a set of such pairs IS a relation.
moreover, in terms of sets functions are a relation with some restrictions:
- That they are binary relations
- The "functional-requirement" (as I call it) refers to the difference between a relation and a function. for every x, f(x) = (only one thing); e.g. a relation can have pairs (x,a) and (x,b) but no function can do this.
As far as I've understood, this gets really "fun" when characteristic-functions enter the scene... With these boolean-valued functions it's possible to define a set.
I’m aware of all that, but it doesn’t really answer my question. If functions can be used as a fundamental concept not based on sets (maybe similar to arrows in category theory), what prevents generalizing that approach to relations? While relations lose the guarantee of single-valuedness, they gain the guarantee of being invertible (or in the case of n-ary relations, arguably a further generalization, permutable).
Since all three notions are closely interrelated, it's fairly trivial to take any one you choose as "fundamental" and define the others in terms of it:
- Sets as fundamental: define ordered pairs via Kuratowski's definition, define relations as sets of ordered pairs, define functions as relations not containing any two ordered pairs with the same first projection but different second projections
- Relations as fundamental: define sets as unary relations, define functions as relations the same way as before
- Functions as fundamental: define sets as functions where the codomain is some fixed singleton (characteristic functions are more appropriate for subsets of a set, rather than sets on their own), define relations as functions whose codomains are power sets
Because of this sort of thing, I don't think any notion of "fundamental" that's purely based on interdefinability really makes much sense.
I personally have a sense that some definitions are "constructive" and others are "destructive" (my use of "constructive" here is in no way related to "constructive" as in "constructive logic", it's just based on the English meaning of "construct"). Of the definitions I gave above, I perceive the definitions of functions and relations from sets, of functions from relations, and relations from functions as "constructive", while the definitions of sets from functions and from relations are "destructive". Since I can't think of any "constructive" definition of sets from functions or relations, while I can think of "constructive" definitions in the opposite direction, I would say sets are more fundamental than functions and relations. Whereas since both relations and functions can be "constructively" inter-defined, I'd say they're both on the same level.
Admittedly, I have no idea how to define "constructive".
Right, I’m actually not convinced that it’s possible to have functions (or relations) as fundamentals without presupposing a concept of sets (domains/codomains) in the first place.
But assuming that it is possible (as the GP believes), my feeling is that relations would be more general, maybe similar to how graphs are a more general concept than directed graphs. Representing relations as functions to power sets feels rather complex to me compared with functions being a special type of relation, which is why I would find the latter more natural. And thus I was wondering whether the GP maybe has a good reason to go with functions rather than relations.
The ‘common’ strategy of going with functions first are mostly due to Type Theoretic Foundations research. The most usual presentation presents the function type as foundational and inherent for the development.
There has been some research pushing towards Function types being a specialization of Relations as types, where relations become the foundational elements. But I think the biggest point of contention in your comment is finding sets (i.e. Domains/Codomains) to be required to define functions.
Most of this discussion is inspired (either implicitly or explicitly) by the type theoretic foundations. There is a fundamental difference between sets and types, but they are both used to describe the ‘inputs’ and ‘outputs’ of a function in general discussion. However, type theoretical foundations takes types to be the foundation of mathematics, so sets are then defined in terms of types and do not act as the ‘inputs’ and ‘outputs’ for functions.
Thanks. Can you recommend where I can read up on the precise formal definition of ‘type’ in that sense, and how sets are then defined in terms of types? So far I only have seen (too) informal discussions on that.
I think the first recommendation would be the SEP (Stanford Encyclopedia of Philosophy) article on Type Theory written by Couquand [1]. It is a broad but well founded walk through the basis of type theory and it’s usage as a foundation for both logic and mathematics. It also contains a section discussing Univalent Foundations, which is the foremost area for type theoretic foundations at present. The papers listed in the reference section contain most of the fundamental research results of note. I do think Aczel’s “The type theoretic interpretation of constructive set theory” (1978) and Bell’s “Types, Sets and Categories” (2012), which are both cited are good papers.
The 'destructive' definitions are a bit less common
> the definitions of sets from functions and from relations are "destructive".
so a destructive definition of a set:
- start with a relation: define unary relations... I can see how this could be 'destructive'; it has a feel like an 'overkill' (or a 'waste') to use relations and then use only half of what they provide to regard them as sets
- start with a function: to define a relation use a singleton co-domain (this is really very similar to characteristic functions. This has been quite tricky for me to wrap my head around: how in logic there's a tacit assumption of 'truth' in the sense that a predicate defines a set and if this set is empty then the predicate is 'false'. I'm studying this from the lens of modal logic and formal semantics)
to define a relation use a power set.
I think all this is still relying on sets, because a co-domain is a set, as well as a power set.
> Since I can't think of any "constructive" definition of sets from functions or relations, while I can think of "constructive" definitions in the opposite direction, I would say sets are more fundamental than functions and relations
As I understand this, the sets really are more fundamental because in the end they bring to the system (for the lack of a better word) the capability to identify things, and when dealing with functions, which come with variables, the concept of a set allows for identifying the same variables in the function's call (parametric denotation?) and the functions actual body (its computable definition)
What I'm trying to say, is why it may well be the case that sets really are more fundamental than functions.
Despite the name, I’ll note that this says far more about category theory than it does about FP. In fact, I’d argue that it’s not particularly closely related to FP at all — this should have been titled ‘The Dao of Type Systems’, or something along those lines. Certainly, the category-theoretic stuff is very interesting, and can even be quite useful for programming, but Haskell and other functional language can easily be used without any knowledge of category theory whatsoever.
> Haskell and other functional language can easily be used without any knowledge of category theory whatsoever.
Yup! Haskell borrows heavily from category theory, and there's a lot of value in knowing the stuff, but people have also been productive in SQL for decades without any formal knowledge of relational algebra.
I think there is a simple, almost obvious, but very powerful concept that gets clearer when learning relational algebra: Everything is a relation.
There is an important part about using an SQL DB which is about the engineering side of things, such as access patterns, indexing, efficient storage and so on. And then there is the side that is about relational expressions.
An intuition of mine is that people who feel more comfortable with the second part, lean on SQL (and DB features in general) to do work for them, while eschewing things like ORMs.
I know Category Theory quite well but have never used it for anything practical. Do you have any examples of practical solutions that benefitted more from Category Theory than just straight forward algebraic thinking?
Interesting, can you suggest some subjects that should be covered in a Dao of Functional Programming book? (Or perhaps recommend other books on the subject?)
> I’ll note that this says far more about category theory than it does about FP. In fact, I’d argue that it’s not particularly closely related to FP at all
I'd say CT is FP. FP is about doing algebra to derive programs and CT is the math that describes that. In Manfred von Thun’s article "Joy compared with other functional languages" ( https://www.kevinalbrecht.com/code/joy-mirror/j08cnt.html ) he asks,
> Could the language of categories be used for writing programs? Any lambda expression can be translated into a categorical expression, so the language of categories is expressively complete. But this does not make it a suitable language for writing programs. As it stands it is a very low-level language.
I think this book could be seen as the (affirmative) answer to that question.
I don’t know about clojure but lisp definitely counts as an abstract algebra (and not in the same way most other languages are.) It’s also a weird derivation of set theory allowing it to be derived from first order logic.
Having studied abstract algebra, I disagree that the soul of lisp is abstract algebra. You're not really actively thinking algebraically when you're writing lisp, not in the same way that other languages have you "actively thinking about category theory". There are also other modern FP languages that are "basically lisps", like Julia or Elixir, that would be hard to call "algebraic".
My opinion (and I don't insist that I'm right) is that you've got to go back to Backus' Turing award paper[1] to ground a definition of FP, and he was specifically talking about an algebraic approach. This is something that seems to get overlooked when people talk about FP, but I believe it's even more important than, say, referential transparency.
Functional programming is what people talk about when they "talk about FP".
The historical story is that "functional programming" just meant purity, originally. Now it seems to mean purity + higher order functions + other strong, fancy types (which I'd claim include algebraic structures such as monads).
This current meaning, exemplified by the ML/Haskell tradition, spiritually comes from Peter Landin's ideas in his paper "The mechanical evaluation of expressions" and its supporters don't revere Backus. Sure, algebraic laws characterise monads etc., and his work was foundational—but the Turing Award paper is not a script that everyone is following.
On the specific topic of deriving programs with algebra, there is the book "Algebra of Programming" by Bird and de Moor from the 90s, (https://themattchan.com/docs/algprog.pdf) but it is difficult to look at the functional programming scene now and conclude that deriving your program algebraically is a more essential aspect of the activity than using referentially transparent expressions. It may well be or become an important idea, but it's hardly the bread and butter of functional programming in practice (while maybe in your headcanon it is functional programming). I think part of the problem here is complexity/irregularity: it's simply not practical or helpful to describe typical desired systems algebraically and then derive code from that description.
> the Turing Award paper is not a script that everyone is following.
Yah, that's my point.
> it is difficult to look at the functional programming scene now and conclude that deriving your program algebraically is a more essential aspect of the activity than using referentially transparent expressions.
Again, that's my point. It's not now but it should be. We are missing out.
It's like we are still using Roman numerals even though the Indo-Arabic numeral system has been invented and is ever-so-slowly diffusing into common knowledge.
Not at all. Lambda Calculus is a much better mathematical foundational for functional programming that Category Theory is. I can teach a programmer Lambda Calculus in a few minutes and they will be able to use it for programming. Not so with CT. You need to add a lot of structure to get anything close to Lambda Calculus. Basically about 50% of a Typical CT book to get there.
Not at all. It is way more useful than learning CT. LC is the foundation used in almost all of computer science. You need to understand it to read any advanced Type Theory papers for example and you can directly use it as a starting point when designing a functional programming language.
> “the simply typed lambda-calculus is modeled by any cartesian closed category (CCC)
That is correct. You can model pretty much anything in Category Theory. The same way you can model pretty much anything in Type Theory or Set Theory. However IMHO it takes a lot more structure to build up to CCC than it does to simply use LC. The paper you are referencing is great. However the author might as well have used LC to achieve the same goal.
I will get down-vote for sure but it's trivial this book and also the series "category theory for programmers". It's actually not very far from the content of several first pages of any book on set theory or logics.
I find the ubiquitous idea is that "category theory" is more prestigous than "set theory", and some programmers, instead of seriously learning mathematics, think that learning category theory would fill up their lack of knowledge (in mathematics). It's quite contrary since category theory alone (i.e. without context) is trivial.
Let's be honest: read this book and the series of the author, and try to use the acquired knowledge to prove some (even simple) mathematical theorems.
The author’s objective is to teach the category theoretical concepts that get used in FP. This is particularly important in Haskell since it uses some of these concepts (functors, applicatives, monads, etc.) as design patterns.
He’s objective has never been for the reader to learn this and apply it to prove math theorems.
Both set and category theory are foundational systems for mathematics (or attempting to be). Category theory being newer is trending and probably why you get the sense that it’s considered more prestigious. But I’ve never heard anyone claim it is more prestigious.
I actually criticise the illusion (that the book and the series bring) that the category theory is "the ultimate source" of motivation in FP languages.
On one hand, it's direct (and very natural) to reproduce some categorical structures in a FP language (e.g. Haskell, ML) since such a language is around functions and values. I doubt that such categorical structures should be considered patterns.
On other hand, Haskell or ML does not come from the category theory, it comes from PCF as a language which is created to make program correctness proving is "easy".
I dont want to mean someone using this book to prove mathematical theorems, I just want to say that it's superficial (about both category theory and computer science), and does not bring sufficient knowledge upon that we can build nontrivial results.
> and some programmers, instead of seriously learning mathematics, think that learning category theory would fill up their lack of knowledge (in mathematics). It's quite contrary since category theory alone (i.e. without context) is trivial.
High applauds for this part.
Category Theory, by design, attempts to be more general, more basic and more abstract.
1. You cannot learn the more abstract stuff first. You have to learn the special cases first- i.e. Calculus, Set Theory, Analysis, etc. You do not start studying Physics with General Relaitivity or Quantum Mechanics because they are more general. You learn them after long years of studuying special Physics of fluid motion, Newton's Law. One should not think that one can simply get a "shortcut" to the most general thing there is, without learning the special cases.
2. A lot of more general sciences are indeed special cases. When you are asked to find the set of points in a certain domain where the derivative of a function cannot be found, you are not actually doing Set Theory. You are doing Calculus.
I believe that the notion one can learn the abstract cases just by studying the abstract science is laughably wrong. They better study Theology. Shouting out "Monad is a monoid in a category of endofunctors" doesn’t teach you Math.
However, let me end this comment and rant with a book suggestion.
Please read "Seven Sketches of Composionality" if are looking for books to learn Category Theory.
I wish I hadn't bought into the functional programming cult so hard as a younger programmer. I thought it was the future and sacraficed learning and gaining mastery of OOP for that when OOP is a much more widely used and honestly now in hindsight probably better tool in most cases.
This is my own inexperience with OOP showing: I keep wondering if trait/protocol/interface programming has made inheritance entirely worthless. Love Rust. I've been working in Java for other reasons, but I've been noticing more and more Rust-like things in Java over the past year.
My day job is programming in Java, and I use streams and lambdas everywhere. I use very little of OO concepts like inheritance. I try to make my data immutable and write functions and methods without side effects, wherever possible.
Popular recent languages like Go, Rust, and Swift borrow a lot from functional programming paradigms.
I'm curious where you are seeing OOP still going strong.
You brought up the worst part of OOP, inheritance. Which most modern OOP rarely uses. Since the 90s “composition over inheritance” has been a mantra. If you want to build strong arguments, focus on real issues. Not incompetent programmers abusing inheritance or abstract factory factories, because they can write just as awful code in functional programming. There are plenty of actual OOP issues to hate on, but that’s because there is no silver bullet.
What is OOP today in practice if inheritance is dead, as you say, and mutability is out of style, as I've notice in all of the codebases I've worked on since ~2014?
It feels like we're just left with a heavyweight syntax for structs + functions bound to data, which feels like pretty thin gruel.
The concept of composition has long been the bread and butter of functional programming paradigm since antiquity. OOP just adopted it later in the wake of nightmare inheritance hierarchies.
Not him/her but I'm writing a compiler, I use functional, sure, but most of it is AST objects, expression objects (which fit OOP very well), internal representations of other objects. Lorra, lorra objects. Working well.
This hasn't been my experience. FP is a fantastic complement to OOP for "practical" programming. It adds an entirely new dimension and avenue for expressability which is why we're seeing more and more OOP languages borrow heavily from FP. For all its abstractions, OOP tends to encourage stateful design and accumulate complexity which is where FP shines.
Interesting. Throughout college and the first 4-5 years of my professional career I only knew OO. Then I learned some FP and it made me a much better OO programmer. Specifically, immutable data and pure functions are probably the 2 most important concepts that improve the code that I write in OO-focused languages. I couldn't believe that I was without those techniques for so many years.
Nowadays I can find a few isolated uses for "classes", but never, and I mean not a single situation where "OOP" (object ORIENTED programming) could ever be preferrable to just using data and functions, whether that's strictly functional programming or plain old procedural.
Could you share more about where you believe OOP hierarchies offer an advantage?
ECS is I believe most popular game architecture to achieve high performance and code maintainability, displacing OOP in most non-Godot games. And for Godot in particular, there's Godex which provides ECS for it and candidly beats default Godot OOP idioms by using a more functional approach.
How do you explain the industry-wide switch away from OOP frameworks to things like React and other Elm-architecture derived libraries?
I personally have used a lot of UI libraries, and I would never willingly use anything object oriented again even before React clearly became "the thing". So this is a fairly suprising claim to me in 2022, not so much if it had occurred 10 years ago.
There are many different programming paradigms; Logic, functional, declarative, iterative, OOP, stack-based (if you consider Forth style languages their own paradigm). Each has its pros and cons.
>> much more widely used and honestly now in hindsight probably better tool in most cases.
Knowing only OOP means OOP becomes the only tool for all cases.
"Tao" is an old translation with (I think) the Wade-Giles system, while "Dao" uses the correct consonant that matches the Mandarin pronounciation of that word.
It has to do with how we carry words from Chinese to English.
``Is Daoism the same as Taoism? Traditionally, yes. The difference in spelling is a problem of transliteration from Chinese to English, where the Chinese pronunciation is somewhere between “Tao” and “Dao.” While it’s far more common to transliterate it as “Taoism,” it is actually pronounced closer to “Daoism.” "[1]
If anyone is interested in learning FP and how to think about it, I personally recommend three resources:
1. Martin Odersky's "Functional Programming Principles in Scala" MOOC on Coursera. Do not focus on the Scala part (5-10% of the course is about Scala).
2. The Little Schemer book. Among the best programming books U have ever read in my life. It actually teaches you how to think recursively. It actually does that.
3. Graham Hutton's Haskell book and YouTube playlist.
77 comments
[ 4.5 ms ] story [ 147 ms ] threadhttps://bartoszmilewski.com/2014/10/28/category-theory-for-p...
Will use this to test, and learn again about it. Get it while is still hot (Last updated: May 21, 2022)
[1] https://bartoszmilewski.com/2021/02/16/functorio/
A number is ultimately founded on sets. A number is a most basic way to structure sets. Every number can be made out of pure sets (and later on, from tuples of sets-as-numbers)
At the moment, functions are also founded in terms of sets. But I think that mathematics can be constructed based on functions instead of sets. As far as I understand, this can be done using simple type theory; but I still have some studying to do about STT.
In any case, my point is that most mathematics since around the 18th century are not really working with numbers, but with functions as if they were numbers.
If not, I recommend reading it.
(why not both?)
moreover, in terms of sets functions are a relation with some restrictions:
- That they are binary relations
- The "functional-requirement" (as I call it) refers to the difference between a relation and a function. for every x, f(x) = (only one thing); e.g. a relation can have pairs (x,a) and (x,b) but no function can do this.
As far as I've understood, this gets really "fun" when characteristic-functions enter the scene... With these boolean-valued functions it's possible to define a set.
- Sets as fundamental: define ordered pairs via Kuratowski's definition, define relations as sets of ordered pairs, define functions as relations not containing any two ordered pairs with the same first projection but different second projections
- Relations as fundamental: define sets as unary relations, define functions as relations the same way as before
- Functions as fundamental: define sets as functions where the codomain is some fixed singleton (characteristic functions are more appropriate for subsets of a set, rather than sets on their own), define relations as functions whose codomains are power sets
Because of this sort of thing, I don't think any notion of "fundamental" that's purely based on interdefinability really makes much sense.
I personally have a sense that some definitions are "constructive" and others are "destructive" (my use of "constructive" here is in no way related to "constructive" as in "constructive logic", it's just based on the English meaning of "construct"). Of the definitions I gave above, I perceive the definitions of functions and relations from sets, of functions from relations, and relations from functions as "constructive", while the definitions of sets from functions and from relations are "destructive". Since I can't think of any "constructive" definition of sets from functions or relations, while I can think of "constructive" definitions in the opposite direction, I would say sets are more fundamental than functions and relations. Whereas since both relations and functions can be "constructively" inter-defined, I'd say they're both on the same level.
Admittedly, I have no idea how to define "constructive".
But assuming that it is possible (as the GP believes), my feeling is that relations would be more general, maybe similar to how graphs are a more general concept than directed graphs. Representing relations as functions to power sets feels rather complex to me compared with functions being a special type of relation, which is why I would find the latter more natural. And thus I was wondering whether the GP maybe has a good reason to go with functions rather than relations.
There has been some research pushing towards Function types being a specialization of Relations as types, where relations become the foundational elements. But I think the biggest point of contention in your comment is finding sets (i.e. Domains/Codomains) to be required to define functions.
Most of this discussion is inspired (either implicitly or explicitly) by the type theoretic foundations. There is a fundamental difference between sets and types, but they are both used to describe the ‘inputs’ and ‘outputs’ of a function in general discussion. However, type theoretical foundations takes types to be the foundation of mathematics, so sets are then defined in terms of types and do not act as the ‘inputs’ and ‘outputs’ for functions.
1 —- https://plato.stanford.edu/entries/type-theory/
Sets -[construct-into]-> Relations -[construct-into]-> Functions
The 'destructive' definitions are a bit less common
> the definitions of sets from functions and from relations are "destructive".
so a destructive definition of a set:
- start with a relation: define unary relations... I can see how this could be 'destructive'; it has a feel like an 'overkill' (or a 'waste') to use relations and then use only half of what they provide to regard them as sets
- start with a function: to define a relation use a singleton co-domain (this is really very similar to characteristic functions. This has been quite tricky for me to wrap my head around: how in logic there's a tacit assumption of 'truth' in the sense that a predicate defines a set and if this set is empty then the predicate is 'false'. I'm studying this from the lens of modal logic and formal semantics)
to define a relation use a power set.
I think all this is still relying on sets, because a co-domain is a set, as well as a power set.
> Since I can't think of any "constructive" definition of sets from functions or relations, while I can think of "constructive" definitions in the opposite direction, I would say sets are more fundamental than functions and relations
As I understand this, the sets really are more fundamental because in the end they bring to the system (for the lack of a better word) the capability to identify things, and when dealing with functions, which come with variables, the concept of a set allows for identifying the same variables in the function's call (parametric denotation?) and the functions actual body (its computable definition)
What I'm trying to say, is why it may well be the case that sets really are more fundamental than functions.
may I recommend this links to read up on the precise formal definition of ‘type’
https://plato.stanford.edu/entries/type-theory/
Simple Type Theory https://plato.stanford.edu/entries/type-theory-church/
https://github.com/adamnemecek/adjoint/
Yup! Haskell borrows heavily from category theory, and there's a lot of value in knowing the stuff, but people have also been productive in SQL for decades without any formal knowledge of relational algebra.
Asking as a practioner interested in learning the conceptual underpinnings :)
There is an important part about using an SQL DB which is about the engineering side of things, such as access patterns, indexing, efficient storage and so on. And then there is the side that is about relational expressions.
An intuition of mine is that people who feel more comfortable with the second part, lean on SQL (and DB features in general) to do work for them, while eschewing things like ORMs.
I'd say CT is FP. FP is about doing algebra to derive programs and CT is the math that describes that. In Manfred von Thun’s article "Joy compared with other functional languages" ( https://www.kevinalbrecht.com/code/joy-mirror/j08cnt.html ) he asks,
> Could the language of categories be used for writing programs? Any lambda expression can be translated into a categorical expression, so the language of categories is expressively complete. But this does not make it a suitable language for writing programs. As it stands it is a very low-level language.
I think this book could be seen as the (affirmative) answer to that question.
I don’t think I can agree. Clojure is a functional programming language, but is far from doing any algebra.
[1] https://amturing.acm.org/award_winners/backus_0703524.cfm then click on "ACM Turing Award Lecture" or just -> https://dl.acm.org/ft_gateway.cfm?id=1283933&type=pdf
The historical story is that "functional programming" just meant purity, originally. Now it seems to mean purity + higher order functions + other strong, fancy types (which I'd claim include algebraic structures such as monads).
This current meaning, exemplified by the ML/Haskell tradition, spiritually comes from Peter Landin's ideas in his paper "The mechanical evaluation of expressions" and its supporters don't revere Backus. Sure, algebraic laws characterise monads etc., and his work was foundational—but the Turing Award paper is not a script that everyone is following.
On the specific topic of deriving programs with algebra, there is the book "Algebra of Programming" by Bird and de Moor from the 90s, (https://themattchan.com/docs/algprog.pdf) but it is difficult to look at the functional programming scene now and conclude that deriving your program algebraically is a more essential aspect of the activity than using referentially transparent expressions. It may well be or become an important idea, but it's hardly the bread and butter of functional programming in practice (while maybe in your headcanon it is functional programming). I think part of the problem here is complexity/irregularity: it's simply not practical or helpful to describe typical desired systems algebraically and then derive code from that description.
Yah, that's my point.
> it is difficult to look at the functional programming scene now and conclude that deriving your program algebraically is a more essential aspect of the activity than using referentially transparent expressions.
Again, that's my point. It's not now but it should be. We are missing out.
It's like we are still using Roman numerals even though the Indo-Arabic numeral system has been invented and is ever-so-slowly diffusing into common knowledge.
Which programmer? Bare Lambda Calculus? Wouldn't that be pretty useless?
> Not so with CT. You need to add a lot of structure to get anything close to Lambda Calculus.
I'm not sure I follow, I've heard that "the simply typed lambda-calculus is modeled by any cartesian closed category (CCC)." http://conal.net/papers/compiling-to-categories/
Not at all. It is way more useful than learning CT. LC is the foundation used in almost all of computer science. You need to understand it to read any advanced Type Theory papers for example and you can directly use it as a starting point when designing a functional programming language.
> “the simply typed lambda-calculus is modeled by any cartesian closed category (CCC)
That is correct. You can model pretty much anything in Category Theory. The same way you can model pretty much anything in Type Theory or Set Theory. However IMHO it takes a lot more structure to build up to CCC than it does to simply use LC. The paper you are referencing is great. However the author might as well have used LC to achieve the same goal.
I find the ubiquitous idea is that "category theory" is more prestigous than "set theory", and some programmers, instead of seriously learning mathematics, think that learning category theory would fill up their lack of knowledge (in mathematics). It's quite contrary since category theory alone (i.e. without context) is trivial.
Let's be honest: read this book and the series of the author, and try to use the acquired knowledge to prove some (even simple) mathematical theorems.
He’s objective has never been for the reader to learn this and apply it to prove math theorems.
Both set and category theory are foundational systems for mathematics (or attempting to be). Category theory being newer is trending and probably why you get the sense that it’s considered more prestigious. But I’ve never heard anyone claim it is more prestigious.
I actually criticise the illusion (that the book and the series bring) that the category theory is "the ultimate source" of motivation in FP languages.
On one hand, it's direct (and very natural) to reproduce some categorical structures in a FP language (e.g. Haskell, ML) since such a language is around functions and values. I doubt that such categorical structures should be considered patterns.
On other hand, Haskell or ML does not come from the category theory, it comes from PCF as a language which is created to make program correctness proving is "easy".
I dont want to mean someone using this book to prove mathematical theorems, I just want to say that it's superficial (about both category theory and computer science), and does not bring sufficient knowledge upon that we can build nontrivial results.
High applauds for this part.
Category Theory, by design, attempts to be more general, more basic and more abstract.
1. You cannot learn the more abstract stuff first. You have to learn the special cases first- i.e. Calculus, Set Theory, Analysis, etc. You do not start studying Physics with General Relaitivity or Quantum Mechanics because they are more general. You learn them after long years of studuying special Physics of fluid motion, Newton's Law. One should not think that one can simply get a "shortcut" to the most general thing there is, without learning the special cases.
2. A lot of more general sciences are indeed special cases. When you are asked to find the set of points in a certain domain where the derivative of a function cannot be found, you are not actually doing Set Theory. You are doing Calculus.
I believe that the notion one can learn the abstract cases just by studying the abstract science is laughably wrong. They better study Theology. Shouting out "Monad is a monoid in a category of endofunctors" doesn’t teach you Math.
However, let me end this comment and rant with a book suggestion.
Please read "Seven Sketches of Composionality" if are looking for books to learn Category Theory.
My day job is programming in Java, and I use streams and lambdas everywhere. I use very little of OO concepts like inheritance. I try to make my data immutable and write functions and methods without side effects, wherever possible.
Popular recent languages like Go, Rust, and Swift borrow a lot from functional programming paradigms.
I'm curious where you are seeing OOP still going strong.
huh?!
It feels like we're just left with a heavyweight syntax for structs + functions bound to data, which feels like pretty thin gruel.
That seems a little early. I think the 90's were still pretty inheritance-centric.
Java only came out in 1996. UML 2.0 was releaeased in 2005.
I'd say the composition over inheritance movement wasn't widespread until the 2000's,
I guess my memory was wrong (or I was hanging around the wrong crowd in the 90's.)
The concept of composition has long been the bread and butter of functional programming paradigm since antiquity. OOP just adopted it later in the wake of nightmare inheritance hierarchies.
golang doesn't. It's quite the antithesis really. They embrace mutability, no null safety, and only recently got generics.
Nowadays I can find a few isolated uses for "classes", but never, and I mean not a single situation where "OOP" (object ORIENTED programming) could ever be preferrable to just using data and functions, whether that's strictly functional programming or plain old procedural.
Could you share more about where you believe OOP hierarchies offer an advantage?
I personally have used a lot of UI libraries, and I would never willingly use anything object oriented again even before React clearly became "the thing". So this is a fairly suprising claim to me in 2022, not so much if it had occurred 10 years ago.
>> much more widely used and honestly now in hindsight probably better tool in most cases.
Knowing only OOP means OOP becomes the only tool for all cases.
https://www.mit.edu/~xela/tao.html
``Is Daoism the same as Taoism? Traditionally, yes. The difference in spelling is a problem of transliteration from Chinese to English, where the Chinese pronunciation is somewhere between “Tao” and “Dao.” While it’s far more common to transliterate it as “Taoism,” it is actually pronounced closer to “Daoism.” "[1]
[1]https://daoism.org/dao-or-tao/
1. Martin Odersky's "Functional Programming Principles in Scala" MOOC on Coursera. Do not focus on the Scala part (5-10% of the course is about Scala).
2. The Little Schemer book. Among the best programming books U have ever read in my life. It actually teaches you how to think recursively. It actually does that.
3. Graham Hutton's Haskell book and YouTube playlist.