From 8d88927b537cc10825d5537d76ce8e2fe340d410 Mon Sep 17 00:00:00 2001 From: Liam O'Connor Date: Fri, 30 May 2025 12:54:39 +1000 Subject: [PATCH] bits and pieces --- theme | 2 +- trees/loc-000S.tree | 7 ++++--- trees/loc-000U.tree | 25 +++++++++++++++++++++++++ trees/places/fpca89.tree | 2 +- 4 files changed, 31 insertions(+), 5 deletions(-) create mode 100644 trees/loc-000U.tree diff --git a/theme b/theme index c80c41d..7d8e231 160000 --- a/theme +++ b/theme @@ -1 +1 @@ -Subproject commit c80c41d5a878188c7ea7c011dfe206263afd8eaa +Subproject commit 7d8e231f816172966d7d53d718e0450dcb5e7e5c diff --git a/trees/loc-000S.tree b/trees/loc-000S.tree index 3135324..cc0b086 100644 --- a/trees/loc-000S.tree +++ b/trees/loc-000S.tree @@ -1,8 +1,9 @@ \import{dt-macros} \date{2025-05-25T13:36:39Z} +\author{liamoc} \title{Against Curry-Howard Mysticism} \p{As someone who teaches PL theory and has worked in PL theory for many years now, I love the [the formulae-as-types notion of construction](howard-80), also known as the Curry-Howard correspondence. It demonstrates a profound connection between lambda calculi and logic. [Wadler](wadler)'s [paper](wadler-14) and accompanying [talk](https://www.youtube.com/watch?v=IOiZatlZtGU) provide an approachable introduction to the topic.} -\p{Yet, among the audience for such talks, primarily geared at functional programming practitioners rather than academics, are many who, I think, are getting the wrong message somehow. I see muddled, severely distorted, or even outright untrue claims being made about type theory and Curry-Howard quite frequently as a result of these misconceptions. So, to clear the air, I'll state my thesis up-front:} +\p{Yet, among the audience for such talks (which are primarily geared at functional programming practitioners rather than academics) are many who, I think, are getting the wrong message somehow. I see muddled, severely distorted, or even outright untrue claims being made about type theory and Curry-Howard quite frequently as a result of these misconceptions. So, to clear the air, I'll state my thesis up-front:} \thesisblock{ \p{\strong{For programming and software engineering practice, Curry-Howard is of essentially no practical benefit, unless you are using a dependently-typed language.}} } @@ -11,7 +12,7 @@ \subtree{ \title{But I get theorems from the types!} \p{ - It \strong{is} true, however, that we learn many theorems about our programs from examining thier types. From the judgement #{f : \texttt{Int} \rightarrow \texttt{Bool}}, I know that the function #{f} will, when executed with an #{\texttt{Int}} argument, produce a #{\texttt{Bool}} result. This is indeed a theorem! But it is \strong{not} a theorem arrived at by any use of the Curry-Howard correspondence, but rather a straightfoward consequence of [type safety](https://en.wikipedia.org/wiki/Type_safety). A similar argument applies when types are used as "witnesses" of a property, e.g. ##{\textit{balance} : \texttt{Tree} \rightarrow \texttt{BalancedTree}} + It \strong{is} true, however, that we learn many theorems about our programs from examining their types. From the judgement #{f : \texttt{Int} \rightarrow \texttt{Bool}}, I know that the function #{f} will, when executed with an #{\texttt{Int}} argument, produce a #{\texttt{Bool}} result. This is indeed a theorem! But it is \strong{not} a theorem arrived at by any use of the Curry-Howard correspondence, but rather a straightfoward consequence of [type safety](https://en.wikipedia.org/wiki/Type_safety). A similar argument applies when types are used as "witnesses" of a property, e.g. ##{\textit{balance} : \texttt{Tree} \rightarrow \texttt{BalancedTree}} If #{\textit{balance}} is the \em{only} way to produce a #{\texttt{BalancedTree}}, then one might be tempted to say that this type "corresponds" to a proposition that a tree is balanced. But this is \em{not} a theorem that follows from formulae-as-types but rather from good ol' type safety and enforcement of module boundaries, just as above. } \p{The [theorems for free](wadler-89) also popularised by [Wadler](wadler), specifically the theorems obtained from the generality of a type signature, are \em{also} \strong{not} a consequence of Curry-Howard, but rather a consequence of the parametricity of the type system.} @@ -22,5 +23,5 @@ \title{Why does this happen?} \p{ Many programmers can get swept up in mysticism about Curry-Howard, overstating its consequences. Of these, I think there are two main groups: the \em{mathematically curious} and the \em{mathematical fetishists}. The \em{curious} are those who, usually through no fault of their own, have no or little experience with program specification, verification, formal methods, semantics, proofs etc, before being introduced to Curry-Howard. They then make the mistake of thinking that Curry-Howard is central to all of these new areas to them, simply because it was \em{their} starting point. To a certain extent, I do understand this viewpoint — being excited about a particular topic in research is a good thing! The good thing here, is that this problem can be resolved simply by doing better education, so that programmers' first exposure to logic, for example, isn't in third year university, when puzzling out types for lambda calculus terms.} } -\p{Fare more problematic, though, is the culture of \em{mathematical fetishism} within the functional programming community: the use of mathematical jargon to obscure rather than clarify — to show superiority over others, rather than establishing a common vocabulary. One example of this is those who insist on calling the Curry-Howard correspondence "the Curry-Howard \em{isomorphism}" because it uses an exclusively mathematical term, "\em{isomorphism}", rather than the more commonly-used (and more accurate) "correspondence". They will often talk very confidently, using large amounts of mathematical jargon, where in reality the idea under discussion is either significantly more straightforward than indicated, or outright wrong. People who behave in this way are really toxic for a programming community. The only solution I can recommend is to try hard to exclude this kind of toxic behaviour from programming communities, and to devote resources to supporting those learners who would otherwise potentially be led astray by this kind of behaviour. } +\p{Far more problematic, though, is the culture of \em{mathematical fetishism} within the functional programming community: the use of mathematical jargon to obscure rather than clarify — to show superiority over others, rather than establishing a common vocabulary. One example of this is those who insist on calling the Curry-Howard correspondence "the Curry-Howard \em{isomorphism}" because it uses an exclusively mathematical term, "\em{isomorphism}", rather than the more commonly-used (and more accurate) "correspondence". They will often talk very confidently, using large amounts of mathematical jargon, where in reality the idea under discussion is either significantly more straightforward than indicated, or outright wrong. People who behave in this way are really toxic for a programming community. The only solution I can recommend is to try hard to exclude this kind of toxic behaviour from programming communities, and to devote resources to supporting those learners who would otherwise potentially be led astray by this kind of behaviour. } \p{} \ No newline at end of file diff --git a/trees/loc-000U.tree b/trees/loc-000U.tree new file mode 100644 index 0000000..a6b9628 --- /dev/null +++ b/trees/loc-000U.tree @@ -0,0 +1,25 @@ +\import{table-macros} +\def\percent{\startverb%\stopverb + } +\parent{loc-000P} +\title{The Ascension of the Lord 2025} +\tag{cmc} +\date{2025-05-29} +\author{liamoc} +\quote{ + Viri Galilæi, quid admirámini aspiciéntes in cælum? Allelúia: quemádmodum vidístis eum ascendéntem in cælum, ita véniet, allelúia, allelúia, allelúia. +} +\p{Our choir at [All Saints Ainslie](https://allsaintsainslie.org.au) was the only one in Canberra, it seems, that actually sang at a service \em{on Ascension day}, rather than the subsequent Sunday. We sang Christopher Tye's [The Eternal Gates](https://www.youtube.com/watch?v=hcSou9sCLkA).} +\quote{ + \poem{ + \line{Th'eternal gates lift up their heads,} + \line{The doors are open wide;} + \line{The King of Glory is gone up} + \line{unto his Father's side.\br} + \line{And ever on our earthly path} + \line{A gleam of glory lies;} + \line{A light still breaks from behind the cloud} + \line{that veils thee from our eyes.} + + } +} diff --git a/trees/places/fpca89.tree b/trees/places/fpca89.tree index 637a3ce..55698b7 100644 --- a/trees/places/fpca89.tree +++ b/trees/places/fpca89.tree @@ -3,4 +3,4 @@ \title{\conf-name{FPCA '89}{4th International Conference on Functional Programming Languages and Computer Architecture}} \date{1989-09} \meta{venue}{London, United Kingdom} -\meta{doi}{10.1145/99370} \ No newline at end of file +\meta{doi}{10.1145/99370} -- 2.51.2