5 ms·

If you want to see how the Curry-Howard isomorphism works in practice, this is a very accessible introduction: https://groups.seas.harvard.edu/courses/cs152/202

by qsort 3y ago

If you want to see how the Curry-Howard isomorphism works in practice, this is a very accessible introduction: https://groups.seas.harvard.edu/courses/cs152/2021sp/lectures/lec15-curryhoward.pdf https://groups.seas.harvard.edu/courses/cs152/2021sp/lecture...

_a_a_a_ 3y ago
Accessible for who, do you mean? That is in no way 'accessible' without solid exposure to quite a lot of discrete maths (which I have and it's still hard going). λf :(τ 1 × τ 2 ) → τ 3 .λx:τ 1 .λy:τ 2 .f (x,y) has type ((τ 1 × τ 2 ) → τ 3 ) → (τ 1 → τ 2 → τ 3 ). Yeah, that's accessible.
- fooker 3y ago
  Seems accessible, if you're willing to look up what what you don't understand.
  - _a_a_a_ 3y ago
    Oh get real. I have a background in this. Lambda notation, Hoare notation (I think), 'standard' logic notation. Don't talk rubbish about 'look it up'. You need a degree to get this. Not a metaphorical degree, the real thing. Edit - and a brain bigger than mine.
    - the_af 3y ago
      > Don't talk rubbish about 'look it up'. You need a degree to get this. Not a metaphorical degree, the real thing. You really don't need a degree. The Curry-Howard isomorphism is taught in undergraduate CS courses, to students who are simultaneously being introduced to lambda calculus. While I wouldn't say it's trivial, it's not rocket science either. Most students get it and pass the exams.
    - fooker 3y ago
      It's an introductory CS concept, requiring a degree would make things a bit circular...
  - SilasX 3y ago
    Under that constraint, what wouldn't count as an accessible exposition?
    - vkou 3y ago
      "I have a truly marvelous demonstration of this proposition which this margin is too narrow to contain."
      - SilasX 3y ago
        So the only way for an explanation not to be accessible is to not provide it? Okay.
        0003 3y ago
        In the spirit of the topic, I ran the truth tables you got yourself a valid argument. Feel free to pin this to the top.
    - fooker 3y ago
      Something involving implicit knowledge and conventions that is not spelled out.
  - user3939382 3y ago
    It doesn’t matter what you think is accessible, it only matters if the person trying to access it thinks it’s accessible. I don’t.
    - the_af 3y ago
      If you can learn how to program, you can learn how to understand this. You first must learn the notation, just as when you learned "def", or "func", or "[x for x in ...]", or "int main() { ... }", or whatever your favorite language's notation is. "Accessible" doesn't necessarily mean "with just knowledge of English, you can jump to this example and immediately understand what it means". Some work is always required; accessible just means this work is not too hard. For example, Python's notation has been occasionally described as "accessible", yet I wouldn't expect my mum to immediately understand a non-trivial Python snippet (so no "print('hello')") without any previous explanations.
      - _a_a_a_ 3y ago
        Quiz: what is the opposite of patronising? Because that's what you're being. Not talking down to people but assuming more than is typical. You're clearly highly intelligent, evidently more so than I am. Additionally my mind doesn't work like yours, I'm not an abstract thinker. Plonk stuff like this in front of me and I can decipher it eventually, if I can get some clear statement of the notation and its semantics anyway, and there is stuff in there I'm not familiar with. Most people aren't abstract thinkers. They are motivated by practical concerns. I spent an enormous amount of time reading up on stuff like this and I really can't see the value to it to me as a programmer. It's deeply frustrating because I know it has value, but I just can't use it. It's interesting, I know it's useful, but I can't use it. Please allow that other people think differently and are motivated differently, and don't assume that what's easy for you is for them. I wish I had your cranium.
        zozbot234 3y ago
        > Most people aren't abstract thinkers. They are motivated by practical concerns. Abstract thinking is motivated by practical concerns, namely being able to think comfortably about larger problems without being limited by one's capability for complex reasoning. Most people don't do it because they aren't used to, or they have never been taught how.
  - seanhunter 3y ago
    By that definition "Baby Rudin"[1] is an accessible introduction to analysis as long as you're willing to look up what you don't understand (ie everything probably the first time) in some other source. [1] https://maa.org/press/maa-reviews/principles-of-mathematical-analysis https://maa.org/press/maa-reviews/principles-of-mathematical...
    - fooker 3y ago
      Rudin is not accessible if you're just looking up things. But it is if you have someone to explain stuff when you get stuff. This one doesn't need that.
- qsort 3y ago
  It's accessible to anybody with any experience programming and who is willing to pay attention. You are just taking a formula out of context, omitting the plain English explanation that comes before it, and pretending it's some kind of alien math. It's not scary at all, in fact it's very simple. Let's do this in Python. First, write a function that curries: def curry(f): def g(x): def h(y): return f(x, y) return h return g my_func = lambda x, y: 10 * x + y curried = curry(my_func) print(curried(5)(3)) # output: 53 Now, let's type it in such a way that mypy --strict won't complain: from typing import TypeVar, Callable A = TypeVar('A') B = TypeVar('B') C = TypeVar('C') def curry(f: Callable[[A, B], C]) -> Callable[[A], Callable[[B], C]]: def g(x: A) -> Callable[[B], C]: def h(y: B) -> C: return f(x, y) return h return g What's the type of curry? Let's hover our cursor over the function name, and lo and behold: Callable[[Callable[[A, B], C]], Callable[[A], Callable[[B], C]]] That's it. That's all it's saying.
  - _a_a_a_ 3y ago
    > You are just taking a formula out of context, omitting the plain English explanation that comes before it, which, this? "We saw earlier in the course that we can curry a function. That is, given a function of type (τ 1 ×τ 2 ) → τ 3 , we can give a function of type τ 1 → τ 2 → τ 3" That helps no-one unless you have some serious hand-holding. I know the type of curry, I've written curry/bind/whateveer in C#, scala, JS and likely others. I have a background in this. It's not 'accessible' to mere mortals and even I'm not familiar with some of the notation here. Stop pretending it's just laziness on other people's part. (oh yeah, did I forget to put constructive logic in my list above? Brouwer's intuitionism? FFS get real, I never even heard of that until a few years ago)
    - zozbot234 3y ago
      It is accessible if you know a few bits of syntax, such as → being right-associative so τ1 → τ2 → τ3 means τ1 → (τ2 → τ3). And others such as "f: X → Y declares f as a function from X's to Y's." which you can find in any math textbook. The point of using such a terse notation rather than faffing around with Callable[…] is to make it possible to work with larger examples without getting bogged down in the verbiage. It's why we use symbols to solve equations in K-12 math.
- mrkeen 3y ago
  It's just the 'mathy' type-setting which is hard to read. Types and terms are in the same font & colour and they're on the same line. To paraphrase: You can curry a function (supply its arguments one-by-one instead of all at once). You have: f(x, y) which has type (τ1 x τ2) -> τ3 You want: f x y which has type τ1 -> τ2 -> τ3 Here's a function which converts what you have to what you want: λx. λy. f(x, y) It has type: ((τ1 × τ2) → τ3) → (τ1 → τ2 → τ3) This type "Curry-Howard"s to the logical formula: (A ∧ B ⇒ C) ⇒ (A ⇒ (B ⇒ C)) Since this logical formula is a tautology, the above conversion function preserves the meaning of the function it converts.
  - _a_a_a_ 3y ago
    > (A ∧ B ⇒ C) ⇒ (A ⇒ (B ⇒ C)) > Since this logical formula is a tautology You forgot to say 'obviously' /s
- housecarpenter 3y ago
  I would interpret "accessible" here as meaning relatively accessible compared to what it could be. The underlying concept is inherently difficult, and so it will always be somewhat inaccessible, but within the space of all possible explanations, I would agree that it's on the more accessible end rather than the less.
xelxebar 3y ago
Nifty. That was a nice 4-page exposé of the correspondence. There are no general proofs, but the correspondence between notations is very suggestive and invokes interesting intuitions, I think. The example derivations with the uncurry example are quite fun to work through. The paragraph about continuations corresponding to double negation is also super neat! Now I just wish there were something similar for the missing category theory third of the trinitary mentioned in another comment.

by qsort 3y ago

_a_a_a_ 3y ago

Accessible for who, do you mean? That is in no way 'accessible' without solid exposure to quite a lot of discrete maths (which I have and it's still hard going). λf :(τ 1 × τ 2 ) → τ 3 .λx:τ 1 .λy:τ 2 .f (x,y) has type ((τ 1 × τ 2 ) → τ 3 ) → (τ 1 → τ 2 → τ 3 ). Yeah, that's accessible.

fooker 3y ago
Seems accessible, if you're willing to look up what what you don't understand.
- _a_a_a_ 3y ago
  Oh get real. I have a background in this. Lambda notation, Hoare notation (I think), 'standard' logic notation. Don't talk rubbish about 'look it up'. You need a degree to get this. Not a metaphorical degree, the real thing. Edit - and a brain bigger than mine.
  - the_af 3y ago
    > Don't talk rubbish about 'look it up'. You need a degree to get this. Not a metaphorical degree, the real thing. You really don't need a degree. The Curry-Howard isomorphism is taught in undergraduate CS courses, to students who are simultaneously being introduced to lambda calculus. While I wouldn't say it's trivial, it's not rocket science either. Most students get it and pass the exams.
  - fooker 3y ago
    It's an introductory CS concept, requiring a degree would make things a bit circular...
- SilasX 3y ago
  Under that constraint, what wouldn't count as an accessible exposition?
  - vkou 3y ago
    "I have a truly marvelous demonstration of this proposition which this margin is too narrow to contain."
    - SilasX 3y ago
      So the only way for an explanation not to be accessible is to not provide it? Okay.
      - 0003 3y ago
        In the spirit of the topic, I ran the truth tables you got yourself a valid argument. Feel free to pin this to the top.
  - fooker 3y ago
    Something involving implicit knowledge and conventions that is not spelled out.
- user3939382 3y ago
  It doesn’t matter what you think is accessible, it only matters if the person trying to access it thinks it’s accessible. I don’t.
  - the_af 3y ago
    If you can learn how to program, you can learn how to understand this. You first must learn the notation, just as when you learned "def", or "func", or "[x for x in ...]", or "int main() { ... }", or whatever your favorite language's notation is. "Accessible" doesn't necessarily mean "with just knowledge of English, you can jump to this example and immediately understand what it means". Some work is always required; accessible just means this work is not too hard. For example, Python's notation has been occasionally described as "accessible", yet I wouldn't expect my mum to immediately understand a non-trivial Python snippet (so no "print('hello')") without any previous explanations.
    - _a_a_a_ 3y ago
      Quiz: what is the opposite of patronising? Because that's what you're being. Not talking down to people but assuming more than is typical. You're clearly highly intelligent, evidently more so than I am. Additionally my mind doesn't work like yours, I'm not an abstract thinker. Plonk stuff like this in front of me and I can decipher it eventually, if I can get some clear statement of the notation and its semantics anyway, and there is stuff in there I'm not familiar with. Most people aren't abstract thinkers. They are motivated by practical concerns. I spent an enormous amount of time reading up on stuff like this and I really can't see the value to it to me as a programmer. It's deeply frustrating because I know it has value, but I just can't use it. It's interesting, I know it's useful, but I can't use it. Please allow that other people think differently and are motivated differently, and don't assume that what's easy for you is for them. I wish I had your cranium.
      - zozbot234 3y ago
        > Most people aren't abstract thinkers. They are motivated by practical concerns. Abstract thinking is motivated by practical concerns, namely being able to think comfortably about larger problems without being limited by one's capability for complex reasoning. Most people don't do it because they aren't used to, or they have never been taught how.
- seanhunter 3y ago
  By that definition "Baby Rudin"[1] is an accessible introduction to analysis as long as you're willing to look up what you don't understand (ie everything probably the first time) in some other source. [1] https://maa.org/press/maa-reviews/principles-of-mathematical-analysis https://maa.org/press/maa-reviews/principles-of-mathematical...
  - fooker 3y ago
    Rudin is not accessible if you're just looking up things. But it is if you have someone to explain stuff when you get stuff. This one doesn't need that.
qsort 3y ago
It's accessible to anybody with any experience programming and who is willing to pay attention. You are just taking a formula out of context, omitting the plain English explanation that comes before it, and pretending it's some kind of alien math. It's not scary at all, in fact it's very simple. Let's do this in Python. First, write a function that curries: def curry(f): def g(x): def h(y): return f(x, y) return h return g my_func = lambda x, y: 10 * x + y curried = curry(my_func) print(curried(5)(3)) # output: 53 Now, let's type it in such a way that mypy --strict won't complain: from typing import TypeVar, Callable A = TypeVar('A') B = TypeVar('B') C = TypeVar('C') def curry(f: Callable[[A, B], C]) -> Callable[[A], Callable[[B], C]]: def g(x: A) -> Callable[[B], C]: def h(y: B) -> C: return f(x, y) return h return g What's the type of curry? Let's hover our cursor over the function name, and lo and behold: Callable[[Callable[[A, B], C]], Callable[[A], Callable[[B], C]]] That's it. That's all it's saying.
- _a_a_a_ 3y ago
  > You are just taking a formula out of context, omitting the plain English explanation that comes before it, which, this? "We saw earlier in the course that we can curry a function. That is, given a function of type (τ 1 ×τ 2 ) → τ 3 , we can give a function of type τ 1 → τ 2 → τ 3" That helps no-one unless you have some serious hand-holding. I know the type of curry, I've written curry/bind/whateveer in C#, scala, JS and likely others. I have a background in this. It's not 'accessible' to mere mortals and even I'm not familiar with some of the notation here. Stop pretending it's just laziness on other people's part. (oh yeah, did I forget to put constructive logic in my list above? Brouwer's intuitionism? FFS get real, I never even heard of that until a few years ago)
  - zozbot234 3y ago
    It is accessible if you know a few bits of syntax, such as → being right-associative so τ1 → τ2 → τ3 means τ1 → (τ2 → τ3). And others such as "f: X → Y declares f as a function from X's to Y's." which you can find in any math textbook. The point of using such a terse notation rather than faffing around with Callable[…] is to make it possible to work with larger examples without getting bogged down in the verbiage. It's why we use symbols to solve equations in K-12 math.
mrkeen 3y ago
It's just the 'mathy' type-setting which is hard to read. Types and terms are in the same font & colour and they're on the same line. To paraphrase: You can curry a function (supply its arguments one-by-one instead of all at once). You have: f(x, y) which has type (τ1 x τ2) -> τ3 You want: f x y which has type τ1 -> τ2 -> τ3 Here's a function which converts what you have to what you want: λx. λy. f(x, y) It has type: ((τ1 × τ2) → τ3) → (τ1 → τ2 → τ3) This type "Curry-Howard"s to the logical formula: (A ∧ B ⇒ C) ⇒ (A ⇒ (B ⇒ C)) Since this logical formula is a tautology, the above conversion function preserves the meaning of the function it converts.
- _a_a_a_ 3y ago
  > (A ∧ B ⇒ C) ⇒ (A ⇒ (B ⇒ C)) > Since this logical formula is a tautology You forgot to say 'obviously' /s
housecarpenter 3y ago
I would interpret "accessible" here as meaning relatively accessible compared to what it could be. The underlying concept is inherently difficult, and so it will always be somewhat inaccessible, but within the space of all possible explanations, I would agree that it's on the more accessible end rather than the less.

xelxebar 3y ago

Nifty. That was a nice 4-page exposé of the correspondence. There are no general proofs, but the correspondence between notations is very suggestive and invokes interesting intuitions, I think. The example derivations with the uncurry example are quite fun to work through. The paragraph about continuations corresponding to double negation is also super neat! Now I just wish there were something similar for the missing category theory third of the trinitary mentioned in another comment.