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.
785 karma · joined January 15, 2011
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 krishnaswami's paper on datafun, which is a functional language that includes datalog primitives in the form of least fixed points of monotone functions. Monotonicity is tracked in the type system, so this seems very relevant.
Edit: just saw that the paper was referenced after all, my bad!
- why do you need termination? Is it an artifact of the logical relation you use? If so, step indexing might help to relax this restriction.
That the set theoretic definition of "function" as a functional relation between sets is rarely useful isn't really so surprising that you need to emphasize that you use a more reasonable notion of function all the time.
And the integral transform notation is frequently changed, but only ever locally and in different ways by different authors. Pick up two books on "Fourier transforms for engineers" and I promise you that you will find different notations for the same thing and probably even different notations within the same book. And none of them will be good.
The latter is crazy. Consider the expression "F{e^{-t^2-y^2}}", which might stand for the fourier transform of a 2d gaussian, or it might be the fourier transform of t, with a parameter y, or it might just be the fourier transform of a constant function, or... It is only really defined in the surrounding text. The notation is incomplete and while in this example that might not be such a large problem it just gets worse as you pile on complexity. All integral transforms are written like this, as are expected value, variance and so on.
A lot of times notation in math is choosen to be suggestive. For example, the integral and sum notations are actually pretty neat, since they make common manipulations more visually clear. In particular, since the order of integration doesn't matter, putting the binder inside the integral as a "factor" is actually pretty inspired - commutativity makes Fubini obvious. The "d/dx" the author complains about can be made precise and is similarly great. Consider "dx/dz = dx/dy dy/dz", doesn't this just look entirely natural? But there's something about manipulating functions as first class objects that seems so unnatural to mathematicians that it needs cryptic notation to ward of the unwary...
> The UPenn dependently typed Haskell > program shows a great deal of promise and > is likely to manifest a decade before other > DT languages generate practical backends.
I don't agree with this at all. The design problems with tacking on dependent types to an existing system are massive - it's a research problem for a reason. On the other hand, writing a "ghc quality" backend for Coq/Agda/Idris/F* seems difficult, but at least it's an engineering problem instead of a rough idea.
In particular, CertiCoq is a compiler for Coq written in Coq, and the main problem here is verification. Simply writing a compiler is no harder than writing a compiler in any language.
> Interesting ideas out of Microsoft Research on SMT solver > directed programming editors that enforce invariants and can > generate code during development.
Another interesting Microsoft Research project along the same lines as Dafny is F. Both are nice, but F is closer to modern dependently typed languages.
> Lots of non-local reporting problems associated > with using unification during type-checker.
I would argue that the problem is that we use constraint solving for type checking. For example, strict bidirectional type checking leads to more tractable errors, since it's straightforward to follow the compiler's reasoning. On the other hand, bidirectional type checking is less powerful, so it's not like there's a silver bullet here.
> Type-safe OTP.
I wish more people were working on things like this. There's some theoretical work on calculi for distributed systems, but once they encounter the real world they inevitably become horrendously complicated.
> 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 cardinal axioms in set theory can be seen as adding more and more inner models of set theory (with fewer large cardinals) into an ambient theory. This is basically the same thing as asserting that "the previous theory is consistent". You can play this game forever and it will not converge - the result hinted at in the article states something different.
---
In the end we use set theory as an alibi. We tell people that ultimately all of mathematics can be encoded in set theory, but it is neither a natural encoding, nor is it really true since we are talking about different flavors of "set theory".
Algebraic geometry is a good example. To begin with, you are not using ZFC to encode categories - since you need to be able to manipulate proper classes as if they were sets - so we need to use some extension such as NBG set theory instead. Then, in order to construct the localisation of a large category you suddenly need large cardinals, even though intuitively the localisation is in some sense no larger than the category you start with.
And this is the point where we forget this construction again, because it doesn't give any useful insights.
There has been a lot of development on the Coq proof assistant since then. I don't imagine that working with Coq in 2008 was particularly pleasant. :)
For example, in Coq you would write
Definition Identity a := a.
Definition Compose F G a := F (G a).
Instance: Functor Identity. Proof[...]
Of course, this is no silver bullet and complicates other things. Everything works out beautifully though, if you combine conversion with bidirectional type checking, at the expense of less powerful type inference.
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/semigroups and isomorphisms.
For example, Gödel's incompleteness theorem is a technical result stating that certain definitions of "model theoretic truth" in classical set theory are incompatible with certain other notions of "truth as provability". Both the statement and its consequences have been so massively oversold for most of the past century that you should never use it in a discussion - think of it as a logical version of Godwin's law.
Similarly, no free lunch type theorems are formally the same as the statement that you cannot compress all n byte sequences into less than n bytes, which is really obvious for cardinality reasons. Again, there is no magic, just clever reductions.
The argument behind the halting problem also applies to your brain and anything that is somehow an abstract model of computation. More fundamentally, the fact that the self halting problem is undecidable is simply an instance of Cantor's theorem, it's not something that can be avoided.
Mathematical logic and therefore computers can be used to talk about infinity and more. Logical "paradoxes" are not a problem either. Some may be genuine proofs of inconsistency of some logical theories and others are simply theorems. The usage of the word "paradox" in natural language is simply imprecise.
---
I could go on, but really I don't take offense at any particular point. What bothers me is that you seem to be overselling mathematical results to argue a non-mathematical point... If you really want to apply, e.g., Gödel type theorems to discussions about your brain, you would first have to argue that the assumptions of Gödel's theorems apply. For instance, you could argue that the definition of model based truth in Peano arithmetic is something that your brain can decide. Then it would follow that what your brain does is uncomputable.
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 from whatever your backend is using is probably not that hard.
Since this is more mathematics than philosophy, the latest truly novel idea is also a few months old instead of a few decades. You really just have to start somewhere and work your way forward. :)
2) Extraction is not the only approach to verifying software with Coq (see Verifiable C, or Bedrock). In other proof assistants, e.g., in Isabelle or HOL extraction isn't even available and so other approaches are common. For a nice example look at the bootstrapping process of CakeML (https://cakeml.org/).
3) Even if it wasn't, the point is that the trusted base with verified software is tiny compared to anything else that people are actually using. "It's not perfect" is not an excuse if it is basically perfect in practice. See the Csmith paper ("Finding and Understanding Bugs in C Compilers", https://embed.cs.utah.edu/csmith/) and what they had to say about CompCert.
This whole "move fast and break things" philosophy should be unacceptable, if you want people to trust in your new cryptocurrency/voting machine/etc, but try telling your investors that it'll take 5 years to develop the software instead of 5 weeks to "a first prototype" whose bugs and bad design decisions will haunt you forever...
> There is nothing wrong with keeping the functional notation for density functions – as physicists and engineers always did – as long as one bears in mind that density functions cannot be evaluated, but only integrated.
This always bothered me, since, as noted in the very next section, distributions don't have an analogue to pointwise multiplication. Even worse, there is a perfectly servicable notation for such "dual functions/vectors" that physicists have been using throughout the second half of the 20th century. We could just use a consistent notation and not confuse new students, but no. "It's always been done this way" is a terrible argument and leads us to the confusing mess of notations that people still use for integrals and integral transforms...
---
Apart from that I would teach people recurrence equations/stream calculus before going into the limiting case of differential equations. It's true that differential equations are sometimes easier to handle analytically, but this is neither relevant (as the article notes) nor a great point in their favor, since we just end up teaching students a bag of tricks instead of explaining why something works...
Even if you somehow project every single point of discussion into one dimension, isn't this a weird axis? It seems like there are a lot of issues in the US which no sane party argues about in Germany (e.g., separation of state and religion). If you were to do a factor analysis after presenting the same polls to parties in Germany and the US you will probably end up with an axis which neatly separates everything by country...
> I think we'll also see the AfD reach a two digit number -- I hope for less than that, but less than 5% (which is the minimum for getting any seats) seems unlikely.
I hope that you're wrong and at least according to current polls >10% doesn't seem like a forgone conclusion (https://de.wikipedia.org/wiki/Bundestagswahl_2017/Umfragen_u...).
Julia has a lot more potential for optimizations than python, but what python has going for it is the larger ecosystem. So if you want to write a one-off experiment that's similar to stuff that already exists in C bindings to python you should use that. If you plan to write a large application that you still want to optimize for current processors in 10 years then I'm not sure if python is a good choice.
Personally I think it's a better idea to instrument your programs and count the number of memory (block) accesses or something. That metric might actually be useful to a reader a few years in the future. The fact that your program was running faster on a modern x86 processor from the year 2010 tells me nothing about how it would perform today, unless the difference was so large that you never needed statistical testing in the first place...
edit: I'm not sure if this paper is accessible to everyone, so here is an alternate link https://hal.inria.fr/inria-00443839v1/document
Is it really just that you can't easily test your program?
It's an LR(1) parser generator for OCaml and Coq with a lot of extremely interesting features, such as genuinely good debugging support for grammars and the ability of generating error messages by example.
What this means is that after you write down your grammar, Menhir will give you examples of all the possible syntax errors that could occur. You can then write error messages for each case and get a parser with built-in error reporting for syntax errors.
This works a lot better than you'd think and I really wonder why nobody else implements this feature. Or for that matter, why they're not advertising it on the webpage! If you want to know more, look in the manual, section 11.
Neither is a particularly satisfying solution if you want to reason about programs, which typically have richer notions of effects. My own recommendation is to embed programs via weakest preconditions (or strongest postconditions as in Chargueraud's characteristic formulas http://www.chargueraud.org/softs/cfml/). This does not allow you to directly evaluate potentially diverging programs, but is far more flexible when reasoning about programs. For example, you can use separation logic to deal with state and concurrency.
If you really want to extract to categories for some reason then I would recommend restricting to concrete categories of presheaves or sheaves - I know of no useful application that doesn't already fit into this framework. Using categories requires you to encode everything into a first-order language which is uneccesarily complicated when working with higher-order functions.
There are at least two formalization of HoTT categories if anybody wants to know more. There's one formalization in HoTT Coq and the formalization as part of the unimath project. Both work heavily with precategories as well as categories in order to formulate some textbook notions without changing all the definitions...
For example, the graph minor theorem states that a certain order on graphs does not have an infinite antichain. Classically this may have some interesting consequences, but in reality it's not very useful. However, the proof contains some real gems, such as the notion of tree decompositions and the graph structure theorem that lead to mountains of new results all throughout graph theory and related disciplines. Tellingly, the graph minor theorem is a short and simple question while the graph structure theorem is a deeply technical statement that would not have been conjectured on its own but rather was discovered in the process of showing the graph minor theorem.