maxiepoo

15 ms·

31.
by maxiepoo 5y ago
The analogy goes much further if you take it as "open set" =~ "semidecidable property", i.e., you can determine in finite time that something is in the subset, but may not halt on an input that is not in the subset. A cl
32.
by maxiepoo 5y ago
I think it's been popularized by the NBA fandom and the incessant Lebron James vs Michael Jordan debates.
33.
by maxiepoo 5y ago
Eh, Nepo's good record against Magnus comes mostly from when they were both playing in youth tournaments. He hasn't beaten Magnus in many years.
34.
by maxiepoo 5y ago
A mathematician that has only used a type theory like Coq or Agda and never Haskell.
35.
by maxiepoo 5y ago
Exactly, Haskell's "do" notation is essentially defined as a built-in macro, so if you ever want to use "do" notation in a language that doesn't have it built-in you will need to use macros. (Let-binding overlo
36.
by maxiepoo 5y ago
This won't be a very deep answer, but to connect with the original post, programming in CPS is more closely related to delimited continuations than call/cc is because the continuations are just ordinary functions in the host langu
37.
by maxiepoo 6y ago
Yes, this is well known, good catch! If you read McBride's paper "Clowns to the Left of Me, Jokers to the Right" ( https://www.cis.upenn.edu/~cis39903/static/clowns.pdf ) is exactly about systematical
38.
by maxiepoo 6y ago
Finally some good news...
39.
by maxiepoo 6y ago
The idea of polarity comes from the category theoretic notion of a universal property. Nice types have introduction and elimination rules but for negative types the introduction rule is "reversible" whereas for positive types the
40.
by maxiepoo 6y ago
These pictures, especially the second one, really remind me of Jonathan Blow's puzzle game "The Witness" which I highly recommend. Very appropriate since part of the game is predicated on how playing all of these abstract puz
41.
by maxiepoo 6y ago
The Power Broker: Robert Moses and the Fall of New York by Robert Caro. Enormous and incredibly informative about politics, city planning and public relations.
42.
by maxiepoo 6y ago
I think you and OP are talking about different things because the term "intuitionist" has been used for both the philosophy that EJ Brouwer espoused (which matches what OP said) and the large field of constructive mathematics that
43.
by maxiepoo 7y ago
It seems the consequences of 'Sokal Squared' are because the papers contained falsified data, which is very different from what Dr. Bik is doing here.
44.
by maxiepoo 7y ago
By one-shot you mean dynamically enforced, right? I.e. if you invoke it a second time it will raise an exception?
45.
by maxiepoo 7y ago
Constructive mathematics is alive and well for 2 reasons. 1. The type theorists/homotopy theorists that are exploring homotopy/cubical type theory as a foundational approach. 2. The objective fact that in general the internal lang
46.
by maxiepoo 7y ago
The "motto" (if it can be called that) is not "avoid success", it's "avoid 'success at all costs'" which makes the sentiment clearer: increasing adoption should never be a priority over principle
47.
by maxiepoo 7y ago
Just to make it clear, the authors of that paper (including myself) are all to some extent Racket developers. Some big improvements have been made but there are still pathological cases. For the latest published on this see this paper: htt
48.
by maxiepoo 8y ago
I highly doubt that you can get a paper at any respectable conference or journal showing something is Turing Complete.
49.
by maxiepoo 8y ago
The Topos theory example is completely wrong though? > For example, if E is the topos of sets, then the slice category is the category of pointed sets: the objects are then sets together with a function selecting a point as a “base point
50.
by maxiepoo 8y ago
Really? Then as written it's very misleading "led to some bug fixes in Racket’s implementation of letrec and set!."
51.
by maxiepoo 8y ago
Removing an unnecessary dependency is a good analogy. From a Curry-Howard perspective, intuitionistic proofs correspond to programs without side-effects, and classical proofs correspond to programs that can use continuation effects (for the
52.
by maxiepoo 8y ago
Does ReasonML have ML's nice module/functor system? That would be a huge advantage over elm.
53.
by maxiepoo 9y ago
Ah whoops, I meant to say that the definitions of most of the casts are uniquely determined by soundness (i.e. beta, eta) and graduality (i.e. being an equipment).
54.
by maxiepoo 9y ago
Author of the blog post here. This is a great overview of internal categories and profunctors. A couple comments 1. I would say the primary application is to proving that certain casts (function cast, etc.) are the primary result of the pap
55.
by maxiepoo 9y ago
Maybe but this is a mathematician's blog, so perhaps you are not the intended audience.
56.
by maxiepoo 9y ago
Yes: http://calculist.org/blog/2012/04/17/homoiconicity-isnt-the-...
57.
by maxiepoo 9y ago
Where are you from that this is true? England? I think very few universities in the USA use Haskell in intro classes.
58.
by maxiepoo 9y ago
As someone that does not understand the rules of Magic, how do they get around the fact that a Turing machine requires infinite memory? Presumably a particular game of Magic has a finite set of cards and probably states too?
59.
by maxiepoo 9y ago
Yeah this kind of nullifies the pull quote > If Newton had known about such functions, he would have never created calculus. since Newton did use infinitesimals in his reasoning.
60.
by maxiepoo 9y ago
Ah yes, I remember seeing an interaction that was probably yours, tried to find it for my comment, but never did.

More ›