13 ms·

Where Do Type Systems Come From?

285 points by philix001 9y ago

winter_blue 9y ago
"Even though theoretically, type theories and type systems are not enough to prevent all the problems in logic and programming, they can be improved and refined to prevent an increasingly number of problems in the practice of logic and programming. That means the research for better practical type systems is far from over!" This is great point, and I think it is absolutely worthwhile to put time into researching better, more powerful type systems. Tony Hoare said[1] that his research into formal systems and his hope that the pr Framing world would embrace these new innovations that increase safety and reliability was futile, but I think what we need is a new approach, with particular care given to practicality and adoptability. [1] https://en.wikipedia.org/wiki/Tony_Hoare https://en.wikipedia.org/wiki/Tony_Hoare
smcl 9y ago
I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.
- agumonkey 9y ago
  To each his own path. Maybe you'll change course, maybe not, maybe type theory will evolve (HoTT comes to mind).
  - miguelrochefort 9y ago
    I can't seem to grasp HoTT. Are there any approachable resources on the subject?
    - agumonkey 9y ago
      I only read two pages on homotopy so far, I cannot answer that :)
    - alimw 9y ago
      Have you tried reading the articles linked to on this page? http://www.bris.ac.uk/arts/research/projects/homotopy-type-theory/ http://www.bris.ac.uk/arts/research/projects/homotopy-type-t...
    - stepik777 9y ago
      There is an official book which is very well written. I remember that I started to read it several years ago and was surprised that I actually can understand most of the things.
- Kenji 9y ago
  It's never too late to bother trying. If you think it'll benefit you in life, just go for it and study it.
  - AnimalMuppet 9y ago
    If. I suspect that smcl can't get excited about type systems because of not seeing the benefit. For me, types are sets of possible values, plus sets of valid operations on those values. I don't much care where they come from. As far as I am concerned, they are an engineering construct to make programming easier and safer, and are interesting only to the degree that they accomplish those goals. Any connection to pure math is completely incidental; if there were no such connection, it would not make (programming) types any less useful. Now, math often gives deeper insight into what's going on, and enables you to create more powerful (useful) abstractions. But if the useful abstractions don't correspond perfectly to types as used by mathematics, I don't care.
    - jholman 9y ago
      Yes, precisely. I'm very interested in theory (by the standards of non-academics). I'm very interested in pragmatic type systems. I've spent a few hundred hours on trying to learn type theory, in the mathematical sense. The only thing I have personally found useful, so far, in type theory, is the notion of sum types and product types. But that's just jargon for things I was able to deduce from a shallow study of many programming languages, so even that has not been that useful to me. On the other hand, I entirely agree with you, that what a type is to a programmer is a set of values and a set of valid operations on those values. Exactly. That's what types mean when you're working close to the metal ("this value is meaningful as a 16-bit float; if you try to dereference it, the consequences are mightily hard to reason about"). That's what types mean when you're talking about the function signatures of higher-order functions that use generic types. That's what types mean when describing statically-typed variables, and what types mean when describing dynamically-typed values. I see some signs that a few other people share my interest. For example, using dependent types to e.g. specify that two sequences can only be zipped if they are of the same length; that's a useful type-check, and if it can be determined statically, that's great (that's a toy example, of course). Unfortunately, most of the languages that contain these features seem remarkably impenetrable. I am very interested in situations where math reveals underlying truths about the universe. Like you, I'm so-far unpersuaded that mathematical type theory is a useful avenue to learning about powerful abstractions about types in programming.
- philix001 9y ago
  I don't think it's common for programmers to have in depth opinions about type systems. And most of the ones who do may not really know what they're talking about.
- ridiculous_fish 9y ago
  > I get that these underpin the technology we as programmers use every single day Is this actually true? Of course Haskell, Idris, etc. leverage type theory, but how much type theory underlies the type systems of widespread practical languages like C# or Java? Can something like C++'s SFINAE be grounded in type theory, or is it just a hack?
  - leshow 9y ago
    C++ metaprogramming might not be pretty, but it's extremely expressive, I'd be surprised if it didn't have some kind of type theoretic background.
- Drup 9y ago
  I believe you get an actual interest for type systems when you start using a rich one. Unfortunately, most mainstream languages have very poor type systems. In particular, it will come naturally over time if you start using languages like OCaml, F#, Scala, Rust, Haskell, ...
- hinkley 9y ago
  I learned set theory and discrete math from this guy: http://internethalloffame.org/about/advisory-board/cl-liu http://internethalloffame.org/about/advisory-board/cl-liu Easily my second favorite instructor, possibly my favorite. I felt pretty prepared to deal with analysis and design in statically typed languages just from that grounding in set theory and logic. Fond of saying things like, "We have a box. What's inside that box? Another box. What's inside that box? We don't care." Now retired, he was an early proponent of distance learning, so surely some of his stuff is accessible still.
- currymj 9y ago
  There’s the technical aspects of the fact that every language has to have some notion of “type”. And seemingly interpreted languages might be JIT-compiled etc. This is of interest if you care about the implementation of languages. Then there’s the opinions that users of languages with more elaborate, expressive type systems have, like how some people really enjoy Haskell or Elm because they feel that the type system helps them express their ideas clearly, avoid errors, and aids refactoring and maintenance. If you’re worried about this one, don’t I guess? If you can use dynamic languages to achieve your goals, and you like them, then that’s fine! There are plenty of languages you can play with if you want to get a feel for programming with types. Even Java 8 and C++11 are decent at this point (I’m sure a Haskell programmer is fuming right now). Then there’s like, a few thousand people in the world who have well-informed opinions on research into the theory of programming languages, the Curry-Howard correspondence between types and proofs. Also a lot of Hacker News posters who have heard these words. Some of them pretend like they know what they’re talking about.
  - acchow 9y ago
    > There’s the technical aspects of the fact that every language has to have some notion of “type” This isn't true. There are no types in lisp or untyped lambda calculus.
    - naasking 9y ago
      Actually, there's one type.
      - acchow 9y ago
        If you're going to shove the system into a typed model, then sure there is one type. But then you've kind of missed the point...
        naasking 9y ago
        If you're going to answer the question of whether a language has types, then you're already trying to see how it can be shoved into types. It's presupposed by the question itself. You literally have to count the types by analyzing the grammar. So for the lambda calculus, you have lambda=1, halt. So does a single type mean no types or literally one type? What's the advantage of thinking that 1 type actually equals 0 types? I don't see any, so in my mind, all languages are unityped or have a richer type structure. Whether a richer type structure is desirable is a separate question.
- bykovich2 9y ago
  Type systems /don't/ underly the technology we use every day. The vicissitudes of real computer architectures do -- and those ain't type systems.
- ianamartin 9y ago
  One of the things that's so wonderful about writing software as a profession is that there is a ridiculously huge array of use cases for different languages and styles. There's nothing wrong with not caring about type systems if they don't make your life or your job better or worse. As long as you enjoy what you are doing, everything else is optional. I didn't start caring about type systems until I started running into cases where I really wished for a static one (when I was working on a large system in Python) and later when I was prototyping things where I had to make a lot of guesses in C#. Both situations frustrated me, and then I got to start really caring a lot about type systems. To a certain extent, I think it's human nature that we often don't really start caring about things that much until we experience real, personal frustration with them. Then we start caring a lot. The reason you see so many people weighing in on this here on HN, is that many regulars are the kind of person to start feeling pain very very soon and over small inconveniences where other people will just sort of deal with the minor inconvenience and focus on other aspects. One attitude is not better than the other, nor is one more ideologically pure or a marker of a better programmer or engineer. The only thing it implies is different pain thresholds. Depending on your area of focus as a developer a low or a high threshold could be either a benefit or a drawback. A language designer needs to have a very low threshold. A front-end developer/designer can afford to have a very high threshold and focus on things besides being provably correct. One of the things I like the most about software engineering is that there are opportunities for joy and discovery for everyone. And as careers progress, you can easily find yourself caring about different things at different times, and there's nothing wrong with that. There's nothing to be ashamed of any more than you should be ashamed of preferring strawberry to chocolate ice cream. (Although, in keeping with tradition here on HN, if you say that you prefer strawberry ice cream, you are dead to me and practically Hitler. :).
- dannyobrien 9y ago
  I feel your pain: after bouncing off Haskell many times, I found that Elm was a great entry into a more practical and narrow way of experimenting with the benefits. Now I'm reading through the new Idris book, which has the same practical approach to more complex (to me) concepts.
- coldtea 9y ago
  >I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. Not even 1/10th of HN has that. Tons of business types, lowly JS programmers, designers, sys-admin types, old-school programmers in C/C++, etc around.
- leshow 9y ago
  What languages have you tried? I think once you experience a language with types outside of the run of the mill Java/C#, you will get more excited about it. Ocaml, Rust, Haskell, Purescript, etc. Haskell for me was the one that got me excited about types.
  - z3t4 9y ago
    ive only used vbscript and javascript extensibly. when ive tried java and #C ive been annoyed by the verbosity of types. and when looking at haskel or ocaml im just confused. for me types are an optimization or extra documentation for undescriptive naming, like str x, int y, list z. vs. name,age,friends. so i want to know what im missing, will there be less bugs and regressions? will i be more productive ?
    - leshow 9y ago
      > for me types are an optimization or extra documentation for undescriptive naming, This is one of those things where you should try to reserve judgement about it because your experience is so limited. Modern typed languages often don't even require you to write the type, because of type inference. > will there be less bugs and regressions? will i be more productive ? The idea with static analysis is that you're pushing more errors into the type system so it's caught at compile time rather than runtime. Everyone will answer this differently. IMO a dynamic type system doesn't make you more productive because the same invariants you have from not having an explicit type still exist in the code, they just go unchecked. For example, if I write a function to add 1 to a number, in a dynamic language if I pass a string I'll get some output that is invalid if I'm expecting the result to be a number elsewhere. Types let you encode those invariants. But encoding simple types and primitives is really just scratching the surface, I could ramble on for ages here but you should just dive into a language with a good type system (like Haskell or Ocaml like you mentioned) and stick with it long enough to give it a chance. It's so much more than just being and to say 'int' or 'string'.
      - kazinator 9y ago
        Speaking of adding to a number, in some dynamic languages, you can add 3/5 to 7/5 and the result will be 2, of type integer, indistinguishable from the object produced by a literal 2. That 3/5 and 7/5 come from some run-time source, so the result type can't be statically hard-coded to integer or rational or whatever. And so now on the static side you're into variant types and "maybes" and other junk creating an incomprehensible soup which basically Greenspuns dynamic typing in a way that will get your name cursed by subsequent maintainers.
pier25 9y ago
Reminded me of Gödel's incompleteness theorems. First incompleteness theorem Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F. Second incompleteness theorem For any consistent system F within which a certain amount of elementary arithmetic can be carried out, the consistency of F cannot be proved in F itself.
- igravious 9y ago
  Honest question. What in the article prompted you to think about Gödel and his theorems? Why were you reminded?
  - deleted 9y ago
    [deleted]
  - Jtsummers 9y ago
    Probably this part from the article: > Similarly, type theory wasn’t enough to describe new foundations for mathematics from which all mathematical truths could in principle be proven using symbolic logic. It wasn’t enough because this goal in its full extent is unattainable.
  - munificent 9y ago
    I'm not sure why pier25 was reminded, but Russell's type theory and Gödel's incompleteness theorem are closely related. They both arose in response to the foundational crisis in mathematics [1]. Russell stumbled onto Russell's paradox (among others) and it shook mathematicians' confidence that everything in math was built on top of a perfectly consistent and stable foundation. If you can define a set that it "the set of sets that don't contain themself" then what other kind of crazy talk can you say in math? How do you know proven things are true and false things can't be proven in the face of weirdness like that? Russell tried to solve the problem by inventing type theory. Types stratify the universe of values such that "the set of sets that don't contain themself" is no longer a valid statement to make. Meanwhile, Gödel went and proved that, sorry, no, math is not consistent and complete. There are statements that are true but which cannot be proven. [1]: https://en.wikipedia.org/wiki/Foundations_of_mathematics#Foundational_crisis https://en.wikipedia.org/wiki/Foundations_of_mathematics#Fou...
agumonkey 9y ago
Types are close to adjoint functors / adjunctions and partial evaluation. Assigning restricted information to part of a structure to gain knowledge through limitation (math).
- igravious 9y ago
  The category-theory window onto the world of types only appeals to a small subset of human minds. For the average programmer you may as well be spouting gibberish because the average programmer will have no way to evaluate the claims (if any) you are making. Note, I am saying that you may as well be and not that you are. Please do not misunderstand me. Types systems certainly are formal theoretical systems but I personally have come to believe that the majority of coders are ill-served by the mathematical leanings of type theorists. I'm not sure I can explain myself better than that at the moment.
  - kazinator 9y ago
    Type theorists are people who understand arrows very well -- as long as those arrows aren't pointers. :)
    - igravious 9y ago
      ba-dum tss! are you here all week?
      - kazinator 9y ago
        Sure---if catering keeps that sirloin roast coming for another seven days. Have you tried it?
  - agumonkey 9y ago
    Do not worry I understand 99% of your message. It's indeed a land far far away from the everyday coding of the majority of programmers. Unless they start digging, which I did. If you take code as data (lisp roots showing) you start to want to reason about it and quickly you end up reading about FP, denotations, different forms of evaluations, the value of metadata (type or else). Now I believe there's an artificial split between math leaning people and pragmatics, the former end up as PhD, the latter in IT or close. But in reality the average coder could understand and even enjoy the land of abstractions, it's just that the river he swims in isn't flowing there so one has to run against the flow. Not to say that ideals are the only-tru-way.
simplify 9y ago
If you haven't thought much about type systems but want to understand what the big deal is, I wrote a post specifically for you [1]. It draws motivation for wanting a good static type system from first principles. [1] https://gilbert.ghost.io/type-systems-for-beginners-an-introduction/ https://gilbert.ghost.io/type-systems-for-beginners-an-intro...
threepipeproblm 9y ago
I loved this because I have read most of the source material in the context of logic, but never made the lead to type theory in computer science.
zzzcpan 9y ago
"Even though theoretically, type theories and type systems are not enough to prevent all the problems in logic and programming, they can be improved and refined to prevent an increasingly number of problems in the practice of logic and programming." It's actually just a belief. Nothing suggests that type systems and type theories can be improved to be practical at preventing bugs. I'd say it's the opposite, even with as much understanding about the nature of bugs as we have today, they don't look very promising, unlikely to make it even into the top ten of other different approaches.
- dungle6 9y ago
  Lolwut?
  - chroem- 9y ago
    He's right. The current type theory crazy is just another in a long line cargo cult programming fads. First it was pure OOP for everything, then it was pure FP for everything, and now it's types for everything. Yes they can be useful, but it's disingenuous to act like they're a cure-all. Most bugs aren't type related, and you're adding additional mental overhead with these extremely elaborate type systems.
    - dpratt71 9y ago
      What is "he" right about, exactly? You say "yes they can be useful", but that's not the impression I get from OP. I am also confused because the very quote OP is responding to states that "...type systems are not enough to prevent all the problems in logic and programming...". Do you consider that acting like type systems are a cure-all?
    - Jtsummers 9y ago
      Types aren't new. As the article discusses they date back over a century at least in math and logic. Within programming, we've had them in every major language for decades. The first big push for strong and expressive type systems is from the functional programming work which led to the ML family and the work that made Pascal and Ada on the imperative (and later OO variants) side, which dates back some 40-50 years now.
miguelrochefort 9y ago
Don't they teach this stuff in school?
- igravious 9y ago
  No they don't. Only in some. Only if you're lucky.
- 0xCMP 9y ago
  The school I went to barely taught C/C++ and the absolute minimum of PHP, CSS, Linked Lists, and Hash Maps. Very sad that so many actually smart people can't graduate knowing much just doing their course work. Let alone imagine those who lack off a bit and still pass. Unless you're programming on your own, like I was along with a few others, you graduate possibly in debt and completely unprepared. So no, they never get in to this stuff.
- lgas 9y ago
  Not everybody goes to school, and not everybody that does takes computer science.
- empath75 9y ago
  I've never taken a CS class.
- khedoros1 9y ago
  We danced around the edges of set theory. Symbolic logic. Combinatorial and sequential logic (especially as applies to logic circuit design). Examples of a few families of type systems, how to use them, and the practical differences between them. We didn't tend to dive deeply into the mathematical underpinnings.
deleted 9y ago
[deleted]
a-nikolaev 9y ago
Watch Oregon Programming Language School lectures "Basic Proof Theory" by Frank Pfenning. https://www.cs.uoregon.edu/research/summerschool/summer15/curriculum.html https://www.cs.uoregon.edu/research/summerschool/summer15/cu... Very clean and easy to follow video lectures on the relation between, types, programs, and logical proofs. One does not need functors and monoids to appreciate the beauty of functional type systems. (And to see why such type systems are indeed discovered rather than invented.)
- z1mm32m4n 9y ago
  I second this. Frank's material is always thorough and approachable. He's designed and taught many courses at CMU, and his lecture notes for them are never less than impeccable.
incan1275 9y ago
I share the author's frustration with wikipedia sometimes - people usually go to wikipedia for a distilled, comprehensible description of the subject matter. What he quoted was certainly not comprehensible, even to someone well-educated in CS foundations.
- owebmaster 9y ago
  I like it because of it. If what I found in wikipedia was the "easiest" description, I'd find it lacking. It is better to not understand everything on the first read than understanding almost nothing because of lack of profoundity.
georgewsinger 9y ago
Nice article. I especially liked: > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter. Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool. Also, I never thought of "higher-order functions" as breaking into a countable hierarchy of nth-order functions, which is an interesting thought. In Haskell the hierarchy would start off as zerothOrderFunction :: a firstOrderFunction :: a -> b SecondOrderFunction :: a -> (b -> c) SecondOrderFunction' :: (a -> b) -> c In general, an nth-order function is a function which either 1. Takes an (n-1)th order function as an input and returns a simple type. 2. Takes a simple type as an input and returns an (n-1)th order function as an output. The upshot is that typed programming languages not only catch bugs, but prevent you from legally expressing many non-sensical expressions (analogous to the set theory paradoxes). For example, consider the expression (\x -> x x) (\x -> x x) If you expand this expression, it reduces to itself: (\x -> x x) (\x -> x x) == (\x -> x x) (\x -> x x) In a purely untyped language, this expression would be legal. But what would be its meaning? Arguably, it is non-sense, and should be excluded from the set of legally expressible expressions. The way to do this is through a type system. And indeed, if you typed this statement into a Haskell REPL you would get a type error; this statement can actually be proven to be untypable (IIRC). On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. It would therefore be interesting if somebody found an expression which was both (i) meaningful and (ii) only expressible in an untyped language. You would then have an argument for untyped languages :-)
- kmill 9y ago
  > > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter. > Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool. In case it's not clear, it's just that it eventually ends up with a run time error (the talk about runFunction being a second-order function is just an explanation for why you should expect it to end up with a run time error). The evaluation is program3() == runFunction(runFunction) == runFunction(1) == 1(1) == Error: func (with value 1) is not a function
Ar-Curunir 9y ago
This article was very well written. It finally clicked for me why "hugher-order functions" are named the way they are. Any more articles in this vein?
OJFord 9y ago
Distinctly unimpressed by this post. The author seems to have an axe to grind with mathematicians as a class, which, as we would have been told in school, isn't 'big or clever'. The whole of programming, nevermind types, perhaps the most mathematical part of modern programming, arises from mathematics. There's some good history here, but the early paragraphs in particular are a display of ignorance if not arrogance. The author quotes Newton, the very chap who's said to have said he merely stood on the shoulders of giants (to 'see' such insight). Any programmer in the 21st century stands on the shoulders of mathematicians and computer scientists of the 20th,; who were in turn standing on the shoulders of the mathematicians of the 19th centuries.
- pertymcpert 9y ago
  I really don't think they have an axe to grind. What do they say that's incorrect? Their point is that much of what we see as type theory is inaccessible to the average programmer. When we say that some field is inaccessible, we don't blame the reader trying to understand. At the same time we're not saying that the field is wrong either, but that communication could be improved.
- bogomipz 9y ago
  >"Distinctly unimpressed by this post. The author seems to have an axe to grind with mathematicians as a class, which, as we would have been told in school, isn't 'big or clever'." I thought it was intended to speak to people who might be intimidated or feel obtuse when they encounter really dense academic texts when trying to learn more about type systems as it relates to programming. As such I really appreciated it. I didn't think the author was grinding any axes at all, quite the contrary.
  - OJFord 9y ago
    I've no problem with that, it was the opening quotation, accompanying graphic, and following paragraph which read - to me, though I appreciate I may not have read it as it was intended - quite disrespectfully toward mathematicians. Among whom I cannot count myself, for whatever it's worth.
bogomipz 9y ago
What a great piece! I wish the author would expand on this piece with either more installments or a even short book. I find myself interested in type systems as it relates to programming language design but I haven't found much middle ground between the basic types described in introductory texts about a language and the opposite extreme heavy academic texts such as the ones the author is breaking down in this article. Can anyone recommend any other such middle ground resources on type systems and type system theory?
- naasking 9y ago
  What do you consider basic? Algorithm W for ML type inference is pretty basic, but powerful too. Or are you looking for something even more expressive?
  - bogomipz 9y ago
    What I meant by basic was the description of types provided by a language - usually in an introductory text you might read when learning a new language. I probably didn't articulate that correctly. But I guess what I was referring to as a "middle ground"qa any resources for learning about types systems written in a similar approachable tone like this article. This was another article I read recently that I thought was similarly accessible on the subject of types systems: https://medium.com/@thejameskyle/type-systems-structural-vs-nominal-typing-explained-56511dd969f4 https://medium.com/@thejameskyle/type-systems-structural-vs-... So I guess I'm wondering if there exists such a book or series that might allow one to further their knowledge of type systems without requiring university study.
    - naasking 9y ago
      Types and Programming Languages is the go to book, and it's very accessible despite being a textbook: https://mitpress.mit.edu/books/types-and-programming-languages https://mitpress.mit.edu/books/types-and-programming-languag... You can find some earlier PDF drafts online if you Google.
      - 9y ago
dvt 9y ago
It's a common misconception that Russell/Whitehead "invented" type theory. In fact, Frege had already made the very insightful distinction between functional and non-functional types in the 1890s -- this was the key development that Russell based his hierarchy of types on. See "Function and Concept" (1891)[1]. It was a growing and communal sentiment that a (meta-)theory of types would make certain mathematical concepts more palatable. If anything, I think the conceptual father of type theory is Gottlob Frege, and Alonzo Church was the first to apply it concretely. [1] http://fitelson.org/proseminar/frege_fac.pdf http://fitelson.org/proseminar/frege_fac.pdf
- rntz 9y ago
  It seems to me Frege understood the need in mathematics to talk about many different kinds of thing - numbers, truth-values, functions, and so forth - and to distinguish which kind of thing you are talking about; but not the necessity to use types (or other methods) to avoid circularity. Indeed, it is precisely the mistake Frege made in his attempt to axiomatise logic and mathematics and which led to Russell's paradox, that motivated Russell (and Whitehead)'s theories of types. Frege certainly articulated a clear notion of what a function is, which is significant.
sriram_malhar 9y ago
I found Tomas Petricek's essay on "Against a universal definition of 'Type'" very informative. He argues that the word 'type' has shifted shape many times since Frege/Russel, in that the intuition behind them is different. He also argues that multiplicity of definition is a good thing. http://tomasp.net/academic/papers/against-types/ http://tomasp.net/academic/papers/against-types/
kronos29296 9y ago
Nice article about type theory. > Why there’s so much research around types if perfectly applying them to programming languages is impractical? Somehow Haskell does this perfectly. Whaddya say to that?
- coldtea 9y ago
  I say, citation needed. Who said "Haskell does it perfectly"? Not to mention the mental overhead of Haskell (which is also not optimal).
  - aleden 9y ago
    Yeah, what the fuck? Most software engineers just want to get shit done quickly so they can go home to their wife and kids.
    - aleden 9y ago
      If you think this merits a downvote please tell why. Excuse my french.
visarga 9y ago
Types aren't just for programming and philosophy. Strongly Typed Neural Networks are also a thing. https://arxiv.org/abs/1602.02218 https://arxiv.org/abs/1602.02218
visarga 9y ago
TL;DR - Type theory == being careful about the domain a function can be applied in (adding meters to seconds or strings to sets should not be possible).
drc0 9y ago
> That’s the equivalent of writing type annotations for programming functions. And the goal is avoiding bugs instead of logical contradictions. mh, given Curry–Howard correspondence, aren't those the same? so the goal is indeed not having logical contradictions?
- Sharlin 9y ago
  Yes. But it's a rare programmer, or even a programming language designer, who thinks of well-typed programs in terms of proving theorems.
- philix001 9y ago
  They are. I avoided introducing an explanation of Curry-Howard isomorphism because I think that would not be very intuitive to many people because the most commonly used type systems have very little power to express logical properties about the program. I may write another article about this.
sgt101 9y ago
Type Systems come from Russel - yup. But the notion of Type has an interesting origin in the west as well (I would love to read/understand histories of this concept from other cultures, but I am ignorant for now). My reading is that it was invented by Scotus as Haecceity ! This was required by Catholic Christianity because of the difficulty that The Creed introduces about the identity of God - there are three entities which represent God, the Trinity - how to account for this? Well; the thisness of God is joined with the thisness of man, the thisness of the creator and the thisness of the thing which is motion (I have never understood The Holy Spirit). You can think of this as multiple inheritance! Theologians then had to account for "why three" as you can carry on making aspects of god with this mechanism infinitely, god the mother, god the lover, god the hunter and so on. But there are three - why? The answer was provided by Scotus's student Occam, entities should not multiply beyond necessity and hence there are three aspects of god because it is necessary for creation that there are. The fun bit it that this procession of thought is somewhat guessed at because writing things like this down or debating them publically was a quick route to the afterlife via a bonfire!
- lists 9y ago
  > The fun bit it that this procession of thought is somewhat guessed at because writing things like this down or debating them publically was a quick route to the afterlife via a bonfire! Theatre and Philosophy have always been able to have a lively chat with one another
Animats 9y ago
There's another approach, from Boyer and Moore. Boyer and Moore built up mathematics from constructs at the Peano axiom level (zero, add1, etc.) plus recursive functions that must terminate. It's constructive mathematics; there are no quantifiers, no ∀ or ∃. [1] They built an automatic theorem prover in the 1970s and 1980s that works on this theory. (I recently made it work on Gnu Common LISP and put it on Github, so people can run it again.)[2] In Boyer-Moore theory, all functions are total - you can apply any function to any object. Types are predicates. Here's a definition of ORDERED for a list of number: (DEFN ORDERED (L) (IF (LISTP L) (IF (LISTP (CDR L)) (IF (LESSP (CADR L) (CAR L)) F (ORDERED (CDR L))) T) T)) If L is not a list, it is considered to be ordered. This makes it a total function, runnable on any input, even though the result for the "wrong" type is not useful. This provides the benefits of types without requiring a theory of types. It's a very clean way to look at the foundations of mathematics. It's simpler than Russell and Whitehead. When you prove things using definitions like this, there's a lot of case analysis. This gets worse combinatorially; a theorem with four variables with type constraints will generate at least 2⁴ cases, only one of which is interesting. Most of the cases, such as when L is not a list, are trivial, but have to be analyzed. Computers are great at this, and the Boyer-Moore prover deals with those cases without any trouble. But it went against a long tradition in mathematics of avoiding case analysis. That made this approach unpopular with the generation of pre-computer mathematicians. Today, it would be more acceptable. (It's fun to run the Boyer-Moore prover today. In the 1980s, it took 45 minutes to grind through the basic theory of numbers. Now it takes a few seconds.) [1] https://www.amazon.com/Computational-Logic-Robert-S-Boyer/dp/1483236528 https://www.amazon.com/Computational-Logic-Robert-S-Boyer/dp... [2] https://github.com/John-Nagle/nqthm https://github.com/John-Nagle/nqthm
- kazinator 9y ago
  If every operation can have any type arguments applied to it and does something sensible with no compiler or run-time error ... good luck debugging, surely. What happens with OOP? Every class has to understand how to "bark", not only the dog class? If any class can somehow "bark" without throwing an exception, that may not be in alignment with the programmer's intent, or promote the furtherance of his or her goals in any way. For intance, the intent may be that the programmer wanted to ask the local variable dog to "bark", but misspelled it as ndog and the integer which counts the number of dogs was asked to bark instead. There is much value in identifying the problem that an integer doesn't bark.
Draco_Au 9y ago
Sexy! in today's hustle, Grothendieck Groupoids are the place to be. :toocool

285 points by philix001 9y ago

"Even though theoretically, type theories and type systems are not enough to prevent all the problems in logic and programming, they can be improved and refined to prevent an increasingly number of problems in the practice of logic and programming. That means the research for better practical type systems is far from over!" This is great point, and I think it is absolutely worthwhile to put time into researching better, more powerful type systems. Tony Hoare said[1] that his research into formal systems and his hope that the pr Framing world would embrace these new innovations that increase safety and reliability was futile, but I think what we need is a new approach, with particular care given to practicality and adoptability. [1] https://en.wikipedia.org/wiki/Tony_Hoare https://en.wikipedia.org/wiki/Tony_Hoare

smcl 9y ago

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

agumonkey 9y ago
To each his own path. Maybe you'll change course, maybe not, maybe type theory will evolve (HoTT comes to mind).
- miguelrochefort 9y ago
  I can't seem to grasp HoTT. Are there any approachable resources on the subject?
  - agumonkey 9y ago
    I only read two pages on homotopy so far, I cannot answer that :)
  - alimw 9y ago
    Have you tried reading the articles linked to on this page? http://www.bris.ac.uk/arts/research/projects/homotopy-type-theory/ http://www.bris.ac.uk/arts/research/projects/homotopy-type-t...
  - stepik777 9y ago
    There is an official book which is very well written. I remember that I started to read it several years ago and was surprised that I actually can understand most of the things.
Kenji 9y ago
It's never too late to bother trying. If you think it'll benefit you in life, just go for it and study it.
- AnimalMuppet 9y ago
  If. I suspect that smcl can't get excited about type systems because of not seeing the benefit. For me, types are sets of possible values, plus sets of valid operations on those values. I don't much care where they come from. As far as I am concerned, they are an engineering construct to make programming easier and safer, and are interesting only to the degree that they accomplish those goals. Any connection to pure math is completely incidental; if there were no such connection, it would not make (programming) types any less useful. Now, math often gives deeper insight into what's going on, and enables you to create more powerful (useful) abstractions. But if the useful abstractions don't correspond perfectly to types as used by mathematics, I don't care.
  - jholman 9y ago
    Yes, precisely. I'm very interested in theory (by the standards of non-academics). I'm very interested in pragmatic type systems. I've spent a few hundred hours on trying to learn type theory, in the mathematical sense. The only thing I have personally found useful, so far, in type theory, is the notion of sum types and product types. But that's just jargon for things I was able to deduce from a shallow study of many programming languages, so even that has not been that useful to me. On the other hand, I entirely agree with you, that what a type is to a programmer is a set of values and a set of valid operations on those values. Exactly. That's what types mean when you're working close to the metal ("this value is meaningful as a 16-bit float; if you try to dereference it, the consequences are mightily hard to reason about"). That's what types mean when you're talking about the function signatures of higher-order functions that use generic types. That's what types mean when describing statically-typed variables, and what types mean when describing dynamically-typed values. I see some signs that a few other people share my interest. For example, using dependent types to e.g. specify that two sequences can only be zipped if they are of the same length; that's a useful type-check, and if it can be determined statically, that's great (that's a toy example, of course). Unfortunately, most of the languages that contain these features seem remarkably impenetrable. I am very interested in situations where math reveals underlying truths about the universe. Like you, I'm so-far unpersuaded that mathematical type theory is a useful avenue to learning about powerful abstractions about types in programming.
philix001 9y ago
I don't think it's common for programmers to have in depth opinions about type systems. And most of the ones who do may not really know what they're talking about.
ridiculous_fish 9y ago
> I get that these underpin the technology we as programmers use every single day Is this actually true? Of course Haskell, Idris, etc. leverage type theory, but how much type theory underlies the type systems of widespread practical languages like C# or Java? Can something like C++'s SFINAE be grounded in type theory, or is it just a hack?
- leshow 9y ago
  C++ metaprogramming might not be pretty, but it's extremely expressive, I'd be surprised if it didn't have some kind of type theoretic background.
Drup 9y ago
I believe you get an actual interest for type systems when you start using a rich one. Unfortunately, most mainstream languages have very poor type systems. In particular, it will come naturally over time if you start using languages like OCaml, F#, Scala, Rust, Haskell, ...
hinkley 9y ago
I learned set theory and discrete math from this guy: http://internethalloffame.org/about/advisory-board/cl-liu http://internethalloffame.org/about/advisory-board/cl-liu Easily my second favorite instructor, possibly my favorite. I felt pretty prepared to deal with analysis and design in statically typed languages just from that grounding in set theory and logic. Fond of saying things like, "We have a box. What's inside that box? Another box. What's inside that box? We don't care." Now retired, he was an early proponent of distance learning, so surely some of his stuff is accessible still.
currymj 9y ago
There’s the technical aspects of the fact that every language has to have some notion of “type”. And seemingly interpreted languages might be JIT-compiled etc. This is of interest if you care about the implementation of languages. Then there’s the opinions that users of languages with more elaborate, expressive type systems have, like how some people really enjoy Haskell or Elm because they feel that the type system helps them express their ideas clearly, avoid errors, and aids refactoring and maintenance. If you’re worried about this one, don’t I guess? If you can use dynamic languages to achieve your goals, and you like them, then that’s fine! There are plenty of languages you can play with if you want to get a feel for programming with types. Even Java 8 and C++11 are decent at this point (I’m sure a Haskell programmer is fuming right now). Then there’s like, a few thousand people in the world who have well-informed opinions on research into the theory of programming languages, the Curry-Howard correspondence between types and proofs. Also a lot of Hacker News posters who have heard these words. Some of them pretend like they know what they’re talking about.
- acchow 9y ago
  > There’s the technical aspects of the fact that every language has to have some notion of “type” This isn't true. There are no types in lisp or untyped lambda calculus.
  - naasking 9y ago
    Actually, there's one type.
    - acchow 9y ago
      If you're going to shove the system into a typed model, then sure there is one type. But then you've kind of missed the point...
      - naasking 9y ago
        If you're going to answer the question of whether a language has types, then you're already trying to see how it can be shoved into types. It's presupposed by the question itself. You literally have to count the types by analyzing the grammar. So for the lambda calculus, you have lambda=1, halt. So does a single type mean no types or literally one type? What's the advantage of thinking that 1 type actually equals 0 types? I don't see any, so in my mind, all languages are unityped or have a richer type structure. Whether a richer type structure is desirable is a separate question.
bykovich2 9y ago
Type systems /don't/ underly the technology we use every day. The vicissitudes of real computer architectures do -- and those ain't type systems.
ianamartin 9y ago
One of the things that's so wonderful about writing software as a profession is that there is a ridiculously huge array of use cases for different languages and styles. There's nothing wrong with not caring about type systems if they don't make your life or your job better or worse. As long as you enjoy what you are doing, everything else is optional. I didn't start caring about type systems until I started running into cases where I really wished for a static one (when I was working on a large system in Python) and later when I was prototyping things where I had to make a lot of guesses in C#. Both situations frustrated me, and then I got to start really caring a lot about type systems. To a certain extent, I think it's human nature that we often don't really start caring about things that much until we experience real, personal frustration with them. Then we start caring a lot. The reason you see so many people weighing in on this here on HN, is that many regulars are the kind of person to start feeling pain very very soon and over small inconveniences where other people will just sort of deal with the minor inconvenience and focus on other aspects. One attitude is not better than the other, nor is one more ideologically pure or a marker of a better programmer or engineer. The only thing it implies is different pain thresholds. Depending on your area of focus as a developer a low or a high threshold could be either a benefit or a drawback. A language designer needs to have a very low threshold. A front-end developer/designer can afford to have a very high threshold and focus on things besides being provably correct. One of the things I like the most about software engineering is that there are opportunities for joy and discovery for everyone. And as careers progress, you can easily find yourself caring about different things at different times, and there's nothing wrong with that. There's nothing to be ashamed of any more than you should be ashamed of preferring strawberry to chocolate ice cream. (Although, in keeping with tradition here on HN, if you say that you prefer strawberry ice cream, you are dead to me and practically Hitler. :).
dannyobrien 9y ago
I feel your pain: after bouncing off Haskell many times, I found that Elm was a great entry into a more practical and narrow way of experimenting with the benefits. Now I'm reading through the new Idris book, which has the same practical approach to more complex (to me) concepts.
coldtea 9y ago
>I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. Not even 1/10th of HN has that. Tons of business types, lowly JS programmers, designers, sys-admin types, old-school programmers in C/C++, etc around.
leshow 9y ago
What languages have you tried? I think once you experience a language with types outside of the run of the mill Java/C#, you will get more excited about it. Ocaml, Rust, Haskell, Purescript, etc. Haskell for me was the one that got me excited about types.
- z3t4 9y ago
  ive only used vbscript and javascript extensibly. when ive tried java and #C ive been annoyed by the verbosity of types. and when looking at haskel or ocaml im just confused. for me types are an optimization or extra documentation for undescriptive naming, like str x, int y, list z. vs. name,age,friends. so i want to know what im missing, will there be less bugs and regressions? will i be more productive ?
  - leshow 9y ago
    > for me types are an optimization or extra documentation for undescriptive naming, This is one of those things where you should try to reserve judgement about it because your experience is so limited. Modern typed languages often don't even require you to write the type, because of type inference. > will there be less bugs and regressions? will i be more productive ? The idea with static analysis is that you're pushing more errors into the type system so it's caught at compile time rather than runtime. Everyone will answer this differently. IMO a dynamic type system doesn't make you more productive because the same invariants you have from not having an explicit type still exist in the code, they just go unchecked. For example, if I write a function to add 1 to a number, in a dynamic language if I pass a string I'll get some output that is invalid if I'm expecting the result to be a number elsewhere. Types let you encode those invariants. But encoding simple types and primitives is really just scratching the surface, I could ramble on for ages here but you should just dive into a language with a good type system (like Haskell or Ocaml like you mentioned) and stick with it long enough to give it a chance. It's so much more than just being and to say 'int' or 'string'.
    - kazinator 9y ago
      Speaking of adding to a number, in some dynamic languages, you can add 3/5 to 7/5 and the result will be 2, of type integer, indistinguishable from the object produced by a literal 2. That 3/5 and 7/5 come from some run-time source, so the result type can't be statically hard-coded to integer or rational or whatever. And so now on the static side you're into variant types and "maybes" and other junk creating an incomprehensible soup which basically Greenspuns dynamic typing in a way that will get your name cursed by subsequent maintainers.

pier25 9y ago

Reminded me of Gödel's incompleteness theorems. First incompleteness theorem Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F. Second incompleteness theorem For any consistent system F within which a certain amount of elementary arithmetic can be carried out, the consistency of F cannot be proved in F itself.

igravious 9y ago
Honest question. What in the article prompted you to think about Gödel and his theorems? Why were you reminded?
- deleted 9y ago
  [deleted]
- Jtsummers 9y ago
  Probably this part from the article: > Similarly, type theory wasn’t enough to describe new foundations for mathematics from which all mathematical truths could in principle be proven using symbolic logic. It wasn’t enough because this goal in its full extent is unattainable.
- munificent 9y ago
  I'm not sure why pier25 was reminded, but Russell's type theory and Gödel's incompleteness theorem are closely related. They both arose in response to the foundational crisis in mathematics [1]. Russell stumbled onto Russell's paradox (among others) and it shook mathematicians' confidence that everything in math was built on top of a perfectly consistent and stable foundation. If you can define a set that it "the set of sets that don't contain themself" then what other kind of crazy talk can you say in math? How do you know proven things are true and false things can't be proven in the face of weirdness like that? Russell tried to solve the problem by inventing type theory. Types stratify the universe of values such that "the set of sets that don't contain themself" is no longer a valid statement to make. Meanwhile, Gödel went and proved that, sorry, no, math is not consistent and complete. There are statements that are true but which cannot be proven. [1]: https://en.wikipedia.org/wiki/Foundations_of_mathematics#Foundational_crisis https://en.wikipedia.org/wiki/Foundations_of_mathematics#Fou...

agumonkey 9y ago

Types are close to adjoint functors / adjunctions and partial evaluation. Assigning restricted information to part of a structure to gain knowledge through limitation (math).

igravious 9y ago
The category-theory window onto the world of types only appeals to a small subset of human minds. For the average programmer you may as well be spouting gibberish because the average programmer will have no way to evaluate the claims (if any) you are making. Note, I am saying that you may as well be and not that you are. Please do not misunderstand me. Types systems certainly are formal theoretical systems but I personally have come to believe that the majority of coders are ill-served by the mathematical leanings of type theorists. I'm not sure I can explain myself better than that at the moment.
- kazinator 9y ago
  Type theorists are people who understand arrows very well -- as long as those arrows aren't pointers. :)
  - igravious 9y ago
    ba-dum tss! are you here all week?
    - kazinator 9y ago
      Sure---if catering keeps that sirloin roast coming for another seven days. Have you tried it?
- agumonkey 9y ago
  Do not worry I understand 99% of your message. It's indeed a land far far away from the everyday coding of the majority of programmers. Unless they start digging, which I did. If you take code as data (lisp roots showing) you start to want to reason about it and quickly you end up reading about FP, denotations, different forms of evaluations, the value of metadata (type or else). Now I believe there's an artificial split between math leaning people and pragmatics, the former end up as PhD, the latter in IT or close. But in reality the average coder could understand and even enjoy the land of abstractions, it's just that the river he swims in isn't flowing there so one has to run against the flow. Not to say that ideals are the only-tru-way.

simplify 9y ago

If you haven't thought much about type systems but want to understand what the big deal is, I wrote a post specifically for you [1]. It draws motivation for wanting a good static type system from first principles. [1] https://gilbert.ghost.io/type-systems-for-beginners-an-introduction/ https://gilbert.ghost.io/type-systems-for-beginners-an-intro...

threepipeproblm 9y ago

I loved this because I have read most of the source material in the context of logic, but never made the lead to type theory in computer science.

zzzcpan 9y ago

"Even though theoretically, type theories and type systems are not enough to prevent all the problems in logic and programming, they can be improved and refined to prevent an increasingly number of problems in the practice of logic and programming." It's actually just a belief. Nothing suggests that type systems and type theories can be improved to be practical at preventing bugs. I'd say it's the opposite, even with as much understanding about the nature of bugs as we have today, they don't look very promising, unlikely to make it even into the top ten of other different approaches.

dungle6 9y ago
Lolwut?
- chroem- 9y ago
  He's right. The current type theory crazy is just another in a long line cargo cult programming fads. First it was pure OOP for everything, then it was pure FP for everything, and now it's types for everything. Yes they can be useful, but it's disingenuous to act like they're a cure-all. Most bugs aren't type related, and you're adding additional mental overhead with these extremely elaborate type systems.
  - dpratt71 9y ago
    What is "he" right about, exactly? You say "yes they can be useful", but that's not the impression I get from OP. I am also confused because the very quote OP is responding to states that "...type systems are not enough to prevent all the problems in logic and programming...". Do you consider that acting like type systems are a cure-all?
  - Jtsummers 9y ago
    Types aren't new. As the article discusses they date back over a century at least in math and logic. Within programming, we've had them in every major language for decades. The first big push for strong and expressive type systems is from the functional programming work which led to the ML family and the work that made Pascal and Ada on the imperative (and later OO variants) side, which dates back some 40-50 years now.

miguelrochefort 9y ago

Don't they teach this stuff in school?

igravious 9y ago
No they don't. Only in some. Only if you're lucky.
0xCMP 9y ago
The school I went to barely taught C/C++ and the absolute minimum of PHP, CSS, Linked Lists, and Hash Maps. Very sad that so many actually smart people can't graduate knowing much just doing their course work. Let alone imagine those who lack off a bit and still pass. Unless you're programming on your own, like I was along with a few others, you graduate possibly in debt and completely unprepared. So no, they never get in to this stuff.
lgas 9y ago
Not everybody goes to school, and not everybody that does takes computer science.
empath75 9y ago
I've never taken a CS class.
khedoros1 9y ago
We danced around the edges of set theory. Symbolic logic. Combinatorial and sequential logic (especially as applies to logic circuit design). Examples of a few families of type systems, how to use them, and the practical differences between them. We didn't tend to dive deeply into the mathematical underpinnings.

deleted 9y ago

[deleted]

a-nikolaev 9y ago

Watch Oregon Programming Language School lectures "Basic Proof Theory" by Frank Pfenning. https://www.cs.uoregon.edu/research/summerschool/summer15/curriculum.html https://www.cs.uoregon.edu/research/summerschool/summer15/cu... Very clean and easy to follow video lectures on the relation between, types, programs, and logical proofs. One does not need functors and monoids to appreciate the beauty of functional type systems. (And to see why such type systems are indeed discovered rather than invented.)

z1mm32m4n 9y ago
I second this. Frank's material is always thorough and approachable. He's designed and taught many courses at CMU, and his lecture notes for them are never less than impeccable.

incan1275 9y ago

I share the author's frustration with wikipedia sometimes - people usually go to wikipedia for a distilled, comprehensible description of the subject matter. What he quoted was certainly not comprehensible, even to someone well-educated in CS foundations.

owebmaster 9y ago
I like it because of it. If what I found in wikipedia was the "easiest" description, I'd find it lacking. It is better to not understand everything on the first read than understanding almost nothing because of lack of profoundity.

georgewsinger 9y ago

Nice article. I especially liked: > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter. Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool. Also, I never thought of "higher-order functions" as breaking into a countable hierarchy of nth-order functions, which is an interesting thought. In Haskell the hierarchy would start off as zerothOrderFunction :: a firstOrderFunction :: a -> b SecondOrderFunction :: a -> (b -> c) SecondOrderFunction' :: (a -> b) -> c In general, an nth-order function is a function which either 1. Takes an (n-1)th order function as an input and returns a simple type. 2. Takes a simple type as an input and returns an (n-1)th order function as an output. The upshot is that typed programming languages not only catch bugs, but prevent you from legally expressing many non-sensical expressions (analogous to the set theory paradoxes). For example, consider the expression (\x -> x x) (\x -> x x) If you expand this expression, it reduces to itself: (\x -> x x) (\x -> x x) == (\x -> x x) (\x -> x x) In a purely untyped language, this expression would be legal. But what would be its meaning? Arguably, it is non-sense, and should be excluded from the set of legally expressible expressions. The way to do this is through a type system. And indeed, if you typed this statement into a Haskell REPL you would get a type error; this statement can actually be proven to be untypable (IIRC). On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. It would therefore be interesting if somebody found an expression which was both (i) meaningful and (ii) only expressible in an untyped language. You would then have an argument for untyped languages :-)

kmill 9y ago
> > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter. > Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool. In case it's not clear, it's just that it eventually ends up with a run time error (the talk about runFunction being a second-order function is just an explanation for why you should expect it to end up with a run time error). The evaluation is program3() == runFunction(runFunction) == runFunction(1) == 1(1) == Error: func (with value 1) is not a function

Ar-Curunir 9y ago

This article was very well written. It finally clicked for me why "hugher-order functions" are named the way they are. Any more articles in this vein?

OJFord 9y ago

Distinctly unimpressed by this post. The author seems to have an axe to grind with mathematicians as a class, which, as we would have been told in school, isn't 'big or clever'. The whole of programming, nevermind types, perhaps the most mathematical part of modern programming, arises from mathematics. There's some good history here, but the early paragraphs in particular are a display of ignorance if not arrogance. The author quotes Newton, the very chap who's said to have said he merely stood on the shoulders of giants (to 'see' such insight). Any programmer in the 21st century stands on the shoulders of mathematicians and computer scientists of the 20th,; who were in turn standing on the shoulders of the mathematicians of the 19th centuries.

pertymcpert 9y ago
I really don't think they have an axe to grind. What do they say that's incorrect? Their point is that much of what we see as type theory is inaccessible to the average programmer. When we say that some field is inaccessible, we don't blame the reader trying to understand. At the same time we're not saying that the field is wrong either, but that communication could be improved.
bogomipz 9y ago
>"Distinctly unimpressed by this post. The author seems to have an axe to grind with mathematicians as a class, which, as we would have been told in school, isn't 'big or clever'." I thought it was intended to speak to people who might be intimidated or feel obtuse when they encounter really dense academic texts when trying to learn more about type systems as it relates to programming. As such I really appreciated it. I didn't think the author was grinding any axes at all, quite the contrary.
- OJFord 9y ago
  I've no problem with that, it was the opening quotation, accompanying graphic, and following paragraph which read - to me, though I appreciate I may not have read it as it was intended - quite disrespectfully toward mathematicians. Among whom I cannot count myself, for whatever it's worth.

bogomipz 9y ago

What a great piece! I wish the author would expand on this piece with either more installments or a even short book. I find myself interested in type systems as it relates to programming language design but I haven't found much middle ground between the basic types described in introductory texts about a language and the opposite extreme heavy academic texts such as the ones the author is breaking down in this article. Can anyone recommend any other such middle ground resources on type systems and type system theory?

naasking 9y ago
What do you consider basic? Algorithm W for ML type inference is pretty basic, but powerful too. Or are you looking for something even more expressive?
- bogomipz 9y ago
  What I meant by basic was the description of types provided by a language - usually in an introductory text you might read when learning a new language. I probably didn't articulate that correctly. But I guess what I was referring to as a "middle ground"qa any resources for learning about types systems written in a similar approachable tone like this article. This was another article I read recently that I thought was similarly accessible on the subject of types systems: https://medium.com/@thejameskyle/type-systems-structural-vs-nominal-typing-explained-56511dd969f4 https://medium.com/@thejameskyle/type-systems-structural-vs-... So I guess I'm wondering if there exists such a book or series that might allow one to further their knowledge of type systems without requiring university study.
  - naasking 9y ago
    Types and Programming Languages is the go to book, and it's very accessible despite being a textbook: https://mitpress.mit.edu/books/types-and-programming-languages https://mitpress.mit.edu/books/types-and-programming-languag... You can find some earlier PDF drafts online if you Google.
    - 9y ago

dvt 9y ago

It's a common misconception that Russell/Whitehead "invented" type theory. In fact, Frege had already made the very insightful distinction between functional and non-functional types in the 1890s -- this was the key development that Russell based his hierarchy of types on. See "Function and Concept" (1891)[1]. It was a growing and communal sentiment that a (meta-)theory of types would make certain mathematical concepts more palatable. If anything, I think the conceptual father of type theory is Gottlob Frege, and Alonzo Church was the first to apply it concretely. [1] http://fitelson.org/proseminar/frege_fac.pdf http://fitelson.org/proseminar/frege_fac.pdf

rntz 9y ago
It seems to me Frege understood the need in mathematics to talk about many different kinds of thing - numbers, truth-values, functions, and so forth - and to distinguish which kind of thing you are talking about; but not the necessity to use types (or other methods) to avoid circularity. Indeed, it is precisely the mistake Frege made in his attempt to axiomatise logic and mathematics and which led to Russell's paradox, that motivated Russell (and Whitehead)'s theories of types. Frege certainly articulated a clear notion of what a function is, which is significant.

sriram_malhar 9y ago

I found Tomas Petricek's essay on "Against a universal definition of 'Type'" very informative. He argues that the word 'type' has shifted shape many times since Frege/Russel, in that the intuition behind them is different. He also argues that multiplicity of definition is a good thing. http://tomasp.net/academic/papers/against-types/ http://tomasp.net/academic/papers/against-types/

kronos29296 9y ago

Nice article about type theory. > Why there’s so much research around types if perfectly applying them to programming languages is impractical? Somehow Haskell does this perfectly. Whaddya say to that?

coldtea 9y ago
I say, citation needed. Who said "Haskell does it perfectly"? Not to mention the mental overhead of Haskell (which is also not optimal).
- aleden 9y ago
  Yeah, what the fuck? Most software engineers just want to get shit done quickly so they can go home to their wife and kids.
  - aleden 9y ago
    If you think this merits a downvote please tell why. Excuse my french.

visarga 9y ago

Types aren't just for programming and philosophy. Strongly Typed Neural Networks are also a thing. https://arxiv.org/abs/1602.02218 https://arxiv.org/abs/1602.02218

visarga 9y ago

TL;DR - Type theory == being careful about the domain a function can be applied in (adding meters to seconds or strings to sets should not be possible).

drc0 9y ago

> That’s the equivalent of writing type annotations for programming functions. And the goal is avoiding bugs instead of logical contradictions. mh, given Curry–Howard correspondence, aren't those the same? so the goal is indeed not having logical contradictions?

Sharlin 9y ago
Yes. But it's a rare programmer, or even a programming language designer, who thinks of well-typed programs in terms of proving theorems.
philix001 9y ago
They are. I avoided introducing an explanation of Curry-Howard isomorphism because I think that would not be very intuitive to many people because the most commonly used type systems have very little power to express logical properties about the program. I may write another article about this.

sgt101 9y ago

Type Systems come from Russel - yup. But the notion of Type has an interesting origin in the west as well (I would love to read/understand histories of this concept from other cultures, but I am ignorant for now). My reading is that it was invented by Scotus as Haecceity ! This was required by Catholic Christianity because of the difficulty that The Creed introduces about the identity of God - there are three entities which represent God, the Trinity - how to account for this? Well; the thisness of God is joined with the thisness of man, the thisness of the creator and the thisness of the thing which is motion (I have never understood The Holy Spirit). You can think of this as multiple inheritance! Theologians then had to account for "why three" as you can carry on making aspects of god with this mechanism infinitely, god the mother, god the lover, god the hunter and so on. But there are three - why? The answer was provided by Scotus's student Occam, entities should not multiply beyond necessity and hence there are three aspects of god because it is necessary for creation that there are. The fun bit it that this procession of thought is somewhat guessed at because writing things like this down or debating them publically was a quick route to the afterlife via a bonfire!

lists 9y ago
> The fun bit it that this procession of thought is somewhat guessed at because writing things like this down or debating them publically was a quick route to the afterlife via a bonfire! Theatre and Philosophy have always been able to have a lively chat with one another

Animats 9y ago

There's another approach, from Boyer and Moore. Boyer and Moore built up mathematics from constructs at the Peano axiom level (zero, add1, etc.) plus recursive functions that must terminate. It's constructive mathematics; there are no quantifiers, no ∀ or ∃. [1] They built an automatic theorem prover in the 1970s and 1980s that works on this theory. (I recently made it work on Gnu Common LISP and put it on Github, so people can run it again.)[2] In Boyer-Moore theory, all functions are total - you can apply any function to any object. Types are predicates. Here's a definition of ORDERED for a list of number: (DEFN ORDERED (L) (IF (LISTP L) (IF (LISTP (CDR L)) (IF (LESSP (CADR L) (CAR L)) F (ORDERED (CDR L))) T) T)) If L is not a list, it is considered to be ordered. This makes it a total function, runnable on any input, even though the result for the "wrong" type is not useful. This provides the benefits of types without requiring a theory of types. It's a very clean way to look at the foundations of mathematics. It's simpler than Russell and Whitehead. When you prove things using definitions like this, there's a lot of case analysis. This gets worse combinatorially; a theorem with four variables with type constraints will generate at least 2⁴ cases, only one of which is interesting. Most of the cases, such as when L is not a list, are trivial, but have to be analyzed. Computers are great at this, and the Boyer-Moore prover deals with those cases without any trouble. But it went against a long tradition in mathematics of avoiding case analysis. That made this approach unpopular with the generation of pre-computer mathematicians. Today, it would be more acceptable. (It's fun to run the Boyer-Moore prover today. In the 1980s, it took 45 minutes to grind through the basic theory of numbers. Now it takes a few seconds.) [1] https://www.amazon.com/Computational-Logic-Robert-S-Boyer/dp/1483236528 https://www.amazon.com/Computational-Logic-Robert-S-Boyer/dp... [2] https://github.com/John-Nagle/nqthm https://github.com/John-Nagle/nqthm

kazinator 9y ago
If every operation can have any type arguments applied to it and does something sensible with no compiler or run-time error ... good luck debugging, surely. What happens with OOP? Every class has to understand how to "bark", not only the dog class? If any class can somehow "bark" without throwing an exception, that may not be in alignment with the programmer's intent, or promote the furtherance of his or her goals in any way. For intance, the intent may be that the programmer wanted to ask the local variable dog to "bark", but misspelled it as ndog and the integer which counts the number of dogs was asked to bark instead. There is much value in identifying the problem that an integer doesn't bark.

Draco_Au 9y ago

Sexy! in today's hustle, Grothendieck Groupoids are the place to be. :toocool