If code is engineering, then types aren't science; they're electronic design rules. Coding without types is like trying to design a printed circuit board without a 'check widths and clearances' button.
That too. Usually your 'DRC' button will check for unconnected signals, shorted signals, clearances, and a bunch of other stuff that I've never used. Having the ability to enter a bit of metadata and then have the computer automatically and almost infallibly check your work is one of the best bits of CAD.
I like the way you think, but maybe it can be flipped around: types are engineering, and code is... assembly? fabrication? Putting together a product is still part of engineering, but it is not called engineering if it is done on a 'try it and see' basis.
Code is more like hot rodding- you throw stuff together, making design decisions by the seat of your pants except for a high level plan (which stays very malleable)
It's very different than the 'conventional' engineering that goes into building a competitive race car
Interesting article. Types definitely make it easier to figure how things work in new codebases. I wonder how often do experienced Haskell developers find bugs in production.
> I wonder how often do experienced Haskell developers find bugs in production
If by this you mean that you are wondering how often bugs in Haskell programs make it to production, the answer seems to be "at about the same rate as bugs in C or Java, as far as we can tell". Which, given that Haskell's (default) type system is not much more powerful at expressing constraints than C or Java's, shouldn't be a big surprise.
Haskell's type system is much more flexible, allowing you to express specific types for many cases where in Java or C you would have to resort to Object or void*; but otherwise, Haskell types can not encode much more powerful constraints than C or Java types - you can only express the available operations and the "shape". The bulk of the power comes from enforcing purity, but that is essentially a property of the standard library, not of the type system. For example, you can't express that a type is a Monad in Haskell - you can specify that it supports the Monad operations, but you have to rely on manual checking to see if it respects all of the monad laws.
Note that Idris or Coq are another matter entirely (as are dependent type systems implemented in Haskell extensions).
> If by this you mean that you are wondering how often bugs in Haskell programs make it to production, the answer seems to be "at about the same rate as bugs in C or Java, as far as we can tell".
That seems surprising. What are the bugs that Haskell has but C and Java don't that replace all the null pointer exceptions?
- perhaps Haskell programs end up being more feature-ful within a given bug budget
- perhaps Haskell induces more logic bugs, because it is more alien to the regular way of thinking
- perhaps the vast majority of NPEs are actually logic bugs, so that preventing them through the type system does not actually significantly reduce the number of bugs
- perhaps the study had some flaws in how it was counting issues
- perhaps some or all of the above are true, in various proportions
> If by this you mean that you are wondering how often bugs in Haskell programs make it to production, the answer seems to be "at about the same rate as bugs in C or Java, as far as we can tell".
I think this is worded deceptively. Bug counts are about the same when measured as bugs per line of code. A line of code in Haskell can do quite a bit more than a line of code in C or Java. I think that's a meaningful difference.
What is any of this based on? I could just as well say that the Haskell software we have in production has essentially never had a bug over 3+ years of runtime, despite being a complex, high-performance, heavily multithreaded service. But I wouldn't expect you to take that as a universal accounting of the language's relative strengths and weaknesses.
Then, fortran or numpy programmers who can only conceive a single type of data (the multi-dimensional array of floats), are not doing science? I disagree.
It is by will alone I set my mind in motion. It is by the brew of arabica that thoughts acquire speed, the teeth acquire stains, stains become a warning. It is by will alone I set my mind in motion.
This isn't a reply to your substantive point (of course I agree that fortran/numpy programmers do science), but certainly when I'm coding with numpy I have a mental model of the shapes of the arrays, very akin to the mental model I have of the types of objects in e.g. Haskell or Python. Sure, the shapes are runtime properties and they're not enforced anywhere, but that doesn't matter to my mental model of what's going on.
Whether or not you're doing science doesn't depend on which software tools you use, it depends on whether you're advancing the frontier of human knowledge. If you're producing publishable scientific research, you're doing science. If you aren't, you're probably not doing science.
I don't think the article is saying otherwise, it's just highlighting a similarity between what type systems do, and the sort of reasoning we associate with science.
The study of types is generally done as part of mathematics, not sciences. There are some attempts to study type system impact in real world programs, and ergonomics, which would fall under science, but these are a very small part of PLT.
However, the point of the article was different - the article was claiming that when you are writing the actual code for your program, you are normally using engineering-style reasoning (abduction), whereas when you are defining the hierarchy of types for your system, you are mainly applying scientific-style reasoning (induction).
Personally, I think that the article is a gross over-simplification of every single term - of deduction, abduction, and induction; of maths, science, and engineering; and of what programmers actually do. It is in fact so over-simplified that I don't see any valuable insight into the article at all. It almlst reads like a description of programming from a TV show that is trying to sound brainy.
I can write types = I'm doing science. I can write code = I'm doing engineering. I'm sure that feels good for lots of people.
"trying to sound brainy" - totally agree. this is ultimately the aim of so many attempts to show insight by defining or redefining terms - even if the the people involved don't know it.
It's because acidemics and intellectuals have to have ways to evelate themselves above ordinary folk, and usually they do this with language. We can see how important this has become in computing when you look at how important the words you use are. God forbid you use the wrong term, say container when you should be saying entity and oooo, bad programmer - why? Because we don't actually know what makes a good programmer so we have to rely on these cultural language indicators.
What was a nontrival programming problem that was solved by applying these ideas? I'd be interested in that. Somehow I suspect this doesn't exist.
1. systematic application of scientific and technological knowledge, methods, and experience to the design,
implementation, testing, and documentation of software ...
It's all there just waiting for someone to read it.
At CHF 198.00, IEEE is "just" waiting to collect fees before permitting unwashed practitioners from reading it.
But we do get a preview and there is a link to www.computer.org/sevocab so we can get a sense of their taxonomical approach. (Try searching for "Data type").
But what use is that document to the current discussion? You're not one of those people who thinks that pointing to an entry in a dictionary settles an argument?
It shows the acknowledged state of the art and thus offers an alternative for people who do not always want to start from scratch. I am well aware that there is a generation that questions everything (because they like to do so or because they simply do not know the state of the art, e.g. because it was not covered in their bachelor studies).
It's not so clear cut. Types are compositional, by definition.
Static analysis needn't be compositional, and so a small change could cause dramatic and unpredictable long-range effects elsewhere in your code. Figuring out what changed or what went wrong can be a nightmare.
I had the chance to experiment this idea a few years ago. I had a text editor which could only lint Javascript. My project was a haskell+js hybrid. There was no analysis for hs aside from running the compiler and seeing the output.
Writing the hs part was a nightmare at first. Once the project grew and I needed refactoring, js became the main nightmare. Hs simply did its thing which at that point, I already had got used to it. Js couldn't tell me if anything wrong outside of function boundaries.
A smarter js linter may prove me wrong but I believe types serve a long term goal by sacrificing productivity in the beginning.
I don't understand this dichotomy - type checking vs. all other static analysis? Or unchecked types vs. static analysis without types? Or something else?
> Starting with the slogan "proofs-as-programs," we now talk about "theories-as-systems."
But if you rewind history, you could also see the parallels to Peter Naur's "Programming as Theory building"
Or more recently: Luciano Floridi's "The Logic of Information: A Theory of Philosophy as Conceptual Design"
Different descriptions of the same thing. You could probably relate most of these ideas all the way back to the Greek classics. Democritus. Aristotle. Socrates. Plato.
Following Godel:- my intuition suggests to me that for a sufficiently powerful programming language (Turing complete?), any type system will preclude otherwise valid statements in the language. Such illegal but valid statements will be much more numerous than legal statements. These statements may not just be valid, they may be useful, and perhaps even elegant!
Sure, and our structural engineering tools and processes no doubt similarly rule out many highly artistic and potentially safe architectural designs. Notice how this argument only seems compelling to programmers when applied to programming.
If you want to go beyond the safe norms, you would have to pay the cost of validating the safety of your design. The analog in programming might be theorem proving that your elegant design was still safe.
Indeed, a type system is a great tool for producing correct code, and I cannot advocate doing away with type safety.
However, my counter-argument would be that important failures often occur due to unforeseen interactions in complex systems, perhaps more so than due to actual defects. If a type system precludes simple solutions ("obviously no bugs"), then that may cause problems in itself.
My feeling is that type systems should be separate from the language, and should statically validate in a progressive manner (eg Typescript on Javascript). As the type system is evolved to become more expressive, the amount of unsafe code can be reduced - but never quite eliminated (if my conjecture is correct).
> Sure, and our structural engineering tools and processes no doubt similarly rule out many highly artistic and potentially safe architectural designs.
Once in a while, civil engineering has a revolution exactly because somebody proves that a class of new designs is safe. The argument is compelling on every field.
There is already finite element analysis. It basically works on arbitrarily complex structures their internal connections, loads, etc. (It enabled the current boom in super skinny high rises and various fancy structures.)
We don't really have that for programming, but it's not like we shouldn't try. (Eg we have TLA+ for processes, we can use Coq and others for proving some parts of programs.)
> We don't really have that for programming, but it's not like we shouldn't try.
We do in the form of abstract interpretation and various other global static analyses. Unfortunately, these analyses are non-compositional, where small code changes can lead to dramatic and unpredictable long-range effects in the properties of your code. Finite-element analysis has similar non-compositional properties.
A type system is a compositional form of static analysis, and composition obviously has considerable reuse and cost reduction benefits, which is probably why most programming doesn't use static analysis tools beyond type systems.
Finite-element analysis - as far as I know - has the advantage of being able to estimate its own errors with some practically useful local upper bound. Because physics at that level is very much local. (Though it can't really help with higher level problems, like cyclic dynamical load and resonance problems, but there are other tools for that.)
> [...] most programming doesn't use static analysis tools beyond type systems.
Yes, unfortunately. :( It'd be great to have access to much better/stricter tools to be able to check just some interesting/important parts of programs (eg. pure business logic modules/functions) without resorting to reimplementing them in static-analysis systems.
That is the point - perhaps you can't, in the same way there are true statements in Peano arithmetic that cannot be proved (if my understanding is correct). The concern is that these statements may still be useful and elegant, and ruling them out may weaken a language significantly.
btw, I think you're missing an important qualification, which is that a given formalism can always be enriched with new axioms to increase the scope of what it's able to prove. This is relevant for type theoretic approaches, which generally have a mechanism for adding new axioms.
iiuc, the dichotomy "programming language vs. type system" doesn't hold for type-theoretic programming. E.g., languages based on System F (like Haskell) are based on a programming language that is inherently typed.
Would I be correct to say that System F, and thus Haskell, has been effectively built on the untyped lambda calculus? If so there are many (very many!) statements in the LC that are illegal under System F. Certainly whole classes of pathological statements have been disqualified, but perhaps some baby has gone out with the bathwater?
To take a much simpler example, the Simply Typed Lambda Calculus precludes non-terminating programs, but is not generally useful.
No I don’t think it’s accurate to say they’re built on untyped lambda calculus, any more than simply typed lambda calculus is built on utyped lambda calculus. They’re very much related, and there’s a strong sense in which they are built on each other, but the kinds of programs available and what can be proved or guaranteed are different.
but (for the simply typed LC anyway) the 'mechanism of action' is just the untyped LC under beta reduction surely? I mean, the type annotations don't actually do anything when the program is run/reduced?
You are essentially identifying the semantic divergence between Church and Curry style types. Church-style or Intrinsically typed Lambda Calculus does not give any meaning to ill-typed expressions and there for beta-reduction can not proceed for these invalid expressions. Where as Curry-style or Extrinsically typed lambda calculus gives meaning to expression that do not consider the type alleged to be possessed by that expression.
The crucial difference between Church and Curry is that Curry allows each term to be ascribed a set of types - perhaps 0, 1 or many - whereas Church insists on each term having exactly one (often annotated). Both are systems for proving type correctness of terms.
I've never really bought this argument. Casting is the way a programmer can selectively bypass the type system and every typed language I've ever used includes casting.
For Church-typed languages as opposed to Curry-typed languages, it's not even apparent what it would would mean to "preclude otherwise valid statements" because types are a part of the language. It's akin to saying structured programming precludes otherwise valid statements in the language because the lack of goto precludes otherwise valid statements in the language. Sure, but the lack of goto is precisely a facet of the language! For a Church-typed language the types are just another part of syntax (this is more than just theory, Racket shows that a type system can in fact be implemented simply as macros).
Invoking Godel here I don't think makes sense. Godel's incompleteness theorems apply to what you can prove about a program with types. The majority of typed programming languages have type systems that are too weak for Godel's incompleteness theorems to apply. And there is no need for a type system to be sound (if thought of as a logical system with programs as proofs via the Curry-Howard isomorphism), again most programming languages' type systems are not sound in this manner.
Even with a Curry-style system of semantics, the presence of casting is enough to allow any type system to allow every valid statement in the language (the proof of this is to cast every term to the same type).
That being said I am sympathetic to the feeling that "I'm just doing this to satisfy the type checker," a feeling that can show up increasingly frequently for languages with increasingly sophisticated type systems. I would argue this often happens precisely when you take the power of casting away. This is the dark side of "correct by construction" techniques where if the construction technique is devilishly complex, then you're forced to deal with that complexity. But this usually only applies to languages with some amount of dependent typing, which the majority of languages do not have.
Casting is not always permitted in all contexts. In C++, many casts that would be valid on the real machine are undefined behavior in the language, for example.
That's sort of the point though. Contexts where casting is not permitted in that sense are where the types are an integral part of the semantics of the language and for which it doesn't make sense to speak of "otherwise valid statements" (as indeed is the case here with C++).
The original comment's "otherwise valid statements" are precisely UB in C++.
But is there a difference between a statement that is excluded from the language by a non-typing rule and a statement that is excluded from the language by a typing rule? In both cases, the "natural" evaluation could work as the developer intends but some language rule prevents that program from being executed.
Honestly the answer is it depends and needs to be looked at on a language-by-language basis. There's certain languages for which there is no difference between typing rules and non-typing rules. Type-checking is literally the same as syntax checking (this is what I was referring to with a types as macros approach that has an implementation in Racket).
There's others where you can try to finesse some sort of Curry-style semantics out of a language that doesn't have those semantics.
The crucial question though is to what end?
The original contention is that types represent a limitation on a language, a limitation that you might want to sometimes lift. To the extent that you can separate the types from a language itself I agree that's true in theory, but that problem is solvable with casts.
And to the extent it isn't solvable with casts, it isn't solvable precisely because the Curry-style interpretation fails and the line between being excluded by a "surface-level" typing rule vs a deeper matter of language semantics is blurred.
All that being said, there is an argument to be made that you sometimes want to preserve a Curry-style fragment of your language precisely in order to facilitate this kind of "escape hatch" with a cast
However, going back to my original point, at least for me, this isn't something I worry about with mainstream languages. It feels more like a theoretical concern than a practical one. If you have a language with a type system that cares a lot about soundness and expressivity then it's something to keep in mind. I worry in dependently-typed languages that without preserving this distinction between types that have runtime-significance and types that do not, you lack an effective cast escape hatch.
For mainstream languages my concerns are exactly the opposite. The type system often is of little use to me because so much code makes use of escape hatches.
I'll post a reply that I wrote to one of parent's comments that was deleted, but I think the parent had some reasonable points.
It's slightly tweaked to remove some of the parts that don't really make sense without the other comment's context.
You're implicitly assuming a Curry-style semantics to your language. Here's an outline of what I assume you mean. Correct me if I'm wrong.
There are effectively two separate languages. Your type-level language and your term-level language. Each of these languages have their own notions of validity. At the type-level, a series of statements is valid if the type checker accepts them. At the term-level a series of statements is valid if the program runs without crashing. There is also some way of associating the two languages together, i.e. type assignment.
Given these two languages, we would like for their two notions of validity to coincide. That is it would be great if given a type assignment, the type-level language is valid (type checker accepts it) if and only if the term-level language is valid (program does not crash).
The first thing to note is that many (most?) statically typed languages don't have Curry-style semantics. As UncleMeat points out not crashing is not sufficient to be semantically valid in C++. It might just happen not to crash on your machine with a certain set of optimizations and compiler flags. Types play an integral role in what it means for a language to be semantically valid and it doesn't really make sense to consider the language independently of types.
For Curry-style languages, there is an indirect linkage to Godel, but the more obvious link is through the halting problem. If type checking is decidable (something you probably want to be true) then your term-level language must be decidable as well if the two languages truly coincide. But then you lose Turing completeness as your first comment points out.
The thing is though that no mainstream statically typed language tries to ensure this. All of them allow assigning a type to something that might loop forever or crash.
I would argue you're effectively attacking a straw man of a type system.
However, I agree with you that "there are times when a type system is too cumbersome, and we must escape it to do useful things." However, this is not something I view as limited to type systems. I view this as true of every facet of programming (and in a greater sense true of every facet of life).
Every system must have a way of piercing its assumptions when you as its user have extra knowledge the system does not. This shows up in performance and protection against side-channel attacks (assembly intrinsics, FFI, etc.). This shows up in orchestration tools (yes yes yes it's all good and well to treat infrastructure as immutable and machines like cattle not pets but I would sometimes like to just SSH onto a machine and make some one-off changes!). This shows up in structured programming (once in a very blue moon Python, it would be great if you just gave me a goto/label). The list goes on and on.
> There are effectively two separate languages. Your type-level language and your term-level language.
Computational Type Theory (CTT) blends the distinction b/w terms and types, and in fact C-H correspondence bears no consequence on CTT research.
From a previous comment [1]:
> I worry in dependently-typed languages that without preserving this distinction between types that have runtime-significance (Church-style) and types that do not (Curry-style), you lack an effective cast escape hatch.
I think we've basically two categories of (turing-complete) programming languages:
1. Mainstream languages that use type systems for multiple purposes: operational semantics, compiler optimization, lightweight formal verification, etc, and provide casting escape hatches.
2. Languages where the type system's primary (and only?) purpose is formal verification, and there are no escape hatches.
It's just that 1 and 2 are really meant for different domains. 2 is mostly used for high-assurance domains like aerospace, automotive, healthcare, blockchain smart contracts where formal verification is high priority and escape hatches aren't sought, hence not built-in.
Thankyou for your reply (and apologies for deleting the comment).
I am not sure that the distinction between Curry and Church semantics is so critical - after all we have but a single 'engine of computation': beta reduction, applied to statements in the untyped lambda calculus. Thus a statement with Church annotations will reduce exactly as one without?
I think I'm taking the view that statements in the untyped lambda calculus, with beta reduction, are our objects of study, and a type system (Church or Curry derived) is a set of theorems (or indeed a mechanism for generating theorems) that we use to prove certain facts about such objects, again much like the Peano axiomatization of natural numbers. Thus I profess my heresy!
This is not heresy; it's just Curry. The assertion that beta reduction (i.e. evaluation) does not rely on type information and types are overlaid on top is precisely the heart of Curry semantics.
The distinction between Curry and Church semantics does not seem particularly relevant for something like the simply typed lambda calculus.
After all
f : Int -> Int
f(x) = x + 1
f(5) : Int // 6
can simply have its types removed after type checking and everything will still run right?
f(x) = x + 1
f(5) // 6
However this distinction becomes more important for type systems with polymorphism, particularly ad-hoc polymorphism.
f : a -> b where b is Zeroable
f(x) = zero
// E.g. List[a] is Zeroable where zero: List[a] = emptyList
// Int is Zeroable where zero: Int = 0
// String is Zeroable where zero: String = ""
Now an expression such as f(5) is impossible to evaluate without type information.
f(5): List[Boolean] // This is emptyList
f(5): Int // This is 0
f(5): String // This is ""
Types become an essential part of what it means to evaluate a term and hence we are led to Church semantics.
Now there are ways of trying to recover Curry-style semantics. One way is to replicate the type system at runtime. Then of course you're free to "erase" the types since you still have them at runtime anyways!
This is essentially what statically typed object-oriented languages do with late binding. Note that in the extreme though, the type system cannot limit the scope of valid programs because valid programs at runtime are precisely those valid at type-checking time because the types are replicated! Often though only fragments of the type system will be preserved at runtime so that there is still a discrepancy. For example, usually return type polymorphism (the previous example of f) is disallowed in these systems (see e.g. Java) to avoid having to embed even more of the type system than just the types of individual objects.
Another option is to compile the program down into a language with a simpler type system (or no type system at all!) and then use Curry-style semantics with the simpler type system. However, that feels more like an implementation detail than anything else. Just because I can compile Java to C does not mean that they have the same semantics. Indeed the point of compilation is precisely to translate between two systems with incompatible semantics, otherwise the compilation is trivial.
Stepping back from all this, Curry-style vs Church-style semantics have implications for type checking and type inference. In general things are harder in a Curry-style regimen. Type-checking which is decidable in a Church system often becomes undecidable in an equivalent Curry system. This makes Curry-style semantics burdensome to work with in rich type systems.
Curry-style semantics are of course an ideal fit for gradual typing systems that aim to go from an untyped system and gradually add typing on top of that untyped system.
I'm sorry but this is wrong: "The assertion that beta reduction (i.e. evaluation) does not rely on type information and types are overlaid on top is precisely the heart of Curry semantics."
Beta reduction is not affected by types ascribed to terms. The crucial difference between Church and Curry is that Curry allows each term to be ascribed a set of types - perhaps 0, 1 or many - whereas Church insists on each term having exactly one (often annotated). That is all. Both are systems for proving type correctness of terms, and are no more than that.
(cont'd) ... and I see it now, the damage that has been wrought.
I imagine Church never dreamed that his approach of unitary type assignment would lead people to believe that types actually exist, and that programs should do different things when meeting such 'types'.
Yes let's get back to Curry, and build a better world.
Ah indeed you're right about beta-reduction; jumping to equating it with general evaluation is a bridge too far.
Eh... I dunno. Church was around for a long time. He saw a lot of the languages we use now.
That ship for ad hoc polymorphism sailed a long time ago. Almost every widely used language I can think of has ad hoc polymorphism, whether that be through runtime types (late binding a la Python, PHP, Ruby, Common Lisp, Javascript, Java, Clojure, Scala, C#, C++, Smalltalk) or through compile time translation (early binding a la Rust, Haskell, also Scala, ML, also Java, also C++, Idris, Agda, Coq). The only languages I can think of at the moment that doesn't have ad hoc polymorphism are C and Elm.
To put it another way every language that supports some notion of overloading has to do a different thing when meeting a type. And I think you'd have a hard time taking overloading away from programmers.
That is more than just your intuition--with minor tweaking, it is a theorem that was taught in my Programming Language Theory course when I was in college!
The tweak is that any safe type system will preclude programs that are otherwise semantically valid. You can have a type system that catches some errors and lets others through, or you can have a type system that catches all errors but also excludes some valid formulas (or even, and most commonly, a type system that catches most errors, also prohibits some valid formulas, but nevertheless still lets other errors through), but you can't have a decidable type system that permits all semantically valid programs and excludes all erroneous programs.
It’s also a multidimensional problem, so sometimes people improve the state of the art in one dimension, but either at the expense or the neglect of another.
I think it’s a bit like any applied science. There’s a theoretical limit to the efficiency of an internal combustion engine. We grow closer to it, often with more complicated machinery, occasionally with better construction (ie, the manufacturing becomes more complex so the product is less complex). And we balance the consequences (pollution, reliability, cost) against the benefits.
Once in a while we substitute a different model (E.g., Atkinson) with small but important differences in the theoretical limits, by looking at the problem differently.
This seems somewhat of a silly critique. By the same logic, we know that the vast majority of problems can not be solved by any program, yet we write programs to solve problems everyday. Or we know that the vast majority of mathematical statements cannot be proven or disproven, yet we can do math proofs just fine.
I think we don't suffer from this because we end up asking questions that are relatively simple. Technically, there are many more uncomputable numbers than computable ones, but we are much more interested in the infinitely smaller set of the computable numbers than the uncomputables. (Furthermore, we are much more interested in rationals than we have any right to be, considering that there are many more real numbers than rationals).
There should be a similar premise for type systems. Perhaps any type system will disallow valid statements, but we can try to make it so that those valid statements are above a certain length, say 100,000. Then, there are still infinitely many valid statements that are illegal, and they may be much more elegant than their counterparts, but they're so long that it is irrelevant for practical purposes.
Now, actually building a type system like that is a whole 'nother beast. I imagine you would give up some notion of completeness for a level of "predisposition", that is, the type system predisposes programmers to making legal statements in the same way that normal number systems(reals, rationals) predisposes mathematicians to making provable statements. A slight nudge towards writing programs in a certain style can go a long way in terms of avoiding "illegal but valid" statements.
I put a related question on Computer Science Stack Exchange a week ago. Linking it here in the hopes that HN users roll-calling here will shed some light.
An elephant's toenail is part of the elephant, but is not "the elephant." Types are implementation details to a computer scientist, just as unit conversions are implementation details to a chemist. Likewise, code is an artifact of engineering, not the engineering itself.
That doesn't seem quite right to me. Maybe code is sermons, types are scripture? Or even code is a religious person's lived-out life, and types are scripture?
The point of the article, for those who read it, is to characterize different activities of development in a static language as deductive, abductive, or inductive and to discuss examples and relationships between these activities.
it's not to contrast static languages with dynamic languages.
He conflates science and logic. Science and logic are two very different things.
for example, given:
f(x) = x*0;
verify the hypothesis that:
for all n in Real Numbers, f(n) = 0
To verify the above using science you would take a statistical sample of x and verify that it equals zero for that sample.
1*0 == 0
2*0 == 0
3*0 == 0
4*0 == 0
That's four test samples out of an infinite domain. To fully verify the function f via science you technically need infinite test cases to verify the fact. Usually you can never achieve this in reality so science usually takes what you call a "sample" and you say that if the sample is true very likely the hypothesis is true. The only assumption science makes is that probability theory applies to events in reality.
Note the isomorphism between science and unit testing; Same bs with none of the statistical rigor.
To do the same in logic you have to make assumptions from axioms and logically derive a proof from axioms.
The previous thing which was called a hypothesis is now called a theorem:
That being said how does Type theory and code apply to science and logic and engineering?
Type theory is part of logic it is not part of science. Don't conflate the two.
What is engineering? Engineering is creating solutions for problems using either or both Science/Logic. In the realm of software engineering there is very little of both, It's all an art. Logic is rarely employed for verification and when it's done it's usually just type checking; and testing isn't done to a rigorous level that other scientific and engineering disciplines require.
For say the creation of the 787 airliner. The entire plane is built theoretically in software to such a degree that when they actually materialize the theoretical model as a physical prototype it can actually fly. Then after it is built they test it rigorously to a very high degree.
For most of software, none of the above is is ever done. We mostly work like artists, just making shit up (design patterns) and adhoc automated testing.
So in all practicality your coding job has no relation to either science, engineering or logic. You are an artist.
I know technically you apply bits an pieces of science and logic in your programming job but ultimately you use adhoc logic and science for even crossing the street, I'm not going to count programming as a "science" due to this.
>That's four samples out of an infinite domain. To fully verify the function f via science you technically need infinite test cases to verify the fact. Usually you can never achieve this in reality so science usually takes what you call a "sample" and you say that if the sample is true very likely the hypothesis is true. The only assumption science makes is that probability theory applies to events in reality.
Usually equating null-hypothesis significance testing with the scientific method is a sign of cargo cult.
87 comments
[ 3.0 ms ] story [ 131 ms ] threadIt's very different than the 'conventional' engineering that goes into building a competitive race car
If by this you mean that you are wondering how often bugs in Haskell programs make it to production, the answer seems to be "at about the same rate as bugs in C or Java, as far as we can tell". Which, given that Haskell's (default) type system is not much more powerful at expressing constraints than C or Java's, shouldn't be a big surprise.
Haskell's type system is much more flexible, allowing you to express specific types for many cases where in Java or C you would have to resort to Object or void*; but otherwise, Haskell types can not encode much more powerful constraints than C or Java types - you can only express the available operations and the "shape". The bulk of the power comes from enforcing purity, but that is essentially a property of the standard library, not of the type system. For example, you can't express that a type is a Monad in Haskell - you can specify that it supports the Monad operations, but you have to rely on manual checking to see if it respects all of the monad laws.
Note that Idris or Coq are another matter entirely (as are dependent type systems implemented in Haskell extensions).
That seems surprising. What are the bugs that Haskell has but C and Java don't that replace all the null pointer exceptions?
Here are some more info http://blog.ezyang.com/2011/05/space-leak-zoo/
It's been almost a decade since though. Maybe the compiler catches more nowadays.
- perhaps Haskell programs end up being more feature-ful within a given bug budget
- perhaps Haskell induces more logic bugs, because it is more alien to the regular way of thinking
- perhaps the vast majority of NPEs are actually logic bugs, so that preventing them through the type system does not actually significantly reduce the number of bugs
- perhaps the study had some flaws in how it was counting issues
- perhaps some or all of the above are true, in various proportions
I think this is worded deceptively. Bug counts are about the same when measured as bugs per line of code. A line of code in Haskell can do quite a bit more than a line of code in C or Java. I think that's a meaningful difference.
https://m-cacm.acm.org/magazines/2017/10/221326-a-large-scal...
They find some effect of language on defects, but it is small, and there are other factors with much larger impact.
It is by will alone I set my mind in motion. It is by the brew of arabica that thoughts acquire speed, the teeth acquire stains, stains become a warning. It is by will alone I set my mind in motion.
I don't think the article is saying otherwise, it's just highlighting a similarity between what type systems do, and the sort of reasoning we associate with science.
Technology is applied engineering, and engineering is applied science.
The study of types may fall into some field of science. Applying it is engineering.
However, the point of the article was different - the article was claiming that when you are writing the actual code for your program, you are normally using engineering-style reasoning (abduction), whereas when you are defining the hierarchy of types for your system, you are mainly applying scientific-style reasoning (induction).
Personally, I think that the article is a gross over-simplification of every single term - of deduction, abduction, and induction; of maths, science, and engineering; and of what programmers actually do. It is in fact so over-simplified that I don't see any valuable insight into the article at all. It almlst reads like a description of programming from a TV show that is trying to sound brainy.
"trying to sound brainy" - totally agree. this is ultimately the aim of so many attempts to show insight by defining or redefining terms - even if the the people involved don't know it.
It's because acidemics and intellectuals have to have ways to evelate themselves above ordinary folk, and usually they do this with language. We can see how important this has become in computing when you look at how important the words you use are. God forbid you use the wrong term, say container when you should be saying entity and oooo, bad programmer - why? Because we don't actually know what makes a good programmer so we have to rely on these cultural language indicators.
What was a nontrival programming problem that was solved by applying these ideas? I'd be interested in that. Somehow I suspect this doesn't exist.
Typescript specifically. But web pages are a different mindset than most domains.
Why not the other way around ?
3.3810 software engineering
1. systematic application of scientific and technological knowledge, methods, and experience to the design, implementation, testing, and documentation of software ...
It's all there just waiting for someone to read it.
But we do get a preview and there is a link to www.computer.org/sevocab so we can get a sense of their taxonomical approach. (Try searching for "Data type").
Static analysis needn't be compositional, and so a small change could cause dramatic and unpredictable long-range effects elsewhere in your code. Figuring out what changed or what went wrong can be a nightmare.
Writing the hs part was a nightmare at first. Once the project grew and I needed refactoring, js became the main nightmare. Hs simply did its thing which at that point, I already had got used to it. Js couldn't tell me if anything wrong outside of function boundaries.
A smarter js linter may prove me wrong but I believe types serve a long term goal by sacrificing productivity in the beginning.
> Starting with the slogan "proofs-as-programs," we now talk about "theories-as-systems."
But if you rewind history, you could also see the parallels to Peter Naur's "Programming as Theory building"
Or more recently: Luciano Floridi's "The Logic of Information: A Theory of Philosophy as Conceptual Design"
Different descriptions of the same thing. You could probably relate most of these ideas all the way back to the Greek classics. Democritus. Aristotle. Socrates. Plato.
Our tools are finally catching up...
If you want to go beyond the safe norms, you would have to pay the cost of validating the safety of your design. The analog in programming might be theorem proving that your elegant design was still safe.
Once in a while, civil engineering has a revolution exactly because somebody proves that a class of new designs is safe. The argument is compelling on every field.
We don't really have that for programming, but it's not like we shouldn't try. (Eg we have TLA+ for processes, we can use Coq and others for proving some parts of programs.)
We do in the form of abstract interpretation and various other global static analyses. Unfortunately, these analyses are non-compositional, where small code changes can lead to dramatic and unpredictable long-range effects in the properties of your code. Finite-element analysis has similar non-compositional properties.
A type system is a compositional form of static analysis, and composition obviously has considerable reuse and cost reduction benefits, which is probably why most programming doesn't use static analysis tools beyond type systems.
> [...] most programming doesn't use static analysis tools beyond type systems.
Yes, unfortunately. :( It'd be great to have access to much better/stricter tools to be able to check just some interesting/important parts of programs (eg. pure business logic modules/functions) without resorting to reimplementing them in static-analysis systems.
btw, I think you're missing an important qualification, which is that a given formalism can always be enriched with new axioms to increase the scope of what it's able to prove. This is relevant for type theoretic approaches, which generally have a mechanism for adding new axioms.
Types are not just an engineering technology, they are a QA tool.
(also, at no stage have you provided an example for such "more elegant" statements)
To take a much simpler example, the Simply Typed Lambda Calculus precludes non-terminating programs, but is not generally useful.
For Church-typed languages as opposed to Curry-typed languages, it's not even apparent what it would would mean to "preclude otherwise valid statements" because types are a part of the language. It's akin to saying structured programming precludes otherwise valid statements in the language because the lack of goto precludes otherwise valid statements in the language. Sure, but the lack of goto is precisely a facet of the language! For a Church-typed language the types are just another part of syntax (this is more than just theory, Racket shows that a type system can in fact be implemented simply as macros).
Invoking Godel here I don't think makes sense. Godel's incompleteness theorems apply to what you can prove about a program with types. The majority of typed programming languages have type systems that are too weak for Godel's incompleteness theorems to apply. And there is no need for a type system to be sound (if thought of as a logical system with programs as proofs via the Curry-Howard isomorphism), again most programming languages' type systems are not sound in this manner.
Even with a Curry-style system of semantics, the presence of casting is enough to allow any type system to allow every valid statement in the language (the proof of this is to cast every term to the same type).
That being said I am sympathetic to the feeling that "I'm just doing this to satisfy the type checker," a feeling that can show up increasingly frequently for languages with increasingly sophisticated type systems. I would argue this often happens precisely when you take the power of casting away. This is the dark side of "correct by construction" techniques where if the construction technique is devilishly complex, then you're forced to deal with that complexity. But this usually only applies to languages with some amount of dependent typing, which the majority of languages do not have.
The original comment's "otherwise valid statements" are precisely UB in C++.
There's others where you can try to finesse some sort of Curry-style semantics out of a language that doesn't have those semantics.
The crucial question though is to what end?
The original contention is that types represent a limitation on a language, a limitation that you might want to sometimes lift. To the extent that you can separate the types from a language itself I agree that's true in theory, but that problem is solvable with casts.
And to the extent it isn't solvable with casts, it isn't solvable precisely because the Curry-style interpretation fails and the line between being excluded by a "surface-level" typing rule vs a deeper matter of language semantics is blurred.
All that being said, there is an argument to be made that you sometimes want to preserve a Curry-style fragment of your language precisely in order to facilitate this kind of "escape hatch" with a cast
However, going back to my original point, at least for me, this isn't something I worry about with mainstream languages. It feels more like a theoretical concern than a practical one. If you have a language with a type system that cares a lot about soundness and expressivity then it's something to keep in mind. I worry in dependently-typed languages that without preserving this distinction between types that have runtime-significance and types that do not, you lack an effective cast escape hatch.
For mainstream languages my concerns are exactly the opposite. The type system often is of little use to me because so much code makes use of escape hatches.
It's slightly tweaked to remove some of the parts that don't really make sense without the other comment's context.
You're implicitly assuming a Curry-style semantics to your language. Here's an outline of what I assume you mean. Correct me if I'm wrong.
There are effectively two separate languages. Your type-level language and your term-level language. Each of these languages have their own notions of validity. At the type-level, a series of statements is valid if the type checker accepts them. At the term-level a series of statements is valid if the program runs without crashing. There is also some way of associating the two languages together, i.e. type assignment.
Given these two languages, we would like for their two notions of validity to coincide. That is it would be great if given a type assignment, the type-level language is valid (type checker accepts it) if and only if the term-level language is valid (program does not crash).
The first thing to note is that many (most?) statically typed languages don't have Curry-style semantics. As UncleMeat points out not crashing is not sufficient to be semantically valid in C++. It might just happen not to crash on your machine with a certain set of optimizations and compiler flags. Types play an integral role in what it means for a language to be semantically valid and it doesn't really make sense to consider the language independently of types.
For Curry-style languages, there is an indirect linkage to Godel, but the more obvious link is through the halting problem. If type checking is decidable (something you probably want to be true) then your term-level language must be decidable as well if the two languages truly coincide. But then you lose Turing completeness as your first comment points out.
The thing is though that no mainstream statically typed language tries to ensure this. All of them allow assigning a type to something that might loop forever or crash.
I would argue you're effectively attacking a straw man of a type system.
However, I agree with you that "there are times when a type system is too cumbersome, and we must escape it to do useful things." However, this is not something I view as limited to type systems. I view this as true of every facet of programming (and in a greater sense true of every facet of life).
Every system must have a way of piercing its assumptions when you as its user have extra knowledge the system does not. This shows up in performance and protection against side-channel attacks (assembly intrinsics, FFI, etc.). This shows up in orchestration tools (yes yes yes it's all good and well to treat infrastructure as immutable and machines like cattle not pets but I would sometimes like to just SSH onto a machine and make some one-off changes!). This shows up in structured programming (once in a very blue moon Python, it would be great if you just gave me a goto/label). The list goes on and on.
Computational Type Theory (CTT) blends the distinction b/w terms and types, and in fact C-H correspondence bears no consequence on CTT research.
From a previous comment [1]:
> I worry in dependently-typed languages that without preserving this distinction between types that have runtime-significance (Church-style) and types that do not (Curry-style), you lack an effective cast escape hatch.
I think we've basically two categories of (turing-complete) programming languages:
1. Mainstream languages that use type systems for multiple purposes: operational semantics, compiler optimization, lightweight formal verification, etc, and provide casting escape hatches.
2. Languages where the type system's primary (and only?) purpose is formal verification, and there are no escape hatches.
It's just that 1 and 2 are really meant for different domains. 2 is mostly used for high-assurance domains like aerospace, automotive, healthcare, blockchain smart contracts where formal verification is high priority and escape hatches aren't sought, hence not built-in.
[1] https://news.ycombinator.com/item?id=22794925
I am not sure that the distinction between Curry and Church semantics is so critical - after all we have but a single 'engine of computation': beta reduction, applied to statements in the untyped lambda calculus. Thus a statement with Church annotations will reduce exactly as one without?
I think I'm taking the view that statements in the untyped lambda calculus, with beta reduction, are our objects of study, and a type system (Church or Curry derived) is a set of theorems (or indeed a mechanism for generating theorems) that we use to prove certain facts about such objects, again much like the Peano axiomatization of natural numbers. Thus I profess my heresy!
The distinction between Curry and Church semantics does not seem particularly relevant for something like the simply typed lambda calculus.
After all
can simply have its types removed after type checking and everything will still run right? However this distinction becomes more important for type systems with polymorphism, particularly ad-hoc polymorphism. Now an expression such as f(5) is impossible to evaluate without type information. Types become an essential part of what it means to evaluate a term and hence we are led to Church semantics.Now there are ways of trying to recover Curry-style semantics. One way is to replicate the type system at runtime. Then of course you're free to "erase" the types since you still have them at runtime anyways!
This is essentially what statically typed object-oriented languages do with late binding. Note that in the extreme though, the type system cannot limit the scope of valid programs because valid programs at runtime are precisely those valid at type-checking time because the types are replicated! Often though only fragments of the type system will be preserved at runtime so that there is still a discrepancy. For example, usually return type polymorphism (the previous example of f) is disallowed in these systems (see e.g. Java) to avoid having to embed even more of the type system than just the types of individual objects.
Another option is to compile the program down into a language with a simpler type system (or no type system at all!) and then use Curry-style semantics with the simpler type system. However, that feels more like an implementation detail than anything else. Just because I can compile Java to C does not mean that they have the same semantics. Indeed the point of compilation is precisely to translate between two systems with incompatible semantics, otherwise the compilation is trivial.
Stepping back from all this, Curry-style vs Church-style semantics have implications for type checking and type inference. In general things are harder in a Curry-style regimen. Type-checking which is decidable in a Church system often becomes undecidable in an equivalent Curry system. This makes Curry-style semantics burdensome to work with in rich type systems.
Curry-style semantics are of course an ideal fit for gradual typing systems that aim to go from an untyped system and gradually add typing on top of that untyped system.
Beta reduction is not affected by types ascribed to terms. The crucial difference between Church and Curry is that Curry allows each term to be ascribed a set of types - perhaps 0, 1 or many - whereas Church insists on each term having exactly one (often annotated). That is all. Both are systems for proving type correctness of terms, and are no more than that.
I imagine Church never dreamed that his approach of unitary type assignment would lead people to believe that types actually exist, and that programs should do different things when meeting such 'types'.
Yes let's get back to Curry, and build a better world.
Eh... I dunno. Church was around for a long time. He saw a lot of the languages we use now.
That ship for ad hoc polymorphism sailed a long time ago. Almost every widely used language I can think of has ad hoc polymorphism, whether that be through runtime types (late binding a la Python, PHP, Ruby, Common Lisp, Javascript, Java, Clojure, Scala, C#, C++, Smalltalk) or through compile time translation (early binding a la Rust, Haskell, also Scala, ML, also Java, also C++, Idris, Agda, Coq). The only languages I can think of at the moment that doesn't have ad hoc polymorphism are C and Elm.
To put it another way every language that supports some notion of overloading has to do a different thing when meeting a type. And I think you'd have a hard time taking overloading away from programmers.
The tweak is that any safe type system will preclude programs that are otherwise semantically valid. You can have a type system that catches some errors and lets others through, or you can have a type system that catches all errors but also excludes some valid formulas (or even, and most commonly, a type system that catches most errors, also prohibits some valid formulas, but nevertheless still lets other errors through), but you can't have a decidable type system that permits all semantically valid programs and excludes all erroneous programs.
I think it’s a bit like any applied science. There’s a theoretical limit to the efficiency of an internal combustion engine. We grow closer to it, often with more complicated machinery, occasionally with better construction (ie, the manufacturing becomes more complex so the product is less complex). And we balance the consequences (pollution, reliability, cost) against the benefits.
Once in a while we substitute a different model (E.g., Atkinson) with small but important differences in the theoretical limits, by looking at the problem differently.
I think we don't suffer from this because we end up asking questions that are relatively simple. Technically, there are many more uncomputable numbers than computable ones, but we are much more interested in the infinitely smaller set of the computable numbers than the uncomputables. (Furthermore, we are much more interested in rationals than we have any right to be, considering that there are many more real numbers than rationals).
There should be a similar premise for type systems. Perhaps any type system will disallow valid statements, but we can try to make it so that those valid statements are above a certain length, say 100,000. Then, there are still infinitely many valid statements that are illegal, and they may be much more elegant than their counterparts, but they're so long that it is irrelevant for practical purposes.
Now, actually building a type system like that is a whole 'nother beast. I imagine you would give up some notion of completeness for a level of "predisposition", that is, the type system predisposes programmers to making legal statements in the same way that normal number systems(reals, rationals) predisposes mathematicians to making provable statements. A slight nudge towards writing programs in a certain style can go a long way in terms of avoiding "illegal but valid" statements.
Ref: https://cs.stackexchange.com/questions/122066/does-the-under...
it's not to contrast static languages with dynamic languages.
for example, given:
verify the hypothesis that: To verify the above using science you would take a statistical sample of x and verify that it equals zero for that sample. That's four test samples out of an infinite domain. To fully verify the function f via science you technically need infinite test cases to verify the fact. Usually you can never achieve this in reality so science usually takes what you call a "sample" and you say that if the sample is true very likely the hypothesis is true. The only assumption science makes is that probability theory applies to events in reality.Note the isomorphism between science and unit testing; Same bs with none of the statistical rigor.
To do the same in logic you have to make assumptions from axioms and logically derive a proof from axioms.
The previous thing which was called a hypothesis is now called a theorem:
The proof of the theorem from the axioms of arithmetic can be found here: https://math.stackexchange.com/questions/400605/a-proof-of-n...That being said how does Type theory and code apply to science and logic and engineering?
Type theory is part of logic it is not part of science. Don't conflate the two.
What is engineering? Engineering is creating solutions for problems using either or both Science/Logic. In the realm of software engineering there is very little of both, It's all an art. Logic is rarely employed for verification and when it's done it's usually just type checking; and testing isn't done to a rigorous level that other scientific and engineering disciplines require.
For say the creation of the 787 airliner. The entire plane is built theoretically in software to such a degree that when they actually materialize the theoretical model as a physical prototype it can actually fly. Then after it is built they test it rigorously to a very high degree.
For most of software, none of the above is is ever done. We mostly work like artists, just making shit up (design patterns) and adhoc automated testing.
So in all practicality your coding job has no relation to either science, engineering or logic. You are an artist.
I know technically you apply bits an pieces of science and logic in your programming job but ultimately you use adhoc logic and science for even crossing the street, I'm not going to count programming as a "science" due to this.
Usually equating null-hypothesis significance testing with the scientific method is a sign of cargo cult.
I'm not strictly equating inference or verification to science. I am simply equating this: https://www.wikiwand.com/en/Scientific_method
Testing and hypothesis are the key words. Prediction is the other keyword. Analysis I never covered, but you assumed I used null hypothesis testing.
Tell me what is your opinion of all of this since you think my opinion is a 'cargo cult.'