You need very little to make a Prolog-like language Turing-complete (lists and recursive predicates). And so Haskell's type system only needs one (or two) extensions to be Turing-complete, `UndecidableInstances` (and maybe `FlexibleInstances` or `MultiParamTypeClasses`). It is no accident. The name "undecidable" shows that the authors of that extension were well aware that it enables Turing-completeness.
I learned a lot from this and your other comment here!
The way I connected the dots when I read about Clear (and OBJ) is that it let me explain free algebras by example, by just showing Clear code. That hopefully makes the concept more accessible than the dry mathy definitions that would have the eyes of most readers glaze over.
I must say that I'm not familiar with Burstall and Goguen's line of research beyond what I've written so far. In the future I'd especially like to know what lessons these specification languages can teach (or already taught) about ML-style module systems, OO languages, and formalizations of mathematical structures in proof assistants (Clear reminds me of the little I've seen of Hierarchy Builder in Coq).
One concrete question I have is how Clear or OBJ or Maude code is actually meant to be run.
Your description of these languages reminds me of model checking tools like TLA+/Alloy. Does Maude target a similar niche?
IMO your view, if not common, is kinda intuitive from the point of view of someone trained in set theory/classical logic (i.e., most people before they find an interest in type theory; I myself was here a few years ago). If it feels like you're in a minority, it's because most others who might have the same opinion haven't reached the point where they could articulate it; many just give up way earlier on understanding type theory.
It certainly makes sense to a set theorist that union and intersection are more primitive than sums and products. From that perspective, type theory seems like a roundabout and unnecessary way of doing things.
The challenge is to imagine type theory as a radically different foundation to logic (because that's what it is), with sums and products as primitives instead, for one superficial difference.
It's hard to explain in words. I personally didn't get it without years of first-hand
experience with proof assistants based on type theory. Constructivism and category theory are other possible gateways into the right mindset.
There is one key difference which I think highlights the charm and simplicity of type theory without delving in technical details too much. The syntax of set theory is in two layers: there are sets, and there are propositions (about elements of those sets). In contrast, there is only one such "layer" in (dependent) type theory: types.
Types play the role of both sets and propositions if you want to encode set theory in type theory. The point is that types can be much more than either of those things, and that idea is inherently difficult to convey to someone whose only conception of logic is sets and propositions.
Thanks! Here we go:
"Note: In versions of Miranda before release two (1989) it was possible to associate "laws" with the constructors of an algebraic type, which are applied whenever an object of the type is built. For details see Turner 1985, Thompson 1986. This feature was little used and has since been removed from the language. "
Author here. It's funny you mention this. I was (am still) writing a post about it, and I went on a rant that while it's a (fun!) way to do "algebra with types", it's not actually the original meaning of it afaik, and then I went to look for a source for it and that grew into this whole blogpost.
That point is discussed in the paper: circle-freeness is Pi^0_2 in the arithmetic hierarchy, so there isn't a reduction to halting (Sigma^0_1) in the usual sense of a mapping between inputs. And in fact, Turing's paper does do a construction like you describe to show that yet another problem ("symbol-printing") is undecidable, and that one is much more similar to halting than circle-freeness. Again, this subtlety is discussed in the paper.
I think you were a bit quick in dismissing the OP paper based only on its title.
The paper in the OP discusses this claim in section 3, and mentions that Kleene came even before that:
> We would note that Kleene seems, however, to have already had the self-referential argument earlier in his classic book from 1952, Introduction to Metamathematics
They also bring up the "symbol-printing problem" present in Turing's 1936 paper, which is trivially equivalent to the halting problem with today's hindsight. That paper has a well nuanced take with a lot of interesting information.
Since that's the point of comparison, what's the Go standard library's strategy? Is it inherently slower than this or does it behave better for different scenarios?
How does this compare to using simd (like simdutf8)?
Even if you had a verified SMT checker, you also need to prove that the encoding of the problem in SMT is correct, i.e., that a proof does translate to a valid register allocation solution, to achieve comparable guarantees to CompCert.
I've learned quite a lot about editing from "Style: Lessons in Clarity and Grace." It presents some tricks to restructure and improve the flow of sentences, and through that process, to generate the momentum to really think about what you want to say.
> If the underlying premise is flawed, who cares if the methodology is correct?
How do we know the premise is flawed?
> The first step should be to show that the github dataset can be used to say anything about quality and productivity of things like language choice.
How do you concretely do that? The initial paper, even if flawed, did a lot of work to try to control for confounding factors. To do what you said, you would have to put as much effort, if not more, to convince people that the results can be falsified to claim anything, with the same level of control in place.
It's not even clear that counting commits is entirely meaningless. Getting some signal out of it does seem tremendously difficult, but not impossible. So questioning the methodology is really the only way to rebut the experiment.
> defunctionalization refers to a compile-time transformation which eliminates higher-order functions, replacing them by a single first-order apply function.
O(N + M) is not equivalent to O(N) if you make no assumptions about the relative growths of N and M, that's why it's actually meaningful to keep both terms around. You can only reduce it to O(N) when N dominates M (M = O(N)).
> I do wonder why people keep building more systems of this kind.
Not a lot of languages have higher-inductive types which is the main advertised feature here. At least they're missing in Isabelle and Coq.
That's also orthogonal to the matter of automation/metaprogramming, which, from the lack of mention, doesn't seem to be their focus right now. There doesn't seem to be anything fundamentally in the way of Coq-style tactics either if they really wanted to build that on top of what is presented here.
I don't have any experience with "business" code, but my naive understanding is that application-level code is typically very monomorphic which is exactly where refinement types are useful, whereas the OP leverages polymorphism to a large extent (not necessarily), and that works well for general-purpose libraries which don't and must not care about their users' data.