fmap

14 ms·

91.
by fmap 9y ago
Can you link to some documentation about how monads work in rust? Based on the sibling comment rust doesn't support higher-kinded types yet, so I'm interested in how you would encode this in rust.
92.
by fmap 9y ago
Great work and obscure enough that I'm sure one of the authors made the submission :) If so, here are a few things that I saw while glancing over the paper (I'll read the paper in detail later): - you might be interested in neel k
93.
by fmap 9y ago
And often we have functions which are only defined in an open neighborhood of zero, yet we still call them functions. That the set theoretic definition of "function" as a functional relation between sets is rarely useful isn'
94.
by fmap 9y ago
Traditionally, mathematicians have a pointlessly hard time when manipulating higher-order functions. This goes from inventing new names for higher-order functions (e.g., "funcational", "transformation"), to constantly us
95.
by fmap 9y ago
I like the slides and agree with the widening language gap. I have a few comments about the conclusions, though. > The UPenn dependently typed Haskell > program shows a great deal of promise and > is likely to manifest a decade bef
96.
by fmap 9y ago
Great post, let me just add one point: > The 21-century understanding is something like: there's no need for there to be "ultimate" foundations. The modern view is that there simply is no ultimate foundation. Large cardina
97.
by fmap 9y ago
I don't know, but Russel O'Connor got his PhD in 2008, the same year that type classes were introduced in Coq. There has been a lot of development on the Coq proof assistant since then. I don't imagine that working with Coq i
98.
by fmap 9y ago
There is an easy design choice - which Haskell didn't take - which would allow us to have transparent Identity functors, associative Compose and many others: Add a conversion rule to your language and don't eagerly expand definiti
99.
by fmap 9y ago
Even that is frequently misleading. Take the problem of finding a maximum independent set. You can show that if you manage to approximate this problem within any constant factor then P = NP. On the other hand, finding large independent sets
100.
by fmap 9y ago
I'm looking forward to reading this series! Based on the overview, I would call it "From design patterns to algebra", though. There's (in most cases) no reason to involve categories in a discussion of monoids/semigr
101.
by fmap 9y ago
I don't want to get into a philosophical debate here, but please don't overstate the meaning of mathematical theorems. For example, Gödel's incompleteness theorem is a technical result stating that certain definitions of &quo
102.
by fmap 9y ago
Why, we could always use emscripten to compile rustc to JavaScript and use that for bootstrapping! On a more serious note, ghc at least solved this problem by allowing you to compile Haskell to C (-fvia-C). Writing a naive C code generator
103.
by fmap 9y ago
Martin Löf's lectures on type theory are pretty much the clearest explanation of modern mathematical logic that you'll find anywhere. Some of the technical results turned out to be false, or at least needed more work, but the anal
104.
by fmap 9y ago
The code in the post is just used to migrate from an untyped interface to a typed one. Unless I'm missing something, there seems to be no mention of any missing features in postgres.
105.
by fmap 9y ago
Let me stress the "install once, and never again" part - this is why I'm using arch. It's the first (binary) distribution I tried that eight years down the line still works as well as the day I first installed it.
106.
by fmap 9y ago
F* is a great project and under very active development. Basically at every POPL you find papers with genuine improvements and simplifications to the core of F*. I don't know of any other language that's improving this rapidly.
107.
by fmap 9y ago
1) It will be very soon: http://www.cs.princeton.edu/~appel/certicoq/ CertiCoq is a formally verified compiler from Coq to assembly (using Compcerts backends), not just an extraction to Ocaml/Haskell/Sca
108.
by fmap 9y ago
Which is why you use mathematics to write formally verified software e.g. in Coq. :) This whole "move fast and break things" philosophy should be unacceptable, if you want people to trust in your new cryptocurrency/voting mac
109.
by fmap 9y ago
And 20 years later, this essay is still as relevant as the day it was written. I agree with pretty much everything that's in the essay, except for a few small points. > There is nothing wrong with keeping the functional notation for
110.
by fmap 9y ago
> I'm not sure what the RILE score is but that chart is worthless if you want to understand party alignment. Even if you somehow project every single point of discussion into one dimension, isn't this a weird axis? It seems lik
111.
by fmap 9y ago
And thus we want benchmarks that measure language performance, not the fastest way to compute Fibonacci numbers. The solution to the latter problem is the same in Python and Julia and consists of calling the assembly function in gmp... Juli
112.
by fmap 9y ago
It's also much more modern. To be perfectly honest, if you are not doing automated theorem proving you probably never need to know about things like first-order logic or classical logic. Alas, we teach first year students boolean algeb
113.
by fmap 9y ago
There are people who have thought about this, e.g., http://onlinelibrary.wiley.com/doi/10.1002/cpe.2939/full Personally I think it's a better idea to instrument your programs and count the number of memo
114.
by fmap 9y ago
Can you expand a little bit on that? It seems like we are talking about very small programs here with simple specifications. What are some common problems with reinforcement learning implementations? Is it really just that you can't ea
115.
by fmap 9y ago
Some people have mentioned parser generators, but so far nobody has mentioned Menhir ( http://gallium.inria.fr/~fpottier/menhir/ ). It's an LR(1) parser generator for OCaml and Coq with a lot of extremely inter
116.
by fmap 9y ago
Proof checking in dependent type theory is nonelementary. Of course, this is a completely artificial result with no real world consequences, but that's complexity theory for you...
117.
by fmap 9y ago
Unnerving is definitely the wrong word. If you want to be negative about it, this is just really good advertising to a tech savvy audience. I honestly just switched my VPN subscription over to PIA after reading this list...
118.
by fmap 9y ago
In a constructive metatheory, partiality is both a richer and more subtle concept than just adding option types everywhere. It's possible to model partiality correctly using e.g. quotient inductive types or countable choice ( https:&#
119.
by fmap 9y ago
I agree that doing category theory without homotopy type theory is working with one hand tied behind your back, but you have to realize that it is very different from textbook category theory. For instance, in HoTT you will find that the ca
120.
by fmap 9y ago
Many "open problems" in mathematics are not actually that interesting on their own. Take the Collatz conjecture: it's pretty much just the statement that a certain 3 line program terminates. In many cases such as this, it is

More ›