fmap

23 ms·

61.
by fmap 8y ago
I don't think Conal makes any performance claims. The code is more parallel friendly because it doesn't involve global state, but for reverse mode AD you are not calculating derivatives as you go, but instead building up a functio
62.
by fmap 8y ago
Tactics are very useful when developing proofs rather than dependently typed programs (unless you are using very precise types, as is common in e.g. the Coq program package). The point is that in a proof you are usually not interested in th
63.
by fmap 8y ago
That's a really beautiful article! Using kinds to keep track of the concrete representation of a reference to a type (rather than the concrete representation of the type itself) is one of the real gems in GHCs design. However, one pr
64.
by fmap 8y ago
From a language design perspective it makes a lot of sense to add linear types to the language itself instead of using an encoding. Every encoding that I know of (such as region types encoded as monads, which is what I think the article wan
65.
by fmap 8y ago
You're right, the linearity restriction on the handler continuation is a peculiarity of multi-core OCaml and really more of an implementation detail. However, it is also true that you cannot encode, e.g., the continuation monad using (
66.
by fmap 8y ago
Well, it's a design choice that you can make for rational numbers and the restricted rationals with error values that we typically use in computer arithmetic. There's nothing wrong with it and as the article points out, even most
67.
by fmap 8y ago
In an ideal world you would be right, but that's not how the funding structures for academic research are set up. Think of a research lab as a company that gets paid per prototype and then has to market the concept for the next prototy
68.
by fmap 8y ago
I couldn't agree more, classical linear logic leads to surprisingly concise definitions. Your day job sounds fascinating, would you mind expanding on it a bit?
69.
by fmap 8y ago
One of the most amazing things about linear logic is that "classical" linear logic has a direct constructive reading. This has some interesting applications in constructive mathematics ( https://arxiv.org/abs/1
70.
by fmap 8y ago
Have you considered algebraic effects and handlers? If you add a linearity restriction on the return continuations (easily doable with the existing type system of Rust) their implementation is no harder than async/await, yet they can e
71.
by fmap 8y ago
Very nice! I wasn't aware of this algorithm at all, but it seems to be an early application of the lifting scheme to the DCT filter, 8 years before this method was introduced in the more general context of perfect reconstruction filter
72.
by fmap 8y ago
I'm in the same situation and it's really worrying. Deep learning is the method of choice for a number of concrete problems in vision, nlp, and some related disciplines. This is a great success story and worthy of attention. Anoth
73.
by fmap 8y ago
Yes! Functional or imperative programming makes no difference in his challenge problems. Tail recursive functions and loops are the same thing. Proving a loop correct using invariants and showing (partial) correctness for a tail recursive f
74.
by fmap 9y ago
> I agree with his rant about "CS departments' algorithmic analysis" failing to cover these real-world hardware issue. That was certainly true of my ~1997 undergrad CS course at the University of St Andrews, that was other
75.
by fmap 9y ago
> Universes in type theory correspond to inaccessible cardinals/Grothendieck universes in ZFC or object classifiers in elementary toposes, at least informally (I doubt there is published work here). There is quite a bit of published
76.
by fmap 9y ago
Let's say a language A is syntactic sugar over a language B if A can be translated to B by macro expansion. In that case, if B is sufficiently expressive, e.g., has first class functions, then in many cases A will be syntactic sugar ov
77.
by fmap 9y ago
Derek also gave a terrific keynote talk at POPL 2018 about the big picture: https://www.youtube.com/watch?v=8Xyk_dGcAwk
78.
by fmap 9y ago
I wonder how the techniques in this monograph stack up against optimization techniques on manifolds ( https://press.princeton.edu/absil ). Projected gradient descent seems like an approximation to steepest descent on a suitab
79.
by fmap 9y ago
I think the problems have more to do with economics. Creating new modern CPUs requires a lot of capital investment, making CPU vendors more risk averse. That's why modern CPUs by and large are not built to meet the demands of future so
80.
by fmap 9y ago
It's surprising that this was written in 2007. This article just perpetuates the tired old myth that there is something special about set theory... At its heart, set theory allows us to encode certain mathematical structures more or
81.
by fmap 9y ago
As far as I can tell, this is another piece of Amal Ahmed's high-level compiler verification project. The idea is that we don't have good tools to compare programs written in different languages, but these tools do exist so long a
82.
by fmap 9y ago
Do you know why that is the case? Nominal logic is usually presented as a sheaf model (i.e., as the internal language of the Schanuel topos), which models a constructive dependent type theory. Is there a problem when constructing a universe
83.
by fmap 9y ago
Whenever I read a post like this I have to wonder: was there as much resistance to writing tests for your code before that became common practice? Many of the arguments seem to apply to test driven development in the same way as they do to
84.
by fmap 9y ago
Consider a formula made up of only conjunctions and disjunctions and true/false. The first player tries to prove the formula and gets to move at every disjunction and is allowed to select which side of the disjunction to prove. The sec
85.
by fmap 9y ago
Theorem proving in intuitionistic logic is a two-player game and maps perfectly to the kind of Monte-Carlo Tree Search that's employed here. Except that it is far more difficult than Chess/Go/etc., since the branching factor
86.
by fmap 9y ago
This reminds me of Guarded Dependent Type theory, which isn't about stream programming, but has the same dimension analysis built into it. Guarded Dependent Type Theory (GDTT) has dimensions (called clocks), fby/sby (called later)
87.
by fmap 9y ago
You're right and looking at the example again I was completely wrong (shouldn't post without coffee). You can implement merging by writing append (+) in the correct way. As written, the code will always insert a new element every
88.
by fmap 9y ago
If you build such a list by consing new elements to the front, then it's insertion sort. If you build the list from a balanced binary tree it's merge sort. --- One important difference between this and quotient-inductive types is
89.
by fmap 9y ago
Ok, I did, so here's the answer in case anybody else is confused: The feature under discussion is "associated type constructors ". Rust already has associated types in traits (I didn't know that part and was confused),
90.
by fmap 9y ago
How does your implementation of associated types differ from the same feature in Haskell? In particular, why is this related to higher-kinded types? From what I remember from the theory, higher-kinded types lead to a genuinely more difficul

More ›