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.
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. "
fwiw I unwittingly retrod this path; looking back at early versions of my algebraic type library there were all sorts of provisions for automatic smart constructors (commutativity, identities, etc., surely inspired by Goguen) that got dropped from later versions for lack of use.
I don't know. But I've read quite a number of papers on type systems, type inferences and functional languages in general from late 80s and early 90s, and every time they mention Miranda, there is this footnote that says that "Miranda is a trademark of Research Software Limited", e.g. [0][1][2], so there has to be a reason why they did this. Sure, Turner himself did that as well, see "History of Haskell" [3], "3.8. Haskell and Miranda":
As required to safeguard his trademark, Turner always footnoted the first occurrence of Miranda in his papers to state it was a trademark of Research Software Limited. In response, some early Haskell presentations included a footnote "Haskell is not a trademark".
but that doesn't really explains why others did... so a hypothesis that maybe he did send people who didn't attribute Miranda's trademark a letter of complaint seems somewhat amusing, you know? A small in-joke for those people who brushed against the FP research of the early 90s.
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.
Disclaimer 1: I have the same last name as Burstall's collaborator, Joseph Goguen. If we're related, it's VERY distant, so I truly can't add anything.
Disclaimer 2: I'm going to tie this back into algebras.
Setup 1: However, I have been a little obsessed with Burstall and Goguen lately and I've been SLOWLY working through some papers and trying to make sense of it. I'm just an F# programmer who likes languages, not an academic.
Setup 2: I've known about Burstall/Goguen for some time, but I never understood the gravity of their respective work until recently. And I have quite literally been annoying with my tech friends and family with all my "Oh my god!" moments as I've been going papers and festschrifts.
This whole time, I haven't been sure if I've been interpreting what I'm reading correctly, so your post has been wonderful in settling some of that.
I understand that some people may resist the idea of describing algebraic data types as analogous to the fundamental theorem of arithmetic for types. Burstall and Goguen were motivated by creating tools and systems built on solid foundations, such as universal algebras, to utilize analytical tools like logic systems and category theory for deeper insights.
However, I believe they were particularly focused on how algebraic data types model the cardinality of state spaces and transitions between states for this reason:
They were designing a specification system that helped working programmers design systems accomplish two things (In today's parlance):
1. Make invalid states impossible.
2. Make invalid transitions between states impossible.
While learning Maude (OBJ's successor), I've been particularly fascinated with how its parent language let you define very fine grained domains.
And it makes sense, because if you're going to search through that domain to find counter-examples violating your theories, it makes sense to reduce the search space proactively.
But what really drove that for me (and maybe I'm projecting here), is how that seemed to correspond to a little program I wrote that constructed a bijection between the natural numbers and all closed lambda functions.
But what really convinces me that they had that in mind is how Maude and OBJ let you add attributes to constructors to identify them as associative or commutative or whether it has an "id" where the impact of these attributes on the constructors actually reduces the state space.
Again, I could be projecting here, but I would love to hear your thoughts and I am excited to read your next post!
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?
I thought the way you explained free algebras was great. I am absolutely not an expert in Clear/OBJ (I'm very much still learning), so I personally appreciated your presentation of it.
To answer your question regarding how these languages are meant to be run:
1. You know more about Clear than I do, so I'm at a loss.
2. I've read through OBJ's documentation, but I've never used it. But Goguen is usually demonstrating it as a language for quickly prototyping mathematical objects, experimental programming language, logical systems, theorem provers, etc. The manuals usually focuses on applying reduction rules to verify models (He claims reduction is often the go to method for proving properties), so I'm not entirely sure how much it parallels TLA+/Alloy yet.
3. Maude very much feels like OBJ where they added additional features to give it TLA+/Alloy like features that allow you to check invariants through searching. It's worth pointing out that Maude is very reflective and that many features of Maude are written in Maude on top of a fairly small core based on rewrite logic. It's not unusual that while you're reading the documentation for an LTL checkers or an SMT solver feature, that they'll show you the Maude code that defines that feature.
To answer your question: Maude does targets a similar niche and has been used to verify concurrent applications, distributed systems and protocols, but I really haven't explored that side of it yet. I've mostly been playing with Maude's functional modules and really spent much time with Maude's object-oriented modules which reflect the semantics needed to simulate and verify distributed systems.
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.
Yes, I think you might be right about that. FWIW, it's 4AM here and I am not firing on all cylinders. I live in the U.S. and politics is weighing heavily on my mind tonight.
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)?
