Counterexamples in Type Systems
counterexamples.org
counterexamples.org
At least BNF grammars are legible
Maybe a better way to describe the notation is "off-putting"?
Like many kinds of formal notation it almost requires a class in a university to have it explained. The same is true of other fields dense in notation where you need to learn the conventions as much as the basics.
That said, of course jargon often is als abused, or used in cases it doesn't have to be, etc. -- that's s bad! And many papers and books suffer from this and would be improved by using less jargon.
But in general I find this negative stance against formal notation, and the expectation that one should be able to dive into subtle and advanced examples without a need of at least some "studying" (not at all necessarily at a university!) quite odd, and unrealistic.
Jargon is ok. Jargon is what happens when you want to be precise while re-using brain machinery for reading. The exotic notations are, on the other hand, just jargon put in a form which you have to (re)learn how to read, for the sake of conciseness alone. That conciseness may pay off if you're going to be working with the notation 8h/day for 10 years (or a year, or maybe even half a year), but if you just want to read and understand concepts and learn facts... To paraphrase: you wanted a banana, but what you got was gorilla holding the banana and the whole jungle along with it.
Hence my question: isn't creating exotic, one-character == 2.5 concepts, notations simply optimization which is harmful to the vast majority of potential readers?
Sorry, I don't follow. What is ASCII? Can you please avoid using computer jargon in your text, it makes my head hurt and it's an unnecessary barrier to entry. Can you please write instead "7-bit encoding of text characters"?
:)
> ...that much harder to stay ∋⌞0x21,0x7D⌝
It may be just me, but I think there's a huge difference between the two, even though both are equally made-up.
You are using wrong / nonstandard notation with no context or definition. Of course I have no idea what you're talking about.
Imagine if instead of writing
(-h/2m ∂²/∂x² + V) φ = E φ
you had to write
“Divide the reduced Plank constant by twice the mass of the particle, then multiply by the second derivative, with respect to the x-coordinate, of the wave-function. To this quantity, add the potential multiplied by the wave-function. This is equal to the product of the energy eigenvalue and the wave-function.”
because you don't want to memorise what ‘∂’, or the superscript 2, one number over another with a bar means, or that the funny greek letter means wave-function in this context x)
Which is exactly how the notation is used in many papers. You're supposed to have the context (from reading books and other papers in the area) and infer the definitions ("it's trivial to show, so we won't"). It's a passive-agressive stance from the perspective of someone not belonging to the club.
> “Divide the reduced Plank constant by twice the mass of the particle, then multiply by the second derivative, with respect to the x-coordinate, of the wave-function. To this quantity, add the potential multiplied by the wave-function. This is equal to the product of the energy eigenvalue and the wave-function.”
When I imagine this, I'm ecstatic. The difference between the two formulations is that the latter I can work my way through with a search engine, WolframAlpha, and Wikipedia, while I have no way - other then learn the whole subject matter - to decipher the former. I just don't understand what's wrong with the second formulation. From what I read, this was the standard way of writing about maths and physics until 17th century - at least. Yes, it's more characters, but it's infinitely more readable and discoverable to the uninitiated.
Not to mention, from the classes I attended, lecturers often say it out loud in exactly this form, while writing the symbols on a whiteboard. So it's obvious that the two are equivalent.
The former notations lends itself better to algebraic transformation, so I don't have any issues with using it for the intermediate steps, but the result - which is what I'm after, as a causal user and not a practitioner - could be presented in both forms. It would immediately unlock a lot of knowledge for use by non-experts. What's wrong with hoping for that?
I think there are two answers:
1. This style of notation was, I believe first really developed in Principia Mathematica in 1910ish. Some of the proofs in that book are big, and would be vastly longer if they were in plain english.
2. Part of the goal of that book was precision. They could reuse existing words, but those have pesky connotations that might mislead. So instead they'd either be left to invent new terminology "sqaggle x, y lemmy ror, x grorple y" or pick something symbologicial.
There are really good conversations about intuitiveness of notation (see, e.g. https://mathoverflow.net/questions/366070/what-are-the-benef...), and I think that comes down to things being hard. Notation is almost always created by an expert who is making something useful to them. It's not clear that the correct expressive notation would even be the same as the correct layman's/teaching notation. Those two concepts may simply be at odds.
This bit from the tail end should not be missed, in our context:
> ADDED LATER: One should also distinguish between the "one-time costs" of a notation (e.g., the difficulty of learning the notation and avoiding standard pitfalls with that notation, or the amount of mathematical argument needed to verify that the notation is well-defined and compatible with other existing notations), with the "recurring costs" that are incurred with each use of the notation. The desiderata listed above are primarily concerned with lowering the "recurring costs", but the "one-time costs" are also a significant consideration if one is only using the mathematics from the given field X on a casual basis rather than a full-time one. In particular, it can make sense to offer "simplified" notational systems to casual users of, say, linear algebra even if there are more "natural" notational systems (scoring more highly on the desiderata listed above) that become more desirable to switch to if one intends to use linear algebra heavily on a regular basis.
Your previous comment, though, is much less optimistic (to me): you say that, even if they are aware of this, the experts have no incentives to use "simplified notational systems". That means that I can either become an expert myself, find an expert who will translate for me, or be unable to make use of the knowledge contained in materials for experts. I wish there was some other choice, like Google Translate from math to English...
I myself have been studying category theory (CT) off and on for a few years now, trying to get enough of an understanding to be able to explain it to others in the software engineering (SE) field. I think there's a lot to gain from CT, but it's so strongly founded on distant mathematical fields like algebraic topology that it's very hard to get at its essence and find tractable connections from an SE perspective.
Finding good explanations is really a hard research problem of its own; it just isn't funded that way.
> That means that I can either become an expert myself
I don't think there's any way around this. If you understand a topic, you have obtained some amount of expertise thereof. An expert cannot simply translate for you; it's not a merely notational difference. There's a body of knowledge that must be transferred.
I would recommend finding an expert who's willing to correspond with you on occasion, and look for more introductory materials like textbooks and position papers in the field. If there's a particular goal you have in mind -- say there's a specific paper that achieves something you have an interest in -- be up front about that; it helps focus the explanations and recommendations.
Being an expert doesn't mean you have to have a very broad base of expertise. In fact, it could be argued that most experts are expert in a very, very small and focused niche. The smaller the niche, the less you need to digest; but the more rarefied the niche, the more stable the successive foundations below you need to be.
As someone who dabbles in the field, I'll bite. I find that more succinct expressions make their structure more apparent than less succinct expressions. This is critical for identifying (and then demonstrating) the general principles underlying any particular example, which is a great deal of what we do in theoretical research. (It's usually better to describe a whole family of solutions than to describe a single solution; and failing that, to indicate some directions potentially leading to general principles.)
What do I mean by structure? This is a bit of a dodge, but structure is what you get when you remove all the data, all the aspects that pin an expression to a specific scenario instead of a general pattern. If you can recognize and memorize the pattern, you can apply it to a much broader class of examples than the one you learned it from. Concise notation is one tool for downplaying the concrete data and calling out the common aspects more deliberately.
As other posters have said, this can be abused. I'd even say it's a very rare paper that uses concise notation appropriately to its fullest extent as an aid to the reader. But the concision does serve an important purpose to experts in the field (who need rather less aid): it makes the newly contributed patterns more visible (and uses existing patterns to effectively de-emphasize parts).
> but if you just want to read and understand concepts and learn facts...
Most research papers do not have as a goal for a technical reader to understand concepts and learn facts. (There are certainly visible exceptions, see just about anything written by Simon Peyton Jones.) Research papers are evidence of progress at the forefront of human knowledge; they're shared amongst an expert community to help drive that whole community forward.
We absolutely need more effort to distill research and collect it into a more cohesive picture. Unfortunately, that responsibility does not (and probably cannot, in the current system) fall on the original researchers themselves. There are a few organized efforts out there for some fields; the one I know of is Distill.pub, for machine learning: https://distill.pub/about/
>> When we rush papers out the door to meet conference deadlines, something suffers — often it is the readability and clarity of our communication. This can add severe drag to the entire community as our readers struggle to understand our ideas. We think this "research debt" can be avoided.
But I don't think the concision of notation is at fault. It's just the most obvious roadblock to a (relatively) lay reader. The truth is simply that the paper wasn't written with you in mind.
You could make a case that, in order to be of value to (most ordinary) programmers, type theory needs to present their results in programmer-speak, not in math-speak. But then programmers ask questions like "why is that true", and the answer is the proof which, being a mathematical proof, is in math-speak.
Wikipedia says[1] the earliest use of characters resembling + and - was in 14th century. From what I remember, math books were light on special notation until (at least) 18th century, and another poster here says it could be even newer (beginning of 20th century).
> and the answer is the proof which, being a mathematical proof, is in math-speak.
There are many, many proofs in Euclid's elements, and the only unusual (ie. not in plain natural language) notation used there (from what I remember and after a cursory glance now) is using clusters of capital letters to denote line segments.
Proofs are just logic, and logic was used for millenia (I think?) before someone decided that `∧` is better than "and" and we should all use it.
What I'm trying to say is that the "math-speak" is (or should be?) defined by what you're talking about, not in what syntax. And if this is true, then using more familiar syntax would be better for lowering the barrier to entry.
On the other hand, as Twisol notes, the modern terse syntax probably has its merits for experts. I'm a casual user - I won't be writing papers or checking their correctness - so I get all the bad (unfamiliar, strange symbols, context dependent syntax) without any good parts. :(
Going through a single line of text to understand a concept is much better than having to go through two or more. I believe you should understand that, if your definition of conciseness matches mine.
As a programmer, you know first hand that repeating oneself is bad practice: it's better to define a function which will encapsulate this computation you need to repeat rather than using copy and paste. The same goes for any language: having vocabulary to embody reccuring ideas helps us discuss complex ideas more easily.
> Do you really need to express concepts with a single strange character?
It is only strange to you because you don't speak greek. Of course many don't: my pedantic point is that Greeks might disagree with you about these characters being strange, and less pedantically, the scientific community will argue that it's not that strange when you belong to their group. There are only a handful of them to remember in the context of type theory.
I guess you would want these characters, like Gamma (Γ), Delta (Δ), tau (τ) or sigma (σ) to be replaced by their ascii equivalent (eg. G, D, t, s), or perhaps even more evocative names? But even if this would be done, you'd still have to understand the underlying concepts they represent, such as the typechecking context which is usually represented by Gamma.
These concepts are indeed not easy to understand: you would have to learn to become a Gorilla in order to be able to hold that banana you languish for, or survive in the Jungle that surrounds it.
One good thing about using a different character set is that they stand out. There's little chance to confuse them with words of vernacular English. Greek mathematicians actually might have a harder time with these notations than you do :)
Yes, but we're talking about the syntax/notation here, not the underlying concepts. I see it like this: imagine a function which has a single argument, in a dynamic language so that we have no type annotation. Let's say I named the argument "pair_of_ints". Following your logic, I should have named it "i2" instead, because then I wouldn't have to repeat myself by writing all the p,a,r,o,f,n,t,s characters all over the function!
Another way of saying this: yes, it's good to encapsulate pieces of logic in subroutines/functions/methods/etc. It's not good, however, to name the functions (let's add: in global scope) f, g, h, f2, f3, gh, etc. just to avoid typing more characters. Instead, we choose a name which can be understood with as little additional context as possible.
> having vocabulary to embody reccuring ideas helps us discuss complex ideas more easily.
Yes. My problem is when all the entries in the vocabulary are one (Unicode) character long.
> I guess you would want these characters, like Gamma (Γ), Delta (Δ), tau (τ) or sigma (σ) to be replaced by their ascii equivalent (eg. G, D, t, s), or perhaps even more evocative names?
The latter, preferably. If something is meant to denote a context, I see little reason to name it "Γ" instead of, I don't know, "context"?
> But even if this would be done, you'd still have to understand the underlying concepts they represent, such as the typechecking context which is usually represented by Gamma.
Yes, but then I wouldn't need to work to understand the syntax, making the process of understanding the concepts easier.
> No unicode or infix operators for judgement forms. When I use them in my proofs they make perfect sense, but when you use them in yours they're completely unreadable.
Computers (parsers, rather) are extremely sensitive to notation, and indeed in this project they eschew greek letters and unicode altogether, however it makes things more verbose, but it is almost certain that the authors communicate the ideas in paper with notation like Γ ⊢ e : σ instead of `TYPE Gamma e s`.
Ah, you're not talking about the same things: you speak code, he speaks type theory.
You are completely correct on that: a good naming convention is better for readability, particularly with a large codebase.
So, let's try to find a compromise. It really depends on the size of the lexicon in the language considered: if all you have is 50 rules in your type theory, do you really need to give each of them a name fully describing its semantics? Of course you don't, so calling them inl1, sub2 etc. shouldn't be an issue, if the name can still act as a reminder of the rule meaning. In the same spirit, rules usually connect together few objects: a context, at most half a dozen of type variables which come up all the time in the rule set, a few operators. Maybe someone with some experience with functional programming would find it easier to understand. In fact, I think I pretty much paraphrased the quote above.
> Yes, but then I wouldn't need to work to understand the syntax, making the process of understanding the concepts easier.
I very much agree with that, but I also think that it's a question of training. In software engineering, people routinely devise DSLs, learn new languages to handle a specific problem or adapt to new working conditions. Once you get the hang of it, it should become easier.
Here's a small tip: Gamma in the greek alphabet corresponds to the letter C in the Roman one, so it sort of makes sense, if one's using Greek letters, to use Gamma for Context - like one would use Delta for difference in math, for instance. It's confusing at first, but it might also help in learning the Greek alphabet - again, same as what we have to go through in math classes.
We're talking about type theory and you took the escape hatch.
> Let's say I named the argument "pair_of_ints". Following your logic, [...]
You spoke of conciseness, that's the logic you introduced, not hers.
> It's not good, however, to name the functions (let's add: in global scope) f, g, h, f2, f3, gh, etc. just to avoid typing more characters. Instead, we choose a name which can be understood with as little additional context as possible.
That's perfectly reasonable to expect programmers to use long enough, meaningful names in a complex program. But here the topic is type theory, which are made at most of a few dozen rules (unless you already want to tackle on a complex type system, but that would be like trying to learn how to drive on an indycar). In such a setting, long comprehensive words are not really needed.
If you allow me to transpose this issue of yours to your domain, software engineering newcomers might see this arcane notation of using brackets everywhere quite confusing. Why not simply use plain English to describe a program?
> Yes. My problem is when all the entries in the vocabulary are one (Unicode) character long.
It's not so bad, why limit yourself to 52 characters when you can have so many more to choose from? Korean has more than 20 different characters for vowels alone (luckily they don't have capital letters), Japanese has 2000 kanjis to convey meaning, not counting the (200 or so) kanas used for spelling and connecting words. Chinese has 10k symbols in everyday use, and so many more obscure ones.
The good thing about these Unicode characters is that they have a short notation, but a long pronunciation, a bit like the spelling alphabet (Alpha, Bravo, ...).
I guess that my point is: English speakers have it easy at the morphological level, learning a few more character cannot be that difficult.
> The latter, preferably. If something is meant to denote a context, I see little reason to name it "Γ" instead of, I don't know, "context"?
If there's only one context being considered, one might as well use Gamma (that letter corresponds to C in the roman alphabet, btw). Perhaps the hidden secret of all this discussion is that Type Theory is more a math subject than an engineering one. Of course at some point a type system has to cross this boundary to be implemented, but that doesn't mean that math people have to speak pseudo-code.
> Yes, but then I wouldn't need to work to understand the syntax.
Math uses Greek letters by tradition, perhaps because the first occidental ones where Greek? As for the horizontal bar to separate the premises from the conclusion, it's an inheritance from Gentzen notation for natural deduction (iirc). Obviously, our knowledge builds up incrementally from former discoveries/inventions, because (at the risk of this discussion to become absurd) how would you be able to extend something if you have to start from scratch every time? Conversely, what would be the point of using a different language once you've done the effort of learning the one used all through the literature?
Sometimes things do change however. A few centuries ago, scientific articles were still written in Latin, or sometimes French. In a sense, it has to be a step up in the right direction for native English speakers now that papers are in English (for those devoted to an international readership at least), perhaps not so much for Latinists and French speakers though. Maybe someone like you will do the extra effort of learning the old way, and push for a new way without the fancy typography? But you'd probably have to publish significant papers for that.
But let’s think about it.
I feel pretty confident that most people on this website are capable of learning the core 2400 Chinese characters in a year if they spent a few hours a day and that’s literally a foreign notation. A lot of people learn new languages all the time.
Kids who don’t want to learn calculus, learn calculus every day. The notation isn’t just awkward, the concepts are too. Yet they learn it.
What we’re talking about is a small notation. It’s a handful of symbols. They work predictably and consistently and the people learning it are usually familiar with the subject on some level.
It’s off-putting because it appears foreign, but the concepts and actual mechanics are already familiar with most of these readers. They just need a Rosetta Stone to help get past the initial awkwardness.
When you look at it from that perspective, it is kind of insulting use a hyperbolic word like insurmountable to a group of programmers.
Many chose not to learn it because they don’t want to be bother or don’t see the value investing their time.
Throwing words like insurmountable around seems like it breeds learned helplessness.
Teaching calculus to children is a good example of why. They have a teacher to hold their hands and answer questions 40 minutes a day with mandatory homework assignments.
If you study concepts on your own, you do not have this luxury. Its very difficult to internalize notation when you do not use it every day. The problem is not the notation itself, but the fact that no notation can be categorically searched and referenced. It cannot be typed or entered into google easily. It is rarely consistent between authors, which is free of problems if you are already fluent in the notation.
Sometimes you can get away with "what does upside down A mean" but consider something like `\forall n \in \mathbb{N}`. Imagine if you simply had `unsigned int` (I don't want to debate the exact implication of unsigned int versus the naturals, but it should serve a point).
When I have tried to explain relatively simple notational structures to working engineers, the universal feedback is along the lines of "I wish there was a good reference for notation because I can't understand this or keep up with it."
Pseudo code, or something akin to it, may be more ambiguous but is much easier to grok and document.
As an aside: something that constantly irks me is the celebration of terseness and convenience. This plagues many texts and robs novices and experts alike from understanding. Notation that is terse to the point of resembling arcane incantations is a problem, and it bothers me that academic publications in the applied sciences don't recognize it as one.
The problem I run into, again and again, is that all the notation is presented as already understood, even in introductory texts. It's not explained, and it's not clear where I'm supposed to go to get it explained. I can't search for it directly because it's a symbol, not a name for the symbol, and if I do manage to find the name, I'm left to wade through all the different contexts in which it might be used to mean something to find out which it is.
It's not an insurmountable barrier because I'm incapable of learning. It's an insurmountable barrier because I can't find a reference to learn from that doesn't already assume I know all the answers.
when you click you never give a damn about notation but before you do it's such a drag
it's like monads
Inference rules just transform the traditional format of
(A && B) -> C
A B
---
C
The usual recommendation seems to be "Types and Programming Languages" by Benjamin C. Pierce.
But then I was able to re-start Thompson's "Type Theory and Functional Programming" and it was clear that I started to understand a lot of it.
If you enjoy the nostalgia of older books like me, then pick up an original copy of "Intuitionistic Type Theory" edited by Per Martin-Löf.
> What's the relationship between programming language theory and type theory?
I'd say programming language theory is more broad than type theory, for instance topics such as compilation techniques and runtime systems are more distant from type theory (though you might prove some type-theoretic thing like type preservation).
There's also a range of type theory books because it's a field that spans pure logic to programming languages, so you can find books like Type Theory and Functional Programming by Thompson that elaborate things like dependent types early on.
Essentials of Programming Languages is very implementation driven and they implement a wide variety of interpreters for untyped languages, typed languages, concurrent, imperative, continuation-passing, object-oriented and more.
It shows that is important to take soundness of type-systems serious. I like what they did with Scala: they boiled down the language into the fundamental parts and built a language from it that has a sound type-system (machine-checked). This has now finally become Scala 3.
Here are some more details: https://www.scala-lang.org/blog/2016/02/03/essence-of-scala....
While Scala 3 filled a soundness hole, it opened a practical crater (and no, path dependent types are not a viable substitute).
Too bad, many nice improvements overall.
Does it show that? I see it more like a set of examples demonstrating there's no such thing as "a sound type system".
[1]: <https://en.wikipedia.org/wiki/Counterexamples_in_Topology>
Which also means you'd be able to add new semantical type behavior specific to a project, not just specific to a language.
What we're doing right now it's highly redundant, it's basically two languages in one. One describes the static constraints, and another the runtime ones. There's no need for that.
For me it is pure black on both Firefox and Chrome
See also https://github.com/adobe-fonts/source-code-pro/issues/250
What problem domain is so complex that it cannot at least be modeled in SQL (or Excel)? What language does not provide sufficient abstractions for tables, columns, relations & basic data types? Why would you want to take a clean domain model that the business agrees upon and then start perverting it with things like polymorphism? Performance is often something thrown around as an excuse to de-normalize schemas, but typically when I ask someone to actually measure it we find that LINQ/SQL/etc is more than fast enough to get the job done for all practical intents & purposes.
That said:
> What language does not provide sufficient abstractions for tables, columns, relations & basic data types?
A key part of the SQL data model is the primary key. I'd really love to see a programming language make PKs or something like them a first-class construct. So if we're looking for something neat to add to PLs that would actually help with business modeling, maybe we could start there?
This certainly seems like an excellent place to start. Every single one of my domain types starts like:
public class MySpecialType
{
public Guid Id { get; set; } = Guid.NewGuid();
//...
}
But, what about the relational aspect? Identity is trivial to solve IMO. How do we canonicalize this idea of relations between types? The way I do this today is:
public class MyRelatedType
{
public Guid Id { get; set; } = Guid.NewGuid();
public Guid? MySpecialTypeId { get; set; }
//...
}
Is there a better way to express this idea with some shiny new language constructs? I feel like I am running out of physical lines of code to golf with here.
The only thing I can think of that is more concise than my above code examples would be SQL.