It never ceases to amaze me how theorists can take simple concepts and make them impenetrable.
A type is a (possibly infinite) subset of all the possible values that can be provided as input to a program, or all the possible results a program can produce.
Type theory is about trying to figure out at compile time, if the inputs to a function are of a certain type (i.e. belong to a certain subset) what type the output will be (i.e. what subset of possible values the output will belong to).
It is not possible to figure this out in general because that would require solving the halting problem, so the art of designing type systems is choosing subsets of the data that allow you to prove useful things about programs at compile time so that you can find errors before the program runs, and eliminate run-time checks and hence make the programs run faster.
The reason people who like dynamically typed languages get frustrated with statically typed languages is that they value development speed more than they value run-time speed or avoiding of run-time errors, so they don't want to put in the extra effort needed to provide the compiler with the information it needs to do these compile-time derivations, or put up with the compiler complaining when it is unable to do them. They just want the program to run, and they're willing to pay for that with some inefficiency and run-time errors.
I never understood that. For anything non-trivial, development speed is increased with types: you get auto-complete, safe refactorings, code navigation etc.
The way static types can make development speed slower is not by forcing you to write the same code with extra types added in, but by forcing you to write different code. In this sense it isn’t really an argument about static types vs dynamic types (imagine a language with no type checks where programs have undefined behaviour at run time on anything that would have been a static type error) but rather a statically typed language vs a dynamic language.
There are patterns or language features in dynamically typed languages which are very hard to translate to static types. I think Peter Norvig has some slides somewhere comparing OOP patterns to lisp, a more dynamic language, and that is the sort of thing I’m thinking of here. For language features, consider implementing an n-ary list map in Haskell vs Common Lisp. Or the typed equivalent of delimited continuations.
That said, research on the differences between languages is difficult and inconclusive. I would like to see more of it.
It's very clunky to do in Haskell, but conceptually they can be built on top of a monadic pipeline.
In practice, the only case where statically typed languages force you to write different code is if:
(a) the type system is too restrictive and dumb (no generics, awkward function types, etc).
(b) you're trying to write a function that effectively returns monster types like Union[None, int, str, List[str]], which is common in dynamic languages but it's something you're not really supposed to do.
I agree with your broader point, that static types can in fact slow down development, but I have a different model.
Types are kind of two things at the same time: tags to tell the compiler how many bytes need to be allocated, and partial proofs of correctness of the program. The key observation of dynamic languages is that in most cases we can do without the first part: the runtime can handle that in the same way it handles memory management. I believe one of the mistakes of the original wave of dynamic typing proponents is that they kind of threw away the baby with the bathwater: the correctness part is important, and at least a form of optional typing should be provided.
The real trouble is that it's not easy to conjure type systems that are both expressive and ergonomic to use for the average developer. Sufficiently advanced type systems are indistinguishable from math riddles, and in a working environment that can be frustrating.
n-ary list map means a function that does map or map2 or map3 or …. (Where map2 is zipWith, not the one you get from the list monad.)
In Common Lisp the lambda-list looks something like:
(MAPCAR func list &rest lists)
And a slow implementation might look like:
(defun mapcar1 (f list &aux r)
(tagbody
g
(when list
(push (funcall f (pop list)) r)
(go g))
(nreverse r)))
(defun every (pred list)
(dolist (x list)
(unless (funcall pred x)
(return nil)))
t)
(defun mapcar (f list &rest lists)
(prog ((lists (cons list lists))
r)
loop
(when (every #'consp lists)
(push (apply f (mapcar1 #'car lists) r)
(setf lists (mapcar1 #'cdr lists))
(go loop))
(nreverse r)))
To implement such a function in ocaml you need to do something like:
type ('ftype,'output) t =
| [] : ('a,'a) t
| (::) : 'a list * ('b,'c) t -> ('a -> 'b,'c) t
val mapn : f:'f -> ('f,'x) t -> 'x
In haskell you would use a heterogenous list and type families. But note that I didn’t implement mapn in ocaml as it would be hard and unreadable…
One nice quality of dynamic languages is that you get very useful objects like lists or python/JavaScript style ‘dicts’ and lots of standard library functions to operate on them. You can implement them in a statically typed language to some extent but they are much less versatile and less first class. It means you often need to write different functions that do basically the same thing because they use different record or tulle types as input. I don’t think any mainstream languages are very close to static typing with structural subtyping.
For people for whom coding is an iterative, exploratory process, forcing type declarations upfront is not just slower… it’s a no-go.
There’s no way to bootstrap that process for them: you’re asking for the output as an input.
I think TypeScript has one of the best compromises.
Also, I think people are understating how easy dynamic typing makes substitutions — everyone else is writing their class twice (interface + class) just to get the same flexibility.
> For people for whom coding is an iterative, exploratory process, forcing type declarations upfront is not just slower... it’s a no-go.
Is there any kind of programming task where it's too much to ask the programmer to know the type of the function he's writing?
The only place I can imagine types being a burden is in a REPL (it's just boring to write them every time), but even then optional types like Python and TS are an unequivocal win (you're presumably going to move your code out of the notebook/repl and into proper source files at some point).
> understating how easy dynamic typing makes substitutions
Yeah so easy they're easily wrong. One of the worst problems of dynamic languages is that they don't have the concept of an interface, which makes it harder and not easier to write generic code.
> everyone else is writing their class twice (interface + class)
That's caveman Java right there. Interfaces with defaults (Java, Kotlin, even C# has something similar IIRC) can easily emulate dynamic patterns like mixins while preserving type safety and without the diamond problem.
> Is there any kind of programming task where it's too much to ask the programmer to know the type of the function he's writing?
I think the problem is that lots of type systems are inherently limited, so there may be patterns that you want to express that your type system simply can't, or that you have to write tons of boilerplate code to express. In languages like Java or C# that don't have Sum types, this can be as basic as "this value is a String or Integer". You have to write a class hierarchy to express this in Java. In JavaScript you simply accept a parameter and branch on `typeof value`. More powerful type systems allow you to express more patterns, but you still have to type them out. This can be done, but if you're doing exploratory work an unknown dataset then this can make the work much slower. And there be may little benefit.
In C# you just declare them as dynamic if you wish to emulate the ways of JavaScript.
People keep forgetting Basic is dynamic and .NET was designed to support it as well, additionally it got improved with DLR classes to support IronPython and IronRuby projects.
So you can co type crazy in C#, F# and C++/CLI, or just get hold of those dynamic features.
Oh sure. But at that point you are using dynamic typing. My dream language is one that allows for full gradual typing, with the ability to opt functions in (opt out could also work) to strict type checking which gives you the safety and performance improvements where you want them, but allows you the flexibility of dynamic typing where you don't. PHP-style runtime type checks would be automatically generated at the boundaries between dynamically typed and statically typed functions.
One problem with gradual typing is that it has comparable performance overhead to dynamic typing: You can only optimize out dynamic type checks, dispatching, marshaling etc. if you have sizeable, self-contained portions of your program (i.e. modules) that only use static types! So the "graduality" of it goes mostly unused in practice.
It can be a useful pattern when designing interface boundaries across modules (e.g. ABI's, data interchange formats etc.) to allow for the required flexibility in a limited context where the overhead isn't going to matter all that much.
Performance is only half the point. The other half is correctness. And I think this pattern of "important correctness and performance sensitive core, surrounded by simple but flexible glue code" is common enough that such a language makes sense. It describes pretty much all of the code that I write at work in fact. Being able to simply add type annotations and have the compiler generate the runtime type checks would be wonderful.
Genuine question: what does old PHP’s (not the newer stronger versions) interfaces and “type” hints count as? It’s very much a dynamic programming language from what I remember of it, but interfaces were crucial to it when I was using it in anger.
Is it one of those in-between systems, just more on the dynamic side?
I have never used PHP professionally, but if you're talking about PHP 5 style interfaces, they are definitely a form of type checking, and they were introduced with the specific purpose of facilitating object oriented programming in PHP.
The point I'm getting at is that using interfaces lets you make guarantees about what methods the objects must have. I'm not really picky about what specific technical means are being used to enforce those, but passing an object of the wrong type to a method is an entirely avoidable category of errors, and I prefer them to be flagged by the compiler/interpreter/runtime/tsc/mypy/whatever as soon as possible.
IME well designed interfaces are even more important than well designed classes, and dynamic languages unfortunately make it harder to enforce interfaces. It's not by chance that the first thing Typescript did was to introduce interfaces.
There's the key phrase. There's plenty of people that can whip up a POC or MVP in an afternoon of hacking or a week of fiddling, but going from that to something that can safely handle millions of users and hundreds of developer contributions needs types and other assurances. If it fits in a developer or a team's heads, then it's just fine - that's how I did my first major JS application, just Knowing what fields my objects have and what types they are expected to have. But that doesn't scale, people move on, gaps exist in tests, etc etc etc.
Seems to me that there's historically been more cognitive overhead to _learning_ most strongly typed languages, e.g you have to think about pointer vs reference, const, heap or stack allocation, borrowing if it's rust, etc. If you're not already familiar with the concepts, your development velocity is slow. But when you start writing more code, everything you said becomes true: types yield a lot of benefit.
People also seem to associate strong typing with compilers that bog down the write->run->debug loop, some of which used to have notoriously bad error messages, and things have changed because of JIT compilation (dart can even be both AOT compiled & JIT compiled), and also because modern compilers are so much better optimized and user friendly compared to just a decade ago (I mean, compare rustc error messages to GCC, lol). Compilers are doing a much better job today of helping decrease total debugging time.
FWIW this doesn't mean more advanced programmers necessarily move to strongly typed languages to increase their productivity. Instead, we are moving toward a progressively typed world (e.g typed python, typescript) to bring the benefits to users of dynamic languages as they begin to need them (without forcing them to use anything). And strongly typed languages are doing the opposite, e.g getting lots of dynamically typed features (e.g type inference in C++ with `auto`, initializer list syntax) which again, don't have to be used unless it helps with code readability and/or development velocity.
Historically, in many languages, you didn’t get either of these. If you were lucky, you would have ctags (https://en.wikipedia.org/wiki/Ctags) for navigation.
Also, development speed can go down if you have to show your compiler that data conforms to a given type. Certainly for one-offs where the user writes and maintains their own program, that can sometimes/often get you something doing something useful for the inputs you have _now_ fairly rapidly.
I think it’s mostly a historical coincidence that popular languages with conspicuous static type checking have often been slower to develop with than popular languages without conspicuous static type checking.
There might be a hidden assumption of stead-state in there. In the initial ramp-up when people are learning a language, or learning to code to start with, types will slow down development because there is one more system to learn and use correctly.
It is notable that if your code is going to be a bug ridden mess regardless of language features, language features that reduce the number of bugs (like type systems) are a hindrance.
But treating dates and surnames alike doesn't help robustness either.
Or separate types for metric distance and imperial distance might have prevented mars(?) lander losses. Or for sea levels referenced to Rotterdam or Le Havre might have prevented some bridges to have differing levels.
I guess; in the sense that it frees cognitive load from reasoning about properties of your program that are easily computed to think about properties that aren't. Even then, maybe thinking about the former primes you to reason about the latter. But even if the compiler tells you what the type of something should be, you ultimately have the synthesize something of that type.
think of the metric/imperial example above. The distance isn't just a number. Holds for most other things, too. Typed is key. Be it either static or dynamic.
Well, the article does not actually answer 'where do type systems come from?' (as in the type systems of programming languages) but 'where do type theories come from?' (as in the foundations of mathematics). I think type systems would have been invented for programming languages even if the mathematicians had never bothered with type theory, simply because they are necessary. I mean treating an integer stored in memory as a string or vice versa is still not going to work no matter what foundations for mathematics one likes...
> A type is a (possibly infinite) subset of all the possible values that can be provided as input to a program, or all the possible results a program can produce.
What you are describing are 'extrinsic types. There are also 'intrinsic types'.
Btw, types don't have to be sets at all. (Nor are they all isomorphic to sets. Some types describe things bigger than sets.)
For anyone trying to understand the difference between extrinsic and intrinsic definitions of sets, consider the set of birds.
Intrinsic definition:
"Birds are a group of warm-blooded vertebrates constituting the class Aves, characterised by feathers, toothless beaked jaws, the laying of hard-shelled eggs, a high metabolic rate, a four-chambered heart, and a strong yet lightweight skeleton."
Extrinsic definition:
"Birds are the set made up of: Sparrows, Pigeons, Robins, Hummingbirds, Hawks, Eagles, Parrots, Penguins, Ducks, etc..."
Hmm, I'm not sure anyone who doesn't already know will be helped by this analogy?
Though not sure whether Wikipedia does a better job:
> An intrinsic/Church-style semantics only assigns meaning to well-typed terms, or more precisely, assigns meaning directly to typing derivations. This has the effect that terms differing only by type annotations can nonetheless be assigned different meanings. [...] In contrast, an extrinsic/Curry-style semantics assigns meaning to terms regardless of typing, as they would be interpreted in an untyped language.
> The distinction between intrinsic and extrinsic semantics is sometimes associated with the presence or absence of annotations on lambda abstractions, but strictly speaking this usage is imprecise. It is possible to define a Curry-style semantics on annotated terms simply by ignoring the types (i.e., through type erasure), as it is possible to give a Church-style semantics on unannotated terms when the types can be deduced from context (i.e., through type inference). The essential difference between intrinsic and extrinsic approaches is just whether the typing rules are viewed as defining the language, or as a formalism for verifying properties of a more primitive underlying language. Most of the different semantic interpretations discussed below can be seen through either a Church or Curry perspective.
I think this is too simplistic for real-world programming languages.
For example TypeScript has the "any" and the "unknown" types. Both encompass the same set of values (any possible value which can be represented in the language), but the allowed operations are different.
C# has something similar with "object" and "dynamic".
For a static type system it makes more sense to think of a type as a set of supported operations rather than a set of values.
> For a static type system it makes more sense to think of a type as a set of supported operations rather than a set of values.
It really doesn't. 'any', 'unknown', 'object', and 'dynamic' are all 'top' in type systems (the type that is the super-type of all other types), they hold the set of all values. The fact a language assigns additional semantics based on their name is just sugar over the underlying type system, the type-system can live quite happily without names.
But even then, you could consider the name of a type a 'discriminating tag', like in discriminated unions. So, something like:
type Top = Any a
| Unknown a
| Object a
| Dynamic a
The same type, but with different states depending on the semantics of the language.
I don't know what you mean with "sugar", but the fact that several different types can represent the exact same set of possible values means that a type cannot be considered as just a set of possible values.
> The same type, but with different states depending on the semantics of the language.
This is just playing games with definitions. What you call "state" is a type in the type system of the programming language.
Or Haskell has types like `Void`, `Maybe`, and `Monad`. If you think of them as "sets of possible values", these all have no possible values. But they're very different types.
You could probably define terms such that of these, only `Void` is a "type" - for example, it's the only one that you can use directly as function inputs or outputs. (i.e. you can write a function `Void -> Int` but not a function `Maybe -> Int`.) I think that would be nonstandard, but maybe reasonable to do. But then when you explain what a "type" is you've only explained a subset of what "type theorists" talk about, which includes the others.
As I said, I think that's a reasonable but nonstandard way to define the word "type" but it doesn't make much difference - type theory concerns itself with them, whatever they're called.
It's also possible usage is just inconsistent on the subject. (Evidence for this: that second link calls constraints "type-like things", when they're just types according to me.) But my sense is that usually, people engaging seriously with type theory or advanced Haskell would call Maybe and Monad types.
(You're of course right that Maybe is a type constructor and Monad is a typeclass, but that doesn't mean they aren't also types.)
> `Maybe a` is a type-lambda abstraction (still a type)
I don't know what you mean by this - lambdas are values not types. You could argue the type of the Maybe type constructor is Type -> Type but there is no Type type in Haskell so Maybe is not a 'type' in the Haskell type system in the way e.g. String is. The separation of types and values is AFAIK the defining characteristic of non-dependent type systems, which Haskell is (for now).
> I don't know what you mean by this - lambdas are values not types.
I think they meant "`Maybe` is a type-lambda abstraction", meaning roughly "a type-level function", which seems true to me. I don't think they meant to say that `Maybe` is a type in the same way String is. (I'd agree it's not, though I'd still call it a type.)
> there is no Type type in Haskell
Incidentally there is[1], and it even has kind `Type` just like `String` does. So you can ask "what is the kind of `Maybe Type`" (it's `Type`) where you can't ask "what is the kind of `Maybe Maybe`" (`Maybe` has kind `Type -> Type` so this is a kind error).
>A type is a (possibly infinite) subset of all the possible values that can be provided as input to a program, or all the possible results a program can produce. [...] That's pretty much it.
I've often seen this reductionist simplification of "type" but I don't think it's accurate because of the emphasis on values without mentioning the rules for those values.
The extra power of "types" comes from behaviors of values.
E.g. in mathematics example, a Complex Number when only seen as "values" looks like a 2-dimensional vector. Therefore, r^2 and complex plane can appear as the same type but they are not. Complex Numbers have extra behavior rules e.g. multiplication that plain r^2 does not. (https://math.stackexchange.com/questions/444475/whats-the-di...)
For a less mathy example, would be a typical DateTime type. Yes, some underlying implementation may use a 64bit integer as an offset from an epoch but a rich datetime type would also have "behavior rules" such as adding 1 day to Saturday makes it wrap around back to Sunday because of modular arithmetic. It's the built-in behavior rules that make using a DateTime type less error-prone than manipulating raw 64bit integers.
Personal anecdote: I initially learned an incomplete and misleading idea about "types" from K&R's "The C Programming Language". From that book, I only thought of "types" as different data widths (or magnitudes). An "int" held 16bits and a "long" held 32 bits, etc. And C keywords like "typedef" futher adds to the misunderstanding of "types" because typedef is just an name alias instead of defining behavior rules.
Complex multiplication can be thought of as just a different function than real multiplication, defined *: C x C -> C or something like that, right?
> rich datetime type would also have "behavior rules" such as adding 1 day to Saturday makes it wrap around back to Sunday because of modular arithmetic.
Conceptually, it's a overloaded method, that's a function, again, with syntactic sugar. Functions are defined from one set to other. The fact that we use same names or symbols doesn't change that types, for all simple purposes, correspond to sets in math.
Really good write up. I'd add a couple of touch points:
- The art of designing type systems you describe is also heavily constrained by the practical limits of language. We could easily add more and more 'types' to a programming environment to cover more use cases, but at some point it makes the 'language' difficult when there's too many. Which is why turn to different languages for different uses.
- There's a bunch of different categories of types. This thread is full of discussion of functions and lambda calculus which is important as function types are some of the most complex, especially for 'trying to figure out at compile time' as you describe. But there's also common types like a 1 byte char, 4 byte unsigned int, or memory pointer that are more based on hardware and established standards, as well as user defined types and 'classes' which bring their own practical complexity and approaches.
> It never ceases to amaze me how theorists can take simple concepts and make them impenetrable.
Yeah, it's pretty much like those people taking a reasonable, standard car, and removing the motor to add horses instead. Who in their right mind would do that? Turns out, plenty of people in the past just did that for no reason at all.
I think you may have misunderstood my intent here. That criticism was not directed at the OP, it was sympathizing with the OP, who cited this passage:
"Linear type systems are the internal language of closed symmetric monoidal categories, much in the same way that simply typed lambda calculus is the language of Cartesian closed categories. More precisely, one may construct functors between the category of linear type systems and the category of closed symmetric monoidal categories."
That is what I was referring to when I used the word "impenetrable". I was talking about pedagogy, not substance.
The thing I was commenting about was that theorists create new vocabulary to talk about new concepts, which can then be simplified and taught more easily.
The impression that these concepts were inherently simple in the first place is the consequence of the observer standing on the shoulders of popularizers, themselves standing on the shoulders of theorists. To think that we had simple things that were made complicated essentially reverts the timeline.
Except that types are not a "new concept". The earliest programming languages already had them. To be sure, early type systems were horrible hacks and many improvements have been made, but I really don't see how knowing that "one may construct functors between the category of linear type systems and the category of closed symmetric monoidal categories" enables anyone to write code more effectively than knowing that types are (at least conceptually) subsets of data, and that some conclusions about them can be made at compile-time.
Now, I don't discount the possibility that I might be missing something, maybe even something very cool and powerful. But I have been coding for over 40 years and I have a Ph.D. in computer science, so I'm not a complete idiot. But so far no one has been able to explain to me what that thing is that I'm missing in terms that I can understand. That is what I am complaining about.
> The earliest programming languages already had them.
I'm not sure which programming language you're referring to, but as you may see in the video I posted elsewhere in this thread, the notion of computer algorithms predate transistors by a few centuries, and the notion of computability, the groundwork for types, predates transistors by a few decades.
The first people that had a stab at it were logicians, and they were used to some abstractions that probably felt as natural as code to you, while the concept of compilation wouldn't exist for another half-century.
> I have been coding for over 40 years and I have a Ph.D. in computer science, so I'm not a complete idiot. But so far no one has been able to explain to me what that thing is that I'm missing in terms that I can understand. That is what I am complaining about.
If you're looking for scientists to popularize breaking research work, you're probably barking up the wrong tree. You'll find plenty of accessible work explaining modern type systems (e.g. f# for fun and profit), it's just that this work didn't exist when scientists set about to solve this problem.
I was referring to Fortran, which distinguished between two types: floats and integers.
> The first people that had a stab at it were logicians
Yes, I know. The original article pointed that out.
> it's just that this work didn't exist when scientists set about to solve this problem.
Yes, I know that too. But it exists today and so today there isn't any reason not to avail onesself of that knowledge when engaging in pedagogy.
I have no idea what we are actually arguing about here. All my original comment was intended as was to echo the sentiment expressed in the first sentence of the original article, that's all.
I have a question that's been on the back of my mind for a while: why just types? Aren't there other things we should be able to tell the compiler so it enforces correctness better? Or a different way to tell those things? What I've seen so far are:
- Type systems of varying complexity, where you sometimes have to abuse the language in complicated ways to express constraints you want;
- Pushing complex checks to runtime, even though they should be - in principle - computable ahead of time. Or, the compiler should be able to tell you ahead of time what you need to do to ensure an assertion never fails.
- External tools like proof checkers.
I guess having types as names of constraints is useful. Then, what I'm looking for is a better "satisfies" from Common Lisp - one that would be guaranteed to run mostly arbitrary code at compile time.
It turns out that sets are a very general concept. Anything you can say about a program can be expressed in terms of sets of states that program goes through as it runs. So there is nothing you can say about a program that cannot be expressed, at least in principle, in terms of sets.
The problem is that sets are themselves Turing-complete. If you can add a member to a set, and remove a member from a set, and test if a set is empty, that is a Turing-complete set of primitives. So if you allow yourself to have a type system that is so powerful as to be Turing-complete you haven't gained anything because now the problem of debugging problems in your type system is equivalent to that of debugging problems in your programming language.
So in order to be useful, a type system has to be constrained in some way that prevents it from being Turing-complete. Choosing those constraints is the art of designing type systems. No matter what you do, it will necessarily be the case that if your type system is going to be useful at all there will be certain things it cannot express. The trick is to insure that those things are things you don't actually care about very much or, alternatively, that your language allows you to "break out" of the constraints of the type system when they become too burdensome and tell the compiler to just do what you tell it despite the fact that it can't prove there won't be errors.
Basically a lot of properties that you probably can think of that could be checked for but aren't expressible in Java types system can still be expressed using types in another system. Therefore if you want something more powerful than the types your using, use more powerful types!
It turns out that we do not really need more to reach the limits of what we can check for automatically.
You are describing types as sets, and in intensional type theory types are not sets. There is also extensional type theory, where types can be sets, but in general we are not talking about that when we speak about type theory in connection to computer science.
But regardless of ITT vs. ETT, the point of type theory is that proofs are mathematical objects. That's where the real power comes from and this is the power unityped languages lack.
I suspect that this false belief that dynamically-checked language afficionados have, of types being sets, is responsible for their disdain for statically-typed languages. If you think that types are sets, it's easy to miss what they can do.
What is "intensional type theory"? Did you mean "intentional"? I know what intentional logic is, but I've never heard of intentional type theory before (and neither has wikipedia).
Static types become less useful as the runtime truth diverges from your static model. For example, different browsers have different APIs. Your code may type check against your browser today, but that doesn't mean it will work correctly in the browser from yesterday or tomorrow, or in other browsers. Dynamic types let you smooth over these differences.
That's an argument for dynamic types, not against static types, and I think languages with both (TypeScript, ObjC) are a sweet spot.
The difference between a type and a set is often formulated by saying that types are "intensional" whereas sets are "extensional," meaning that the definition of a set imposes a constraint on what objects are qualified to be set's elements, while the definition of a type imposes a constraint on the operations (including construction) that can be performed on objects of types involved.
Yup. Exactly that. Type theorists have coopted much of the landscape of formal / mechanised mathematics, I believe much to its detriment. The problem is right there in your statement: Type systems are for static checks. This makes a lot of sense in modern programming languages, but much less so in mechanised mathematics: After all, the notion of theorem subsumes all those static checks.
Good question! I believe I have the solution for this, actually. I am just working out the foundations properly (I call it "Abstraction Logic"), but the basic direction of it is described at https://practal.com
But what is "this"? I think the only criticism of existing theorem provers at https://practal.com is that Coq uses coercions rather than subtyping. Is there a practical example where Coq just doesn't have a good equivalent for what subtypes can do?
Coercions / subtyping is a big one, because mathematics is full of quotient types and identifications. This is a very practical issue, that comes up many many times. Not necessarily if you "program" in Coq, but if you try to do math in Coq. Another one is that there is no good treatment of undefinedness. An "option" type doesn't cut it, because it pollutes everything. The question is, how can you enable undefinedness everywhere, without polluting everything? That is only possible by adjusting your logic.
Maybe this is a dated perspective now, since more modern languages like Julia are aiming for dynamic types with good run-time speed, or like nim which aim to make statically typed languages as easy to use as dynamic ones.
I use Nim, C, Python/Cython, Shell, etc., etc. After a short while Nim felt to be the fastest/most fluid development time frame of the whole bunch - while also having a strong static typing style..I find it a very "get to the point" programming language/style.
Sure, sure. Nothing is perfect. It could use stronger REPLs, one has to workaround compiler limitations occasionally, and I seem to be the only one telling people to use the TinyC/tcc backend as a default in their $HOME/.config/nim/nim.cfg or $HOME/.config/nim/config.nims for sub-second compile-times (part of "fluid"). It is very good as-is and deserves more attention than it gets.
This "mathematical interpretation" is still far too complicated for most "statically typed languages" (outside the "functional niche"). You have a handful hardware-compatible integer- and floating-point data types which can be combined into composite data structures. The compiler checks upfront whether assignments are type-compatible (which is the biggest and most important difference to dynamically typed languages).
Eh, even outside the functional niche generic types are pretty mainstream these days. Eg people reasonably expect that their language's standard library offers a sorting function that can deal with any comparable items.
And once you have that kind of functionality, you need more than just what you described.
(And, no, Go's approach doesn't cut it. Their 'generic' sorting interface only works for in-place algorithms.)
Generics are mostly just a compile-time duck-typing layer on top of the simple static typing model I described (with the purpose of getting some of the flexibility of dynamic typing back into a statically typed language).
I think the confusion might stem from C++'s templates.
Those templates can be used to do something like generics, but they are also basically duck typing at compile time.
In Haskell terms, C++'s generics are like typeclass-instances without typeclasses themselves. (I think in Java terms they would be similar to not providing interfaces. But I don't know enough about Java to see whether that's actually true.)
A type is a (possibly infinite) subset of all the possible values that can be provided as input to a program, or all the possible results a program can produce.
Type theory is about trying to figure out at compile time, if the inputs to a function are of a certain type (i.e. belong to a certain subset) what type the output will be (i.e. what subset of possible values the output will belong to).
It is not possible to figure this out in general because that would require solving the halting problem, so the art of designing type systems is choosing subsets of the data that allow you to prove useful things about programs at compile time so that you can find errors before the program runs, and eliminate run-time checks and hence make the programs run faster.
The reason people who like dynamically typed languages get frustrated with statically typed languages is that they value development speed more than they value run-time speed or avoiding of run-time errors, so they don't want to put in the extra effort needed to provide the compiler with the information it needs to do these compile-time derivations, or put up with the compiler complaining when it is unable to do them. They just want the program to run, and they're willing to pay for that with some inefficiency and run-time errors.
That's pretty much it.