anfelor

8 ms·

31.
by anfelor 4y ago
Ocaml 5 and Koka ( https://koka-lang.github.io/koka/doc/index.html ) can get quite close to the speed of C...
32.
by anfelor 5y ago
I agree with you that this is really about the foundations of algebraic topology, but what makes you say that these are not the foundations of mathematics? In the community of computer-aided formalization, a lot of interest in modern type t
33.
by anfelor 5y ago
This is a response to the recent "Geniuses of the past were aristocratically tutored", discussed at https://news.ycombinator.com/item?id=30698624
34.
by anfelor 5y ago
If you don't know it already, you might be interested in 'Dirk Gently's Holistic Detective Agency' by Douglas Adams and/or the funnier second part 'The Long Dark Tea-Time of the Soul'.
35.
by anfelor 5y ago
You might be interested in the FBIP versions of Okasakis datastructures in https://github.com/koka-lang/koka/tree/master/test/perf/sets Most of them only have 'insert' and 'looku
36.
by anfelor 5y ago
> Also I think you mean "Catholic", not "catholic". Wow, I sometimes like to think that I speak English at a native level and then I learn about something like this.. Catholic: relating to the Catholic church catholic
37.
by anfelor 5y ago
My inner voice helps me tremendously while working on a proof or an algorithm: I say the individual steps in my head and then I remember them better. I can even do this with writing blog posts, but then when I get to the keyboard I still kn
38.
by anfelor 5y ago
You are right, a decoding function is needed. The decoding for my given encoding function is not computable because you need to look at all elements of the sequence to see if the rest are the padded zeros or part of the number (because ther
39.
by anfelor 5y ago
This seems like little more than a parlor trick. First, a true "exhaustive search" is actually impossible. The cantor space is uncountable (which can be seen by prepending '0.' before every binary sequence which gives th
40.
by anfelor 5y ago
Another example not covered on the article is tail call optimisation. GCC is not very good at it and manually adding it using goto can sometimes speed code up by ~20%. Very useful when writing down a complex recursive algorithm that you can
41.
by anfelor 5y ago
If you want to study category theory with people online, I recommend the Zulip Channel: https://categorytheory.zulipchat.com/ (you can DM me for an invite). Still, I don't understand how this is in anyway related to &q
42.
by anfelor 5y ago
The Readme defines: // Data NonEmpty = | New a (NonEmpty a) NonEmpty |A :: ~ * ~> * => {(list A) :: |new}. // A list non-empty is list only with new constructor The haskell datatype reads like a co-i
43.
by anfelor 5y ago
Daan is employed full-time at MS Research and gets to spend this time on Koka (when he is not writing conference papers). There is currently no further funding or deployment of Koka within Microsoft that I know of (unlike mimalloc which see
44.
by anfelor 5y ago
No, that seems wrong. Its currently only Daan working on this, but as you can see the last commit to 'master' was 7 days ago and the last commit to 'dev' yesterday...
45.
by anfelor 5y ago
Yes, I am currently writing a masters thesis about it! It is a "research language that [is] currently under heavy development" as the README says so I don't recommend using it for anything other than a research/toy proje
46.
by anfelor 5y ago
Since Pen claims to be inspired by Koka, I would hope that they eventually implement Perceus reference counting [0], which (partially) solves the problem of too many allocations. The idea is that with immutable datastructures you often free
47.
by anfelor 5y ago
If you ask people what the capitals of Turkey and Australia are, you might hear Istanbul and Sydney surprisingly often. There seems to be some probabilistic inference in our brain that the largest city in a country should also be the capita
48.
by anfelor 5y ago
The funny symbol is called sqsubseteq and you can find that out by drawing it here: https://detexify.kirelabs.org/classify.html But I agree that there needs to be a way to type latex Symbols quicker. The Lean Community did
49.
by anfelor 5y ago
> But fortunately there are elections in September. Laschet has time and again defended lignite ("Braunkohle" in german) and will probably become the next chancellor. Write an email to your local green party branch and ask how
50.
by anfelor 5y ago
Also, one wonders if EU states would have been better at closing their borders at the start of the pandemic (like Australia or New Zealand did) if it wasn't for the EU. Maybe not, because there are always big trade networks on a landma
51.
by anfelor 5y ago
The scary thing about this is that many people have images that look like child porn at home: Family photos of naked grandchildren playing at the sea or in the mud, as well as sexting between consenting teenagers. There is no way automatic
52.
by anfelor 5y ago
I did math in undergrad and I am now going the computer science PhD route. I think basic math really helps and some fields like combinatorial optimizations are good as well, but most of mathematics is only useful for pure mathematicians and
53.
by anfelor 5y ago
Yes, there is no concrete intervention that the CCP did. Still, a supervisor broke off their contact with a promising student based on either the fear of retribution or personal feelings of nationalism. That culture is the product of CCP ce
54.
by anfelor 5y ago
But unofficial relationships matter in science. For example, I am currently doing an unpaid internship in the hopes of getting a paper out of it. If the professor cancelled it, I might be left with nothing to show for months of hard work, s
55.
by anfelor 5y ago
"The authors of the study also performed an in-depth laboratory analysis of 67 telephones included in this list. The investigation revealed that more than half of them, 37 phones, found evidence of the activity of the Israeli Spyware&q
56.
by anfelor 5y ago
The CDU had a rough period where they were accused of mismanaging several important parts of the covid strategy (including giving contracts for pursuing masks to their cronies) and they couldn't figure out who should become their candi
57.
by anfelor 5y ago
Not a lawyer, but in that case it seemed to be a factor that turnitin was transformative, because it never sold the texts to others and thus didn't reduce the market value of them. But that wouldn't apply to copilot which might re
58.
by anfelor 5y ago
They don't do that it seems. In the footnotes of https://docs.github.com/en/github/copilot/research-recitatio... they mention two repositories from the training set none of which specify a license.