fmap

13 ms·

121.
by fmap 9y ago
> I don't know why computer people's category theory always looks so foreign to me. Sometimes I feel like we're in completely different worlds with vaguely similar-looking language. Well, another way to think about it is t
122.
by fmap 9y ago
Nitpick, but the idea is even older, going back at least to Girard (1971) and Reynolds (1974). :) I don't know exactly what the problem is for Go. There are tradeoffs, e.g., just with the type system: impredicative, stratified or predi
123.
by fmap 9y ago
> For loops do not get the job done easily enough. There was a nice paper at this years POPL which (in my opinion) allows you to substantiate this claim. The paper is "Stream Fusion to Completeness", by Oleg Kiselyov, Aggelos B
124.
by fmap 9y ago
Regarding extraction in Coq, there's certicoq: http://www.cs.princeton.edu/~appel/certicoq/ Granted, there's a lot of engineering work left to do, but it's moving in the right direction.
125.
by fmap 9y ago
At the assembly level, we are always working with continuation passing style. Normal calls are implemented by pushing their "return address" on the stack and then jumping to it after the procedure has finished. Formally, this is e
126.
by fmap 9y ago
> IMO taking the compiler out of the trusted computing base is the way to go. That is the point of compiler verification after all. I'm biased here, but I think that another important point is to work out what the specification of a
127.
by fmap 9y ago
What I found after Googling is that there is a theorem by Sierpinski which shows that if we make an additional assumption about the cardinality of [R]^\omega, which seems to be approximately the same as the boolean prime ideal axiom, then t
128.
by fmap 9y ago
What do you mean? If ZF without choice shows that a statement P holds then certainly ZFC also proves the same statement. Do you mean that there is a consistent extension of ZF with the statement "There exists a surjection from R to P(R
129.
by fmap 9y ago
I was thinking about categorical probability theory or measure theory based on locales. Unfortunately there are (to the best of my knowledge) no textbooks or good writeups available for either, merely long lines of research papers. As said,
130.
by fmap 9y ago
One thing which the author of this essay gets right is that contemporary mathematics is a bit dogmatic when it comes to the logical foundations. We should be looking at the Banach-Tarski theorem as evidence that a particular logical framewo
131.
by fmap 9y ago
> In particular, one should abandon the dichotomy between conjecture and theorem. Wasn't that the status quo before the 20th century? It's strange to suggest that working with infinite (or rather, ideal) objects is stupid. The
132.
by fmap 9y ago
A large part of any scientists job is communicating results. The people you criticize may not be novelists, but they are certainly professionals when it comes to communicating technical knowledge. However, this knowledge is only communicate
133.
by fmap 9y ago
I agree with you in principle, but I think the problem is more one of scale than of complexity theory. Sure the clique problem is hard to approximate in arbitrary graphs, but the graphs that appear in social networks are far from arbitrary.
134.
by fmap 9y ago
The truth seems to be that we don't know what makes a good language. In academic research we have criteria for what makes a language expressive, and tools for analyzing existing languages and check if they allow for modular development
135.
by fmap 9y ago
And just to be clear, the use case where you are doing repeated lookups/traversals of a linked list is uncommon? If not, you could always go with a hybrid implementation, e.g., using a vector with a changelog and applying the modificat
136.
by fmap 9y ago
As others have pointed out, the current state of the IoT market is nothing short of crazy, e.g., regarding security, device ownership, and, ironically, connectivity. I wonder if this isn't a perfect time to finally monetize the mountai
137.
by fmap 10y ago
My point is that category theory is useful for discovering nice abstractions such as algebraic effects and handlers or Monads for that matter. It's like all math, just a clever way to write/solve problems... As for the semantics o
138.
by fmap 10y ago
You may want to talk to Andrej Bauer about that ;) Specifically, the semantics of Eff involve free Monads.
139.
by fmap 10y ago
I'm not sure about non-deterministic behavior without looking it up, but you can fix this example to be implementation defined, rather than undefined like this: #include <stdio.h> int postincrement(int *x) { int y = *x;
140.
by fmap 10y ago
Where do you study and which subject? In an ideal world, I would recommend people to go to university iff they want to do research level work. For everyone else, there should be on the job training and a highschool education which teaches y
141.
by fmap 10y ago
Any investment into this kind of technology is bound to have positive returns because it'll make neuroscience more effective. Right now computational neuroscience is using a lot of blunt instruments such as electrode arrays which are i
142.
by fmap 10y ago
You're right, maybe is equivalent to the type of lists with at most one element. There are however monad instances which are genuinely different. For example the state monad is defined as F(X) = S -> S*X I.e., a value of type
143.
by fmap 10y ago
What exactly are you trying to learn? Mathematical logic is a huge field in its own right, with plenty of topics that are of historical interest and a lot of active research areas. If you want to learn modern mathematical logic you're
144.
by fmap 10y ago
The elephant in the room is that programming in English would be a huge step backwards. Modern programming languages are all about scalable, modular abstractions. Natural language typically doesn't supply many sound abstractions. Every
145.
by fmap 10y ago
Your money was transferred to your account with 60% probability and donated to the Trump Foundation with 40% probability. Press escape or e to abort with 10% probability. So uhm... More seriously, what do you mean?
146.
by fmap 10y ago
Out of curiosity, which field are you working in precisely? In my experience (in type theory / programming languages), the main problem is that a lot of papers are just badly written. Good papers really do use precise language to be ea
147.
by fmap 10y ago
In my experience this is already being practiced. Maybe it's different in machine learning, but in type theory simpler explanations are well worth publishing and are published all the time even in high impact venues. As far as I can te
148.
by fmap 10y ago
This whole situation is ridiculous. I am working in a university and I have my own office. Turns out that employees are by far the most expensive part about doing research in computer science, and the cost of giving everyone their own offic
149.
by fmap 10y ago
Your criticism is spot on. If something like Distill existed for my own research area I would applaud it, but probably not use it because of time constraints. On the other hand, being able to write well and to create good interactive illust
150.
by fmap 10y ago
Turing gets more credit in popular culture, but academically Church is more influential. Just look at the list of Church's PhD students: http://www.genealogy.ams.org/id.php?id=8011 I have no clue why Turing became such

More ›