Live data from Hacker News

Seemingly impossible functional programs (2007)

math.andrej.com

41–46 of 46 posts

Re: Seemingly impossible functional programs (2007)

#41

> 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.

A mathematician that has only used a type theory like Coq or Agda and never Haskell.

Re: Seemingly impossible functional programs (2007)

#43

I find this very interesting, but I'm unable to understand it, so the result still seems impossible to me. Can someone explain how find works if the predicate is something like: return true if and only if every other bit is 1

The trick is that your predicate can’t be implemented in Haskell, because the predicate itself requires looking at infinitely many elements.

Re: Seemingly impossible functional programs (2007)

#44

I find this very interesting, but I'm unable to understand it, so the result still seems impossible to me. Can someone explain how find works if the predicate is something like: return true if and only if every other bit is 1

if a predicate depends on finitely many bits then you can exhaustively check whether it is total by enumerating all of it's possible inputs

Re: Seemingly impossible functional programs (2007)

#45
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?

p is a predicate, which is a function mapping elements of some type to true/false (booleans). A total function is a function which is defined for all possible inputs. So a total predicate is a function that maps all possible inputs to either true or false.

For real numbers, f(x)=x² is a total function, but g(x)=√x is not, because g is undefined for x<0

Re: Seemingly impossible functional programs (2007)

#46
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.

Yeah, math is riddled with ungoogleables, for example, graph can mean network of nodes or function plot depending on context
Post reply on HN