fmap

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 function that will calculate the derivatives at the end. That's the effectively the same operation as normal reverse mode AD.

Anyway, this discussion still misses the point. The actual program transformation that powers this paper is "compiling to categories", which is essentially making the computation graph explicit in a modular way. This is why you can go through the program in parallel afterwards - sharing and dependencies are already made explicit and there is no need to discover them as you go.

The main innovation of the paper is the factorization of different AD modes in terms of simple transformations on categories (e.g. the Yoneda embedding applied to forward AD gives you reverse AD). In this format it is easy to see that the methods are correct and easy to extend the code since there just isn't very much of it.

This is a great paper (and talks!). It's taking a messy algorithm and factorizing it into simple and reusable components.

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 the precise shape or computation behavior of the underlying proof term and this allows you to use far more aggressive automation than what you are doing with a typical macro. Likewise, you don't really want to see the proof term in the first place. Think about how long chains of equational reasoning are encoded in type theory - this is just noise that detracts from writing your proofs.

As for homoiconicity, I think this is orthogonal to a tactic language. Both lean's tactics and template Coq allow you to reify the syntax of the type theory in order to write automation tactics, but this is separate from the proof search aspects of tactics.

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 problem with it is that a polymorphic type, such as [] of kind "* -> *", or a function like map of type "forall a b. (a -> b) -> [a] -> [b]" really only works with boxed types. I always wondered how expensive it would be to monomorphize everything at the level of kinds and have what GHC calls levity polymorphism by default.

Languages like Rust and C++ always monomorphize everything and while this does get slow it is still not the exponential blowup that theory suggests. In fact, there is an ML compiler (MLton) which does the same and it is still not too bad. Doing it at the level of reference representation - which is where the generated code actually needs to change - should be much cheaper and definitely a practical default.

The only real problem I see is that you could in principle write code that does "kind polymorphic" recursion, which couldn't be compiled away. But that sounds seriously crazy and I see no reason to allow it in the first place...

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 wants to get at) leads to excessive sequentialization of code. This in turn leads to a lot of boilerplate (or crazy type inference problems) at compile time as well as suboptimal run time performance.

Linear types are the perfect example of a feature that belongs in the core language, or at the very least into a core intermediate language. They are expressive, in that you can encode a lot of high-level design ideas into linear types. You can compile a number of complicated front-end language features into a linearly typed intermediate language. Linear types have clear semantics and can even be used for improved code generation. If we ignore the messy question of how best to expose linear types in a high-level language then this is just an all around win-win situation...

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 (typed) algebraic effects. The precise relationship isn't that simple, but this paper:

  https://arxiv.org/abs/1610.09161

analyzes a particular setting in detail.

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 proof assistants use this definition for rational division.

For real numbers though, division by zero will always diverge or be undefined, no matter how you represent them. All computations on real numbers are continuous and there is no continuous extension of division which includes 0 in the domain of the denominator.

One can get around this by switching to projective reals (essentially reals extended with a new element that's both +infinity and -infinity). This is no longer totally ordered and has some other problems, but it's actually a great choice for a lot of numerical computations. Yet, I've never seen something like this implemented in hardware, aside from John Gustafson's unum concept.

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 prototype in an infinite loop. If you can't package up what you're doing into a sequence of small prototypes then you're not getting paid.

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?

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/1805.07518) and programming (http://homepages.inf.ed.ac.uk/wadler/papers/multiparty/multi...).

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 express many useful monadic abstractions.

...I saw this thread too late, hopefully you will still see this comment. I'm genuinely curious.

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 filters.

There's a great expository paper about these kinds of filter implementations by Daubechies and Sweldens in the general case: https://9p.io/who/wim/papers/factor/factor.pdf

Interestingly enough, Sweldens does not seem to cite Loeffler's paper, so it's likely that they came up with the same method independently of one another.

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. Another AI winter will just make it harder to secure funding for something that may well be a good solution to some problems.

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 function by (functional) induction are the same thing.

> 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 otherwise exemplary.

I counter with similarly anecdotal evidence from 2012. :)

While we had a normal "Algorithms and Datastructures" course that taught the classical theory, there was also a separate course about "Algorithm Engineering" which was (among other things) about performance in the presence of the memory hierarchy. The upshot is that there are different cost models that you have to use in the analysis of your algorithms (e.g., IO complexity), but the techniques that you use for the analysis are the same.

---

To be honest, I think the system is working as intended here. Undergraduate courses are not really designed to push people to the forefront of current research. They're intended to give you the basic skills you need to catch up to modern developments yourself.

I think what's happening here is that people remember "optimality proofs" from their algorithms courses and take that to mean that there is nothing more to be done (that's the sentiment I got from this blog post anyway). The problem with this is that in this context "optimality" referred to a technical definition - optimal with respect to some specific simplified model of computation. The result is probably not optimal with respect to a more complicated model!

> 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 work. For the connection between CZF and type theory (choice and excluded middle are orthogonal on both sides) see Benjamin Werner "Sets in types, types in sets" and Bruno Barras' (still unpublished but available) habilitation thesis. There is more work here, but the equivalence between universes in type theory and universes in set theory should be clear from these references.

As for the "equivalence" between object classifiers in Topoi and universes in type theory, which definition of object classifier are you referring to? There is a notion of universe in a (pre-)sheaf topos and indeed such universes can model universes in type theory. See the work by Hofmann, Streicher, and many others.

On the other hand, the "internal" definition of an object classifier in a topos is a higher-categorical concept. The statement that a universe is an object classifier is equivalent to the statement that a universe is univalent in type theory.

> It still boggles my mind why type theorists think that "function extensionality" and quotients, two entirely 1-categorical concepts, are best treated using homotopy coherent diagrams. And it is unclear since when proving theorems in less generality (because additional axioms are assumed) is considered progress.

To be clear, one can treat 1-categorical extensionality principles in an extensional type theory, see for example observational type theory which has functional and propositional extensionality as well as quotient types without compromising the computational character of type theory.

As for your question, think of it like this: You can easily treat 1-categorical concepts within an infinity-topos, but the other way around is very complicated and involves quite some encoding overhead. If you are in homotopy type theory you can model ordinary extensional type theory (with some caveats about the universes) by restricting yourself to working with sets. The other way around is, again, just as crazy as in set theory.

And progress in type theory and logic is not about proving things with less assumptions - you may have been thinking of reverse mathematics. Homotopy type theory is considered progress since it fully explains the behavior of intentional identity types, which already existed in traditional Martin-Löf type theory.

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 over B. On the other hand, there are many language features that are orthogonal to first class functions, for which the translation is no less complicated than the frontend of most compilers. For example:

- Delimited continuations

- Related to this, algebraic effects and handlers.

- Implicit types.

- Join patterns for concurrency.

- Linear/Affine ressource management.

- Related to this, type state and session types.

- Probabilisitic programming.

- Differential programming.

And many more. The point is that you do not want a language that includes all of these extensions at the same time, since many are mutually exclusive. For example, differential programming does not mix with state or first-class functions. Linear types ensure safe ressource management, but you need an escape hatch both for efficiency and your sanity. Algebraic effects or delimited continuations in a language which already has imperative features will lead to very fun bugs as soon as someone unfamiliar with the language implementation tries to mix the two features.

On the other hand, for every single example in this list I can point to an application domain where the additional expressivity is beneficial.

E.g., delimited continuations are extremely nice when implementing some complicated backtracking search. A DSL with (pure functions and) first class support for delimited continuations can express such a search function very naturally and later on - in the compiler for the DSL - we can decide how to implement this feature.

This allows for additional optimizations, which would otherwise be implemented in an ad-hoc manner. For example, several linear return continuations can be implemented by having several return addresses and stack pointers and restoring one of them, rather than using a cactus stack. Another example, rarely used return continuations can be tracked out of line as in "zero-cost exception handling".

Mixing these implementation details with the implementation of your search function is just a bad idea, since they are orthogonal to the problem you actually want to solve. And, as we all know, mixing continuations into an existing imperative language just gives continuations a bad name, which is precisely why you want a DSL. :)

Derek also gave a terrific keynote talk at POPL 2018 about the big picture: https://www.youtube.com/watch?v=8Xyk_dGcAwk

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 suitable manifold, so I would expect conjugate gradient or Newton methods to perform better in practice.

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 software - they're built to meet the demands of Excel 97 (exaggerating slightly for effect).

The programming interface of a modern x86 CPU is best thought of as a virtual machine with a JIT. The JIT performs some optimizations to make old code run more in parallel without the need for recompilation. This is a terrible model for compilers and programmers, since it makes optimizations hit or miss, and of course it's why we're in this whole spectre/meltdown mess at the moment. If we switched to a more reasonable programming model which actually met the needs of software (fine grained interprocessor communication without going through central memory, many more registers, actual software access to pipelines, caches, etc.) then it would make a lot of old software run slower (through emulation), but new software could finally make better use of your hardware...

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 less naturally, but things are not "made out of sets".

For example, the real numbers are not sets in the same sense that "the map is not the territory". Sets allow us to encode real numbers, but this encoding is mostly arbitrary. Is 3 an element of pi? If pi truly is a set, then this is a sensible question to ask, since sets are defined by their members. However, there is evidently an abstract concept of "real numbers" which exists without mentioning the elements of a real number. The technical reflection of this dilemma is the fact that in set theory there are multiple isomorphic copies of "the complete archimedean ordered field" which are all different as sets.

This is one reason why type theory is superior to set theory. In type theory we can actually capture the abstract concept of real number and work with it, instead of always working with an encoding. This might not matter so much for something as simple as a real number, but it matters a lot when you talk about more complicated structures.

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 as we stay in the same language. So while it's currently difficult to verify a compiler from a rich functional language to assembly, we have very good tools to verify a compiler from one subset of a language to another.

So if we want to verify a compiler from a functional language to assembly we "simply" need a language that is a superset of both, and that's where FunTAL comes in.

---

I'm looking forward to reading the paper and it's great that this project is producing some independently useful artifacts. On the other hand I still think that this approach to compiler verification is a bit odd. Time will tell, I suppose...

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?

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 formal verification: - You have to go over every single line of code (to show full functional correctness|to achieve full test coverage). - The amount of code that goes into (verifying|testing) an application is on the same order of magnitude as the application itself! - There are still bugs in (unproven|untested) parts of the application! - It's not perfect, so why should we use it at all?

At the end of the day, formal verification is slowly but surely becoming mainstream. Whether through more advanced type systems, static analysis, domain specific model checking, or through interactive theorem proving. We're finally at the point where whole program verification is starting to become realistic for some domains and it will only become easier from here.

---

As for the article itself, others have already pointed out some specific problems. Let me just add one more: Simulation proofs do not scale, but are far from the only option. I would encourage you to look into more high level verification techniques using axiomatic semantics, such as Iris in Coq.

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 second player tries to prevent the first player from finding a proof and gets to move at every conjunction, selecting a side of the conjunction to descend to. The final state here is an atomic proposition which is either true or false and determines which player won. You derive a value function from that in the same way as you do for Go or Chess.

You can extend this idea to full first-order intuitionistic logic and probably also to higher-order logics, as well as many different modal logics. There are also formulations of classical logic as a single player game, but that doesn't seem to be very useful here.

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 is essentially unbounded.

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), clock quantification (to introduce new dimensions), and dimension analysis built into the type system in the form of "clocked universes" (type universes which depend on clocks). The latter is required for the semantics to make sense, but it also allows an implementation without implicit caching. In particular, GDTT does not have an analogue of first for all types, but only for those types which don't themselves depend on the clock parameter and this requires clock dependence to be tracked in the type system.

Maybe not so interesting for stream processing as is, but it could probably be extended along those lines...

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 time there is a cons (:).

One way of getting better performance "by default" is to construct lists with constructors for empty list, singletons and append and then adding equations to ensure that the resulting binary tree is balanced.

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 that there are examples of "types with equations" which cannot be expressed as a rewriting system, e.g., free groups.

It's a still a cool feature to have this built into the language.

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), and what this feature adds is that it allows us to associate a first-order type constructor to a trait.

Since the type constructor is first-order, and first-order type constructors are already present in the base language in the form of generic types, the implementation is simplified to the point that it can reuse the existing infrarstructure for type inference.

---

Apart from that, the reason for this implementation choice seems to be that it's required for precise lifetime management. Almost all datastructures in rust seem to be parameterized with a lifetime argument, even if they have no further type parameters. Since there is no such thing as a second-order lifetime (i.e., a "lifetime constructor" T : (lifetime -> lifetime) -> lifetime), first-order type constructors are enough to handle all issues that pop up because of lifetime management.

---

That actually seems like a very pragmatic design. The only problem I had while reading this RFC is that the combination of "multiple-inheritance" in traits with their built in namespacing leads to some really ugly syntax, e.g., "<T as Foo>::Bar<'a, 'static>;". Is this already idiomatic rust?

There's several more things that confuse me in this RFC, but this is probably the wrong place to discuss these things. Incidentally, what is the right place to talk about this?

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 difficult type inference problem (going from easy first-order unification to undecidable higher-order unification), while associated types are simply existential types (and in particular no more difficult than higher-rank polymorphism).