7 ms·

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 value

• cjfd 5y ago
  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...
  • setr 5y ago
    JS would like to have a word with you.
    • cjfd 5y ago
      Yes, but would I like to have a word with JS? I am quite certain the answer is 'no'..... On a more serious note: JS is in the background also keeping track of types, obviously.
• branko_d 5y ago
  > they value development speed I never understood that. For anything non-trivial, development speed is increased with types: you get auto-complete, safe refactorings, code navigation etc.
  • mro_name 5y ago
    maybe you get the sunshine case out of the door quicker. But beware new-year or leap years. Or daylight saving change. Or non-ascii. I mean, who would ever care about fringe cases when you can have continuous delivery instead?
    • DeathArrow 5y ago
      Well, if it works when you deploy, maybe you get lucky and the bug will arrive after you've moved to another company. :D
    • goto11 5y ago
      I don't see how this is different between type systems. No type system I know of guarantee you handle leap years correctly.
      • mro_name 5y ago
        in real life nobody will guarantee you anything. 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.
      • mro_name 5y ago
        I apologise for the misleading example "leap year".
        • goto11 5y ago
          I'm a fan of static typing, but if people think it will protest them from logical errors like forgetting about DST, then they are actually worse off.
• TeMPOraL 5y ago
  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.
  • capitol_ 5y ago
    Lifetimes in rust fits this, they are sort of types.
  • shikoba 5y ago
    If you're interested, there is Calculus of constructions that can express anything.
  • eru 5y ago
    > Aren't there other things we should be able to tell the compiler so it enforces correctness better? Well, programming language people tend to call any kind of property you can statically check a 'type'.
    • Koshkin 5y ago
      There's static asserts.
      • eru 5y ago
        Yes. I meant the theory people would still look at that through the lens of type systems. See eg https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type
• auggierose 5y ago
  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.
  • creata 5y ago
    > Type theorists have coopted much of the landscape of formal / mechanised mathematics, I believe much to its detriment. What foundation would you rather have? And what would it do better / how would it be less "detrimental" to formal mathematics?
    • auggierose 5y ago
      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 https://practal.com
      • creata 5y ago
        > the solution for this But what is "this"? I think the only criticism of existing theorem provers at https://practal.com 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?
        • auggierose 5y ago
          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.
• bryanrasmussen 5y ago
  >They just want the program to run, and they're willing to pay for that with some inefficiency and run-time errors. or they don't make the kinds of errors that static typing helps defend against so for them it is an impediment.
• twelvechairs 5y ago
  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.
• a_imho 5y ago
  1. Reasoning about a subset of values is usually easier. 2. Modeling the domain with types, making erroneous states unrepresentable is helpful 3. Carefully chosen types help with communicating intent
• goto11 5y ago
  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.
  • philh 5y ago
    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.
    • lkitching 5y ago
      Maybe and Monad are not types - Maybe is a type constructor and Monad is a type class.
      • philh 5y ago
        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. But to support my "nonstandard" claim: * https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/type-type https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compil... mentions "Types (possibly of higher kind); e.g. [Int], Maybe" * https://limperg.de/ghc-extensions/#polykinds https://limperg.de/ghc-extensions/#polykinds talks about "types of different kinds", using Int and Monad as examples. * https://en.wikipedia.org/wiki/Kind_%28type_theory%29 https://en.wikipedia.org/wiki/Kind_%28type_theory%29 says "the type [] (list) is a type constructor". It uses the terms "data type" and "proper type" for what I think you simply want to call "type". 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.)
• pyrale 5y ago
  > 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.
  • lisper 5y ago
    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.
    • pyrale 5y ago
      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.
      • lisper 5y ago
        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.
• flohofwoe 5y ago
  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). That's pretty much it.
  • eru 5y ago
    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.)
    • flohofwoe 5y ago
      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).
      • reuben364 5y ago
        Generics are not really the statically typed answer to duck-typing. Subtyping with structural types, such as in TypeScript, is.
        • eru 5y ago
          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.)
• eru 5y ago
  Be careful, that's just one way of looking at things. See https://lispcast.com/church-vs-curry-types/ https://lispcast.com/church-vs-curry-types/ or https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#Intrinsic_vs._extrinsic_interpretations https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#I... > 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.)
  • nicoburns 5y ago
    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..."
    • eru 5y ago
      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.
• deleted 5y ago
  [deleted]
• jasode 5y ago
  >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-difference-between-mathbbr2-and-the-complex-plane 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.
  • chakkepolja 5y ago
    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.
• 4ad 5y ago
  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.
  • lisper 5y ago
    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).
    • 4ad 5y ago
      At the risk of more confusion https://ncatlab.org/nlab/show/intensional+type+theory https://ncatlab.org/nlab/show/intensional+type+theory. As a gentle introduction to modern type theory I would recommend https://arxiv.org/abs/1601.05035 https://arxiv.org/abs/1601.05035.
• DougBTX 5y ago
  > more than they value run-time speed 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.
  • cb321 5y ago
    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.
• Koshkin 5y ago
  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.
• ridiculous_fish 5y ago
  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.