fmap

27 ms·

241.
by fmap 13y ago
Sorry if I wasn't clear about this, but you can embed classical mathematics in a type theory with univalence. If you look into the HoTT book, there is a chapter on set theory in type theory. The general form of excluded middle is incon
242.
by fmap 13y ago
You get a choice between univalence and excluded middle. The whole argument is that univalence is more useful in practice. Briefly, in Martin-Löf type theory equalities are very strong, but you do not have many tools for proving new equalit
243.
by fmap 13y ago
Since you are using the word "constructivism" so often, there is probably some sort of misunderstanding. Constructivism usually refers to the philosophical school of thought which rejects the axiom of excluded middle for fairly do
244.
by fmap 13y ago
That's actually what the people at Valve did (GDC 2013): https://developer.nvidia.com/sites/default/files/akamai/game... Performance improved as a result. The number they give is ~20%. The other nic
245.
by fmap 13y ago
For many machine learning problems you can find an equivalent problem which is convex. This seems to be the method of choice for dealing with things like Support Vector Machines. Many academics seem to dislike neural networks because of how
246.
by fmap 13y ago
It might be legally significant, but technically, there is no real difference. Given your social network, and training data consisting of the public members of a group you can use a semi-supervised learning algorithm to determine group memb
247.
by fmap 14y ago
This came up a few times already and it really isn't as wrong as it sounds. In Haskell all "side effects", which include memory stores, are in the IO monad (with a few exceptions). Writing a global variable is a side effect, because you cha
248.
by fmap 14y ago
Which "parameters" are you optimizing? Where did the corresponding model come from? When is a certain model even applicable? How do you implement the search procedure efficiently? Is the result actually meaningful? Can you expect future pre
249.
by fmap 14y ago
What is your point? There are optimizations for dynamic languages which are typically implemented as self modifying code (e.g. polymorphic inline caching) and need writable and executable pages. Without this you could still create writable
250.
by fmap 15y ago
The data structure is not better than a normal hash table. It is a different trade-off. For instance, you don't have to do a rehashing step, which is important for real time applications. Memory usage is also very deterministic at 2*(n-1) w
251.
by fmap 15y ago
That's a very good point. One way to circumvent this problem is to combine hashing and crit-bit trees, by constructing an unordered tree on the hash values of the set elements. The nice thing here is that if the hash function behaves like a
252.
by fmap 15y ago
Because of the way nested functions are implemented in GCC. If you call a nested function it has to know the frame address of the containing function in order to refer to its local variables. So if you take the address of such a function th
253.
by fmap 15y ago
You are right, the problem is undecidable in general. If the compiler is unsure whether a constraint is satisfied it will have to add a runtime check. This is similar to the behavior of array accesses in Java: If you access an invalid index
254.
by fmap 15y ago
I don't really know Microsoft's C compiler well enough to answer why your specific example fails so spectacularly, but I can make a guess: You are using inline assembly containing a computed jump instruction. In this situation the compiler
255.
by fmap 16y ago
I'm sure that someone has already mentioned this, but "A concurrent lambda-calculus with Futures" is a paper about AliceML. The problem is that the full syntax and semantics of StandardML contain a lot of features which are not very relevan
256.
by fmap 16y ago
I just read the original paper on samplesort, so this might not be the most up to date description, but the basic idea is as follows: - From an input sequence of length n, choose a random subsequence of length k. - Sort the subsequence. - P