Hacker Newsnew | comments | show | ask | jobs | submit | login

"Closed manifold" typically means a compact manifold without boundary (see e.g., http://en.wikipedia.org/wiki/Closed_manifold).

reply


Ah, thanks!

reply


> Some of the computer scientists, however, instinctively interpreted the statement “Let x be such that P(x)” as a variable declaration. This led them to give an “incorrect” answer to a question

"Let x be such that P(x)" is something like a variable declaration. It's the introduction of an argument to a function (think "function(x){ ... }"). I think the real conceptual problem lies in the fact that many mainstream programming languages allow subversion of the type system by allowing "uninitialized" variables, so that every type is automatically inhabited.

There is also the fact that a mathematician may just want some "x such that P(x)" rather than introducing a generic one, which I think the author mentions.

-----


Certainly physics is not a branch of mathematics, but it isn't uncommon for papers in theoretical physics to essentially be math papers with an eye toward applications to some physical notions, and physicists do come up with new math.

-----


It's true that Turing complete languages are (almost by definition) equivalent for writing programs of type "Nat -> Nat". However, things are not so simple at other types and it turns out there is actually something of a spectrum of computability. Andrej Bauer has a nice post on such things here: http://math.andrej.com/2011/07/27/definability-and-extension...

-----


> Natural transformations between functors gives you parametricity and "theorems for free"

Could you elaborate? This is something everyone always talks about but I've never really seen a proof/precise statement.

-----


The "Theorems for free" paper is here: http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf ( I guess is the most precise you can get :) )

-----


Lawvere and Schanuel's excellent "Conceptual Mathematics" has plenty of exercises, and the book is insanely approachable while still teaching a good amount (it's chock full of examples).

Mac Lane (Categories for the Working Mathematician) also has exercises and I think the ones from the first few chapters aren't so hard.

-----


Here's a reasonably well-cited article rebutting these claims.

http://www.jpurol.com/article/S1477-5131%2809%2900349-0/abst...

And a free version which seems similar http://www.harryfisch.com/pdf/Declining%20Worldwide%20Sperm%...

-----


The first article, the abstract, refers to hypospadia, a urethral defect. The second, full text article, is the one directly addressing the article above.

-----


More than addresses it - smashes it out of the park! I wonder what has happened to Elizabeth Carlsen?

-----


You should definitely check out Brent Yorgey's diagrams package (see examples here http://projects.haskell.org/diagrams/gallery.html) which is a declarative drawing library. Graphics are described in an essentially "mathematical" way, and as you can see, many of the examples come from mathematics.

-----


Could you explain what you mean by this? I'd say using monads is way more "in-your-face" in OCaml since you have to explicitly say which monad you're using (via opening a module or what have you) and there's no do-notation.

Perhaps you mean that one doesn't need monads as much in OCaml since it's impure and so they aren't required to manage state?

-----


To be this is a community factor rather than a technical one. You can't talk to a Haskell person for five minutes before they're trying to explain monads to you, (often whether you already understand them or not) and to an OCaml programmer they're just another tool.

-----


I'm fairly sure it's a complete technical one. Haskell's purity enforces effect typing, OCaml doesn't. You can just get more done without monads in OCaml and you have to have built-in syntax for sequencing (e.g. ;).

-----


You're probably talking to the wrong Haskell people :-P

-----


See this page (https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usag...) for info on erasure. Unused proof values or indices in data types used for static checking are erased at compile time via usage analysis (if you don't use it in the RHS of a function definition, it gets erased).

If you want to ensure that the indices of your data type or arguments to your function are erased, you can use the new dot notation. E.g., if you give a function called "half" the following type

  half : (n : Nat) -> .(pf : Even n) -> Nat
then the compiler will complain if the proof argument is actually used.

-----

More

Guidelines | FAQ | Support | API | Lists | Bookmarklet | DMCA | Y Combinator | Apply | Contact

Search: