Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Seemingly impossible functional programs (2007)

math.andrej.com

Post reply on HN
Print view View original

11–20 of 46 posts

Re: Seemingly impossible functional programs (2007)

#11

Post by ZoltanAK2 »

quocanh wrote: post #9

Can someone explain to me in plain English what this is? I looked up Cantor Sets so I have a vague understanding... but there are many things I don't understand. Like what does it mean to have a sequence with a bit appended to a Cantor Set? Why is that a Cantor Set? What the heck is a total p - is it a function?

Cantor space is just the space formed by infinite binary sequences, that is sequences which assumes only the values 0 or 1.

Considered as a topological space, Cantor space happens to have the same structure as the Cantor set, a highly disconnected subset of the real numbers that has some at-first-unintuitive properties.

But you don't have to understand, or even worry about this correspondence to grasp what's going on with seemingly impossible functional programs. Thinking about Cantor space as "the type of infinite binary sequences" is good enough.

Re: Seemingly impossible functional programs (2007)

#12

Post by lmm »

theamk wrote: post #4

Maybe I am not a enough of a functional programmer, but I don't see what's impossible here? Any symbolic algebra system (like Wolfram Mathematica) can do such derivations, and much more. Sure, this is interesting, but in the sense of "look at this emergent behavior -- such a simple system can do unusually complex result", rather than "wow! no one could do such things with computer before"

You can do symbolic algebra on symbolic function definitions. What's interesting about this stuff is that it works for "real" functions - plain Haskell functions that we can't inspect the definition of, just call in the normal way (there's no macros or monkeypatching or anything like that going on). It's like being able to use numerical methods but still somehow solve everything exactly.

Re: Seemingly impossible functional programs (2007)

#13

Post by bckr »

mycroftiv wrote: post #3

I found this post and the code and math so fascinating it changed my life when I found it three years ago. I did not previously understand the capability of computers to work with the abstract logic of infinite sets in a meaningful way and it led me into the world of formalization of mathematics in the dependently typed programming language Agda, which is one of the current activities of the mathematician (Martin Esc…

Can you mention some downstream effects such that your life was changed?

Re: Seemingly impossible functional programs (2007)

#16

Post by steego »

ajkjk wrote: post #6
bmc7505 wrote: post #5

Earlier quoted context omitted.

One of the authors of this work apparently now works on supercompilers at Meta and open sourced some nice tools for equivalence checking based on graph rewriting [1] and constructive type theory [2]. If you're interested in that kind of thing I would recommend checking out his work: [1]: https://github.com/ilya-klyuchnikov/mrsc [2]: https://github.com/ilya-klyuchnikov/ttlite

Are we already calling it 'Meta' unironically?

To be fair, people who work on supercompilers have been in the meta space long before it was ironic.

Re: Seemingly impossible functional programs (2007)

#17

Post by dan-robertson »

recursive wrote: post #15

> The Maybe type constructor is predefined by Haskell as [...] It's hard for me to imagine a reader that understands the rest of this jargon, presented without explanation, who does not know what `Maybe` is.

1. People often struggle to target the things they write well towards a specific group of people and that often leads to this sort of thing.

2. I think when I came across this when it was posted to hacker news 5-10 years ago, I didn’t know any Haskell or any ML language and I didn’t know the maths but the program was small enough and direct enough that I think I managed to puzzle through a lot of it just by trying to match the code to the type signature (though this isn’t really sufficient to get a good feel for what is going on)

Re: Seemingly impossible functional programs (2007)

#18

Post by rowanG077 »

ajkjk wrote: post #6
bmc7505 wrote: post #5

Earlier quoted context omitted.

One of the authors of this work apparently now works on supercompilers at Meta and open sourced some nice tools for equivalence checking based on graph rewriting [1] and constructive type theory [2]. If you're interested in that kind of thing I would recommend checking out his work: [1]: https://github.com/ilya-klyuchnikov/mrsc [2]: https://github.com/ilya-klyuchnikov/ttlite

Are we already calling it 'Meta' unironically?

Supercompilation has also been known as metacompilation for decades.

Re: Seemingly impossible functional programs (2007)

#19

Post by zvorygin »

quocanh wrote: post #9

Can someone explain to me in plain English what this is? I looked up Cantor Sets so I have a vague understanding... but there are many things I don't understand. Like what does it mean to have a sequence with a bit appended to a Cantor Set? Why is that a Cantor Set? What the heck is a total p - is it a function?

Thank you for asking this, I was having a devil of a time googling what "total" meant in this context.

Re: Seemingly impossible functional programs (2007)

#20

Post by gijvikvff »

bckr wrote: post #13
mycroftiv wrote: post #3

I found this post and the code and math so fascinating it changed my life when I found it three years ago. I did not previously understand the capability of computers to work with the abstract logic of infinite sets in a meaningful way and it led me into the world of formalization of mathematics in the dependently typed programming language Agda, which is one of the current activities of the mathematician (Martin Esc…

Can you mention some downstream effects such that your life was changed?

I think they just mean that they wouldn't necessarily have heard about or got into Agda otherwise.
Post reply on HN