Seven deadly sins of talking about “types” (2014)

http://www.cl.cam.ac.uk/~srk31/blog/2014/10/07/

by _qc3o • 11 years ago

131 171 11 years ago

cl.cam.ac.uk

qznc• 11 years ago

The coda at the end is nice tool in general. Whenever you find yourself in a discussion, where it seems people talk past each other because some words have a fuzzy meaning, try to avoid the word completely. Works good for discussions about "free will", "love", "intelligence", "luck", "conciousness", and apparently "types".

pseudonom-• 11 years ago

http://lesswrong.com/lw/nu/taboo_your_words/

pekk2• 11 years ago

I found this wonderfully clear and refreshing and I felt hopeful for the future of programming. In the meantime, it's just nice to see that not everyone is a shambling cultist, repeating canned talking points they read on a wiki which affirm to them that their own choice is the very best choice possible.

davidgrenier• 11 years ago

It's fair to say that but it isn't the case that someone can have an worthwhile opinion of something they haven't tried and a lot of people working with say JavaScript or PHP just have never tried a decent ML-style language in anger.

I think Stephen is a tiny bit guilty (as we all are) of that which I'll use Kahneman wording's to put: "Nothing is as important as you think it is when you are thinking about it". There's what seems to be an exaggeration that whatever cost a type system has must be high... it isn't even true of dependently typed programming languages.

I also think product and sum types can be given a free pass to most complaints and while at it, you can throw in first-class function type as a minimum. And I will grant that you can stay away from ad hoc polymorphism and subtyping.

dragonwriter2• 11 years ago

It's fair to say that but it isn't the case that someone can have an worthwhile opinion of something they haven't tried

I disagree. I don't have to try hitting myself in the head with a hammer to have a reasonable basis to believe it would be a bad idea. There's not much point in having reasoning ability if you can't apply it to develop useful opinions on what is and isn't even worth trying.

Obviously, that's not to say that there aren't additional insights possible from direct experience, and that people sometimes apply prejudice rather than sound reasoning to present opinions on things they haven't tried, but its simply silly to say that people cannot have a worthwhile opinion on something they haven't tried.

pekk2• 11 years ago

I don't have any problem with ML, nor do I favor Javascript or PHP. Maybe you shouldn't make so many assumptions.

hawkice• 11 years ago

I have always gotten the impression there was a failure of communication when (without lose of generality) Haskell programmers would tell (also, without loss of generality) Python programmers that Python only has one type, 'object', which appears to violate the understanding of the Python programmer thoroughly enough that there isn't really even a conversation about what is meant by the comment.

The first point dissolves this conversation (because clearly neither the Haskell nor Python programmers are confused about the execution of actual programs). Notably, it dissolves it in a way where that pesky third issue doesn't pop up (which is perhaps the worst of them all, sans _maybe_ the last).

jrochkind1• 11 years ago

What's the "pesky third issue" again?

AnimalMuppet8• 11 years ago

From the article, "Patronizing those outside the faith".

juliangamble• 11 years ago

The 'uni-typed' argument is interesting, but seems to fall down under further examination. This is a comment from some guys at the University of Indiana, who are neither Python or Haskellers, but are working on advanced type systems:

... however Sam Tobin-Hochstadt argues the uni-typed classification is not very informative in practice.

The uni-typed theory reveals little about the nature of programming in a dynamically typed language; it's mainly useful for justifying the existence of "dynamic" types in type theory.

Projects like Typed Racket were invented precisely to discover and model the implicit type information utilised by programmers in such languages. Often types are quite accurate, and shows there's a lot more going on than meets the eye.

http://stackoverflow.com/a/23286279/15441

tel11• 11 years ago

You bring up a very interesting point here. The "unityped" argument is a trivializing one, invented to try to draw bright lines between the worlds of static and dynamic typing.

But it's ultimately a minimal argument instead of an interesting one.

A dynamically typed fragment of code can be interpreted as a program in a statically typed world. From here we can attempt to use inference to partially recover real static information and use it during compilation. This is as old as dynamic languages---typed specialization! It's also a genuinely sophisticated static type system imposed on a genuinely dynamic language.

That's an interesting POV from the compiler's perspective, and it should not be ignored.

The other interesting perspective, though, and the one of more modern excitement, is that it's less about whether or not a program technically has a particular type but whether or not failure to be expressible at "good" types should be brought to the programmers attention immediately!

You can see a statically typed language as a gradually typed language which refuses to compile whenever `any` gets inferred, for instance.

seanmcdirmid6• 11 years ago

To be fair, the type community makes a distinction between types (static entities) and tags (dynamic entities). From their perspective, Python is definitely "tagged" in the sense that tags are checked dynamically, and memory safety is preserved.

On the types mailing list, I think Bob Harper conceded the point that maybe it is more useful to use "type" to refer to dynamic tags when talking to practicing programmers; it is just that in the types community, type has a well defined specific meaning (I can't find a link right now since I'm behind the GFW, but can dig it up later if you are interested).

djur4• 11 years ago

An alternate viewpoint is that static typing advocates invented a novel categorization that allows them to dismiss typing systems they disagree with. "Tag" doesn't have a consistent theory meaning "type determined at runtime"; on the other hand, "type determined at runtime" has been referred to simply as a "type" for decades.

hcarvalhoalves2• 11 years ago

Well, that's an interesting comment. I have almost a decade experience in Python, and having recently picked up Haskell, I clearly see the value of having (or not) a static type system.

I have noticed that during all these years I would just "type-check" the various APIs in my mind, or with the aid of the REPL, but it's not as easy when programmers with less experience join the project. I would often have to explain tracebacks about type errors (e.g., tried to call a missing method on `None`, but the programmer didn't expect that API to return `None`). Strong typing avoids errors from propagating, but without static checking only gets you half-way there.

I would still use Python (or other dynamic language) to introduce someone to programming - not having to reason about types lowers some barriers - but nowadays I'm not sure it pays off for a project expected to be maintained.

crdoconnor3• 11 years ago

I was always on the fence about static typing because I figured that it automatically led to more verbose code (clearly a significant down side), but after looking at Haskell and F# I'm not so sure that's true for them, even though it definitely is for C++ and Java.

I'm still unconvinced that additional testing is required to overcome bugs that a static type checker would catch, though. In my experience all of those "call a missing method on None" issues get caught relatively quickly by a test that you would have to write anyway even if you were using a language with static typing.

tome3• 11 years ago

I'm going to make a few comment and nitpicks.

"Patronising those outside the faith ... Please drop the condescending tone."

This is a great sentiment, but rather jarring to have it followed up by "No sane person can argue that we want to bifurcate a programming language into distinct base-level and type-level fragments".

"Equivocating around “type-safety”"

Surely it's reasonable to use the terminology "type safety" to describe a range of properties that code may have beyond the (supposed) original meaning of "memory safety".

"If everyone would just use a modern language with a fancy type system, all our correctness problems would be over, right? ... Type systems cannot be a one-stop solution for specification and verification."

This is an enormous straw man. No fan of strongly typed languages claims that they solve all correctness problems. Furthermore, the fans of strongly typed programming are the most likely to appreciate the additional forms of verification that Stephen outlines.

AnimalMuppet8• 11 years ago

This is an enormous straw man. No fan of strongly typed languages claims that they solve all correctness problems.

I have read the claim "If it compiles, it works" (or minor wording variations), on this board, more than once (in reference to Haskell). Fans of strongly typed languages do in fact make claims that sure sound like they are saying that.

tel11• 11 years ago

It's said semi-tongue-in-cheek. The original statement was filled with caveats. [0]

Sometimes it's said less tongue-in-cheek. Then it usually has to do with the facts that large refactorings can be handled by merely breaking things and rewiring until types check. This generally does work since types typically guard "wirings".

But taken out of contexts and as the meaning is extended bit by bit it becomes truly ridiculous and nobody would disagree.

So, don't just propagate the rumor. Nobody is claiming miracles. It just sounds like that at around the 8th iteration of the telephone game.

[0]: As far as I'm aware, this is the origin of the idea: http://r6.ca/blog/20120708T122219Z.html

coolsunglasses5• 11 years ago

People get excited when they find out they can have types that are expressive, eliminate many useless bad programs almost for free, and be working in a language more expressive than most.

tome3• 11 years ago

The claim "If it compiles, it works" taken literally is so trivially falsifiable that it cannot reasonably be interpreted as a serious claim that types "solve all correctness problems".

EDIT: I propose that next time you read "If it compiles, it works" you reply with "Are you suggesting that types solve all correctness problems?" I guarantee you that you will not get an affirmative response.

EDIT: I do however take the point that fans of strongly typed programming should act to moderate the excitement of some amongst their numbers in order to reduce the incidence of ambigous or misleading claims.

fsloth4• 11 years ago

If the program is a composed from trivial data conversion steps that are implementable using standard transforms (C++:s stl algorithms, ML:s folds, etc) then it is very likely that it works when it compiles. If there are various branches in the logic and I can encode those branches using types as invariants then that eliminates a particular category of bugs altogether which reduces logical errors. If I use immutable variables it helps even more. I'd say the 'compiles and works' means that if one can leverage existing operations on containers and use types as helpfull invariants then those two stylistic choices reduce the possible number of bugs in various categories.

I would not claim all errors are removed... e.g. numeric code that depends on the precision of arithmetic on floating points is as error prone with or without static types.

mercurial6• 11 years ago

I can confirm that "If it compiles, it works" is tongue in cheek.

However, it's also true that I feel confident that a program in OCaml will be working correctly either the first time, or shortly afterwards, once it compiles (and, just as importantly, will keep working tomorrow or break at compile time). Knowing that the compiler eliminates for you a large amount of potential mistakes is a huge relief, and lets you focus on the parts of your program where the compiler cannot help you and where logic errors are lurking - especially where you are manipulating several values of the same type.

eli_gottlieb3• 11 years ago

Most of the time, that's tongue-in-cheek.

On the other hand, when working with dependent types, the specification is a type, and if the theorem giving that specification type-checks (ie: the "proof" is a program of the appropriate type), then the code is correct, period.

Of course, attempting to prove the theorem can be hair-pullingly frustrating and takes valuable time, but it will expose the assumptions and corner-case you weren't thinking clearly about.

tel11• 11 years ago

With deference to Dr Kell, I think this is overwrought.

He has some good points, points made happily against a particular form of "type cultist" who oversimplifies argument toward making types out to be something magical. They're not, no sane person would think so, but they are a static, syntactic proof system pertaining to the meaning of your programs and there's a lot to be said for such technology.

I am happy to quibble exact points made in this rant, but I'm on my phone so for now I'll merely say that there's a large design space of programming languages and a similarly large (perhap today larger) space of type theories. Matching them up to hit all of your tradeoffs is hard, but there have been some great successes and I would happily contend that any professional programmer owes it to themselves to explore this design space "in anger".

I'm also happy to generally claim that faster, more complete feedback is better than the opposite. Static systems of all regards are faster than "dynamic" ones, and most of them are more complete. This is where you hear about comparisons of types (especially dependent ones) and tests. It's great stuff to think about and explore.

Further, I want to emphasize that SMT solvers are fascinating too and nobody thinks that they're not. The style of proof they provide is more expressive and less certain, though, so the right answer is to know how to combine all of these modes of evidence.

sanderjd• 11 years ago

Type checkers are one way to gain assurance about software in advance of running it. Wonderful as they can be, they're not the only one.

This is true, but in my experience they are far and away the most common and easily tooled automatic way. Tests may run automatically, but they must be manually written, and static analysis tools are not (yet?) very widespread.

colanderman2• 11 years ago

No, I think a separate type-level language is a good thing, so long as my data-level language remains Turing complete (and thus undecidable). I would much rather be forced by the syntax -- by the construction of the language itself -- into a guaranteed decidable subset, rather than have to reason things out myself and get frustrated when the compiler doesn't agree with me (or when it used to agree with me and doesn't any longer!).

Now, there's no reason that the type-level language can't be exactly a subset of the data-level language. I'd just rather not play guess-and-check decidability with the compiler the same way I currently have to play guess-and-check optimizability.

marvy2• 11 years ago

I think the author meant that you don't want two separate Turing-complete languages, one for values at runtime, and another for values at compile time.

eru8• 11 years ago

There are good arguments for not even getting Turing-completeness in your value-level language. Totality would be a nice goal.

See http://blog.sigfpe.com/2007/07/data-and-codata.html

colanderman2• 11 years ago

Oh I totally agree. Unfortunately for many that's far too radical a notion, despite how unnecessary Turing-completeness is for 99.95% of programs written, and how desirable termination is. First you have to convince the Ruby/Python/JS/Elixir crowd of the frivolity of code mutability.

breckinloggins2• 11 years ago

Things that also get my goat (from a less type theoretic point of view):

- Assuming that type checking is the only thing you might want to do with your program at compile time. There are, in fact, arbitrarily many things you might want to do at compile time. Textual preprocessing, expansion macros, type checking, C++ template metaprogramming, etc. are all obvious examples. The fact that most languages bolt all of these things on as one-off features is a sign that something deeper is being missed (perhaps the 3-Lisp[1] idea, for example, or just consider plain ol' Lisp macros).

- Assuming that totality, soundness, and lack of side effects are always type checking virtues. Sometimes I'd like a "typechecker" that isn't always guaranteed to terminate. Sometimes I'd like my typechecker to launch some missiles. This is really more about the previous point.

- Assuming that type checking is NOT desired at runtime. Sometimes it is. Clojure's core.typed has the property that it is "just code" and can therefore be run at anytime and used for things other than checking that your code is safe to ship. [2]

- Assuming that a program that fails type checking shouldn't be run. Maybe it should and the parts of the program that fail type checking should be run inside some monadic context. Maybe we want not only gradual typing, but gradual enforcement. Maybe if we had richer type data, then "failing type checking" wouldn't be binary. Perhaps a program that fails certain type checks has to add runtime support to enable certain features, but if the same program type checked to be about pure memory locations, the runtime would vanish and a "straight to the metal" program would remain. (In other words, maybe what we currently call a language's "runtime" should just be a residue of things that couldn't be checked at compile time, among other things.)

- Assuming that types and the type checker should be a fixed feature of the language. Perhaps type checking should be something that is built as a library from language primitives. Take this far enough and you get something like exotypes. [3] Which reminds me...

- Assuming that "type" is the only kind of metadata you might like to attach to a symbol, expression, or value. There are many other things I might like to express, and I might like to use the usual machinery of type checking to analyze or work with those things. Clojure's value-level metadata and Common Lisp's property lists are some good examples of generalizing this.

- Focusing on manifest typing for verifiability of programs and ignoring the extra information it gives tooling. Visual Studio's IntelliSense and F#'s type providers are examples. At least one person at Microsoft has trouble sleeping at night because he or she is worrying about when the rest of us are going to figure this one out. [4]

- Assuming that most programmers want one or the other. The article touched on this, but I wanted to expound a bit. I would like my original prototype to feel like play-doh and my finished product to feel like concrete. Why do I have to do this in two different languages? "Oh I'll prototype it in python and then switch to Haskell when I want it to be safe." What?

- In general, assuming that it is the job of the language designer to provide the safety nets, rather than the DSL or API designer. A suitably designed programming language is one that could prevent operation Foo in layer 3 while allowing it in layers 1 and 2. This is one reason why languages like Idris are so complicated. Dependent types HAVE to be complicated because the language designer feels that it is his or her job to make sure the part of your program that runs at compile time terminates and doesn't do anything "bad". Why do we rarely question this assumption?

[1] http://lisp-univ-etc.blogspot.com/2012/04/lisp-hackers-pasca...

[2] https://github.com/clojure/core.typed

[3] http://dl.acm.org/citation.cfm?id=2594307

[4] http://blogs.msdn.com/b/dsyme/archive/2013/01/30/twelve-type...

eru8• 11 years ago

Sometimes I'd like a "typechecker" that isn't always guaranteed to terminate.

ghc has an undecidable-instances pragma for that.

kyllo3• 11 years ago

Why do I have to do this in two different languages? "Oh I'll prototype it in python and then switch to Haskell when I want it to be safe." What?

This has always sounded a little crazy to me, too. I did recently have a successful experience at work where I prototyped something in Javascript and then built the production version in Java, but porting the code felt like a lot of wasted effort, compared to if I could just add typechecking to the JS version. A gradual typing library seems like a good way to achieve that.

codygman9• 11 years ago

Sometimes I'd like my typechecker to launch some missiles.

You'd like missiles to be launched at compile time?

breckinloggins2• 11 years ago

Doesn't everyone? ;-)

zak_mc_kracken• 11 years ago

If somebody stays away from typed languages, it doesn't mean they're stupid, or lack education, or are afraid of maths. There are entirely valid practical reasons for staying away. Please drop the condescending tone.

Well, ok, let's hear these practical reasons?

Otherwise, it's just an empty claim.

eru8• 11 years ago

Legacy code (and skillsets) are always a good practical reason.

cbd19845• 11 years ago

It's also nothing to do with static checking—“type safety” holds in all “dynamically typed” languages.

This. Exactly true, and often forgotten.

It's useful here to distinguish between conversions and casts. Conversions use type information to ensure computations remain sensical; the canonical example is a conversion between integers and floating-point values which makes sure you never end up feeding invalid bit patterns into the relevant arithmetic hardware. An example of a cast is taking a bit pattern you had been treating as an integral value and then telling the language it's a floating-point value, and there not being an error at that point.

Conversions don't break the type system; they use the type system. Casts throw types away.

kyllo3• 11 years ago

Casts don't only throw types away, they can also add type information to otherwise untyped input, such as reading data from a file or an HTTP request payload.

dllthomas6• 11 years ago

Arguably, there is an intersection of "cast" and "conversion" where casts are valid.

cbd19845• 11 years ago

Casts don't only throw types away, they can also add type information to otherwise untyped input, such as reading data from a file or an HTTP request payload.

This is true. A more interesting example might be a program which creates database queries from user input casting input strings to the type "unescaped string", and then converting them to type "escaped string" by performing a string-escaping process on them. (A cast from "unescaped string" to "escaped string", which is done implicitly very often in languages where those types are not machine-checkable, is often disastrous.)

tel11• 11 years ago

Type safety also trivially holds in any dynamically typed language. You just call all values the same type---suddenly "preservation" and "progress" hold without actually meaning anything.

That's why its "type safety of a system which captures interesting invariants" which is actually interesting.

http://jspha.com/posts/six_points_about_type_safety/

cbd19845• 11 years ago

Type safety also trivially holds in any dynamically typed language. You just call all values the same type

This isn't what most dynamically typed languages do and I suspect you know it. The reason "1" + 1 works in Perl (that is, produces a defined value rather than an undefined one or a program crash) is because the Perl runtime uses type information to deduce which conversion needs to be performed and then performs it.

The fact the type information is deduced as opposed to declared explicitly doesn't make it anything other than type information.

jeorgun• 11 years ago

While I mostly agree, by this definition most things called "casts" aren't anything of the sort. In C++, static_cast (when called on value types) and dynamic_cast are both conversions, not casts--- static_cast<int>(5.5) returns exactly what you'd expect. Java and C# use C-style syntax, but their semantics are the same as those C++ casts. And of course the same is true of non-C-derived languages like Swift.

By your definition, most "casts" are actually conversions--- and while that's probably true, it feels pretty unhelpful, in the same way that it feels unhelpful to say "Python only has one type".

cbd19845• 11 years ago

I agree that the terminology I used in my post isn't mainstream, and I won't claim it is. However, I couldn't think of a different word which would have the same familiarity with this audience which could plausibly carry that meaning. If anyone else can come up with better words, I'll use them.

To be clear, here's what I mean:

Conversion: The machine looks at the current type to figure out how to transform the value into a valid instance of the new type.

Casting: The machine ignores the current type and simply applies the new type.

michaelochurch• 11 years ago

The hardest objective problem in computer science may be P ?= NP, but the hardest subjective problem is whether it is better to have static vs. dynamic typing in languages. There are extremely intelligent, thoughtful people on both sides... and it's rare in software engineering that there is such an even divide. I'm quite familiar with Haskell, Scala, Clojure, and many other languages... and I still can't conclusively call one better. I prefer static, on a mix of practical grounds, but I realize that it's not a clear victory.

Take the concept of data frames from R, also seen in Python's Pandas library, and probably inspired by the APL family's (column-oriented) tables. It's not a complex concept. Yet it's very powerful for interactive data exploration. It's also a bitch to statically type (see: https://github.com/acowley/Frames). It's more of a leap than lenses (and probably, like lenses, extremely cool once you fully "get" it).

If we have to pull out some advanced Haskell extensions to do something basic in interactive data analysis then I consider that worrying. (This is not to say that Frames isn't a great piece of work. Bringing subtyping into a Hindley-Milner derived language and not having everything go to hell is really hard. See: Scala) And remember, this is coming from someone who's pretty invested in the "static" side.

Clojure also has a world-class aesthetic sense. Haskell is still using camelCase. OCaml uses under_scores; that's better than fuckingUglyCamelCase, but not ideal. Clojure (and the Lisp family in general) is run by people who realize that aesthetics are really important and that allowing hyphenated-tokens is far better than allowing people who hate their space bars to write "a-1" when they should be writing "a - 1". That's just one example. For another, maps. Clojure has {"five" 5, "ten" 10} but Haskell has fromList [("five", 5), ("ten", 10)]. My point is that (which I prefer Haskell, for its types) Clojure's aesthetic sense is arguably better, and I would say world-class, especially considering that it runs on a butt-ugly platform (JVM) and is still a beautiful language. We need to keep watching that community closely because they're doing some great work in a wide variety of fields, including front-end development (ClojureScript).

Type systems don't just make you write annotations; they force you to structure your code around type-checkability. This is inevitable, since type checking is by definition a specific kind of syntactic reasoning.

There is some truth around that. Just to get data frames, you need row types which means you have subtyping, and that complicates type checking considerably. Haskell (see Frames) uses multiple "experts only" language extensions to get something that "just works" for casual use but requires advanced knowledge to grok the types. It's great work, but its difficulty shows that we can't just ignore subtyping.

The counter-argument that I'd make is that 95+ percent (maybe more?) of all functions that are ever written ought to have simple static types. So much of code, when it is clean, is already well-typed, even in a dynlang. The difference is that, in a static language, the compiler yells any time someone fucks that up in refactoring. And, more generally, you learn about errors (not all errors, but a surprising percentage of them) sooner and that's a good thing. In a dynamically typed language, you see a lot of functions that evolve into multimethods that do different things per input type(s) and (although usually this won't happen if the code is maintained by decent designers) you can get O(n2) or worse complexity in the functionality. If you're programming defensively in a dynlang, you have to think about all the crap that might be passed into your functions. "What's a Matrix plus a Scalar? How about a RowVector plus a ColumnVector? How about a Sparse2DArray plus a DataFrame?"

On the whole, I'd rather be in a statically-typed language for a program of any size, and I'm stodgy and conservative and old (but efficient and concise) so, for me, "big code" starts around a couple thousand lines. I hate writing boilerplate unit tests that a compiler and a type system would knock out automatically. But I do have to give Clojure a lot of props for its community and its aesthetic sense, and I think that the above obviously derive from its ease-of-use and its Lisp heritage, both of which are tied to a feature (dynamic typing) that I otherwise wouldn't much like.

The main question that I've been pondering for a few years (and not coming to satisfactory answers) is whether it's possible to unify the cleanness-of-language and aesthetics of Clojure/Lisp with the static typing of Haskell... and not get some hyper-complex type system that results in compile-speed problems at scale (e.g. Scala under typical use). It's an open problem.

eru8• 11 years ago

(It should also do so using a straightforward explanation, ideally featuring a counterexample or stripped-down unprovable proposition. I don't know any type checker that does this, currently.)

I guess the incomplete-pattern-matching warnings (in eg ghc) come closest. They usually give you an example of an example of a value you haven't matched. But that's a very restricted and simple domain.

fsloth4• 11 years ago

I think the argumentation here is a bit a skewed towards 'what static types can and cannot do for the compiler' - i.e. how they can help the computer in constructing formal proofs. For me another almost as valuable thing is how static types help me think about and design the code. The static type information is always there to remind "this entity belongs to this set of objects" which frees me from the cognitive burden of maintaining this constantly in my working memory. With specific static types the function signatures now document the tranforms defined for those entities . This aspect of static types as a cognitive tool is highly personal, and not same for everyone, unlike the language and the compiler, though.

wyager• 11 years ago

I emphatically reject the many of the conclusions of this article.

Let me say it simply. Type systems cannot be a one-stop solution for specification and verification.

Wrong! Any correctness property can be encoded into a sufficiently powerful type system. Which brings me to...

Curry-Howard is an interesting mathematical equivalence, but it does not advance any argument about how to write software effectively.

This is absurd, of course. The isomorphism between type systems and proof systems allows us to build lots of impressive systems like Agda and Coq.

No sane person can argue that we want to bifurcate a programming language into distinct base-level and type-level fragments.

That's actually quite a reasonable desire.

Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code.

To the author, this seems to mean "therefore, we shouldn't have types!". In reality, a sufficiently flexible programming language allows you to write type-level code in the same language as value-level code. See Agda.

Rich Hickey's transducers talk gave a nice example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic.

Lots of people have typed transducers just fine... http://blog.podsnap.com/ducers2.html http://conscientiousprogrammer.com/blog/2014/08/07/understan...

djur4• 11 years ago

To the author, this seems to mean "therefore, we shouldn't have types!".

This doesn't follow from the author's earlier statements about using and benefitting from languages with static type checkers. An ideal typed Lisp dialect would fit the author's requirements.

jroesch3• 11 years ago

An ideally typed Lisp would be no different then a dependently typed language semantically.

Yes, you would use slightly different syntax but a key feature of most dependently typed languages is that they only have a single class of pseudo-terms that are used for both types and programs.

An example Idris program:

   double : Nat -> Nat
   double n = 2 * n
   
   ourVectorType : Type
   ourVectorType = Vect (double 1) Int

   aVector : ourVectorType
   aVector = [1, 2]

If you change everything above to an S-Exp you have a typed Lisp where both types and terms have the same language.

danielscrubs• 11 years ago

Excellent points. Thanks.

jedharris• 11 years ago

Thanks for refuting by example all the other comments that say "The author is wrong because no one actually believes those things."

AnimalMuppet8• 11 years ago

>Let me say it simply. Type systems cannot be a one-stop solution for specification and verification.
Wrong! Any correctness property can be encoded into a sufficiently powerful type system.

I'm writing a factorial function. But, because the caffeine hasn't kicked in yet, at the recursion step, I add one instead of subtracting one. The result is that the program will run in an infinite loop until either the fixed-size Int rolls over to 0, or the bignum-style integer consumes all available memory. That's certainly incorrect behavior. But I'd like to see your "sufficiently powerful type system" that will handle that.

Then there's numerical accuracy. Here the results are not "wrong wrong", they're just "a little bit wrong" or "less accurate than they could have been". Again, I'd like to see your type system detect that.

In my world, embedded systems, you can get hard-real-time situations, which means that the right answer, too late, is wrong. I believe that there are formal verification tools, but they don't look anything like a type system. And even those tools depend on a very deep knowledge of the processor that the code will be running on (not compiled on). Once more, I'd like to see your type system that's going to handle this.

> Curry-Howard is an interesting mathematical equivalence, but it does not advance any argument about how to write software effectively.
This is absurd, of course. The isomorphism between type systems and proof systems allows us to build lots of impressive systems like Agda and Coq.

And if Agda and Coq were being used to write much software, you'd have a point. But if I understand correctly, they're mostly used for automated proofs. The point is that the program compiles, and therefore something is proven. The point isn't to get a runnable program.

codygman9• 11 years ago

The result is that the program will run in an infinite loop until either the fixed-size Int rolls over to 0, or the bignum-style integer consumes all available memory. That's certainly incorrect behavior. But I'd like to see your "sufficiently powerful type system" that will handle that.

I believe that Agda could do this.

mercurial6• 11 years ago

The Sniveley/Laucher talk included a comment that people like dynamic languages because their syntax is terse.

Sure. Trying to have a strongly-typed Java program, for instance, means a lot of boilerplate. As a consequence, it's often not done, or at least not done enough.

To suggest that any distaste for types comes from annotation overhead is a way of dismissing it as a superficial issue.

On a large codebase, there is nothing superficial about it. The more boilerplate you have, the more difficult it becomes to understand the codebase and to find code which actually does something.

If everyone would just use a modern language with a fancy type system, all our correctness problems would be over, right? If you believe this, you've drunk far too much Kool-Aid. Yet, apparently our profession is full of willing cult members. Let me say it simply. Type systems cannot be a one-stop solution for specification and verification. They are limited by definition. They reason only syntactically, and they specify only at the granularity of expressions. They're still useful, but let's be realistic.

Let's be realistic, and not pretend this is a widespread opinion.

Rich Hickey's transducers talk gave a nice example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic. Usually they are captured only overapproximately, which, in turn, yields an inexpressive proof system. The end result is that some manifestly correct code does not type-check.

Possibly, but it's all a question of tradeoffs. There is a lot more incorrect than correct code which doesn't typecheck.

mateuszf3• 11 years ago

On a large codebase, there is nothing superficial about it. The more boilerplate you have, the more difficult it becomes to understand the codebase and to find code which actually does something.

In case of types it's true for humans. IDE will be able to build a very precise model and ease navigation and code changes when it understands types.

superuser2• 11 years ago

Why should this be a property of the IDE and not the language itself?

No, seriously. If the language sucks but your interaction with the IDE is fine, why not have a language that is closer to your interaction with the IDE to begin with, and use a text editor?

mercurial6• 11 years ago

IDEs can help, but they're not a panacea. There is still a mental overhead when dealing with a more verbose codebase. Not to mention increased programmer time, especially when coding guidelines mandate the creation of builders.

fsloth4• 11 years ago

This topic of "what are static types good for" continued to bug me because I could not formulate a concrete answer to myself. I found the following Reddit discussion

http://www.reddit.com/r/programming/comments/lirke/simple_ma...

Which had eventually the specific thing I was after in a comment by Rich Hickey which helped to nail the concept I was after

"Statically typed programs and programmers can certainly be as correct about the outside world as any other program/programmers can, but the type system is irrelevant in that regard. The connection between the outside world and the premises will always be outside the scope of any type system."

Which is precisely why I enjoy types: Self referential consistency makes sure I do not make errors within the logical model I have set for myself. It does not help me build better models but once those models are built it helps me to compose programs that do not break the invariants in the chosen formalism.

Which, I think tells exactly what static types are good for: For those sort of problems that benefit from having a formal specification. There are a lot of programs that have this quality.

So the argumentation is a bit skewed off. It should not be about whether static or dynamic types are better but more focus on what are those identifiable problem patterns where a dynamic type system helps programmer create more value than a static one and vice versa.

shadowfox• 11 years ago

Self referential consistency makes sure I do not make errors within the logical model I have set for myself. It does not help me build better models but once those models are built it helps me to compose programs that do not break the invariants in the chosen formalism.

I think this is a valid point.

But I am less convinced about the second part. I feel that better type systems do help one model the world better (while retaining the consistency checking that you mentioned). In my mind at least having more/better "type tools" is like having differently shaped pieces in your lego tool box. You can create better models for yourself, because the pieces allow you to. And the more experience you have with them, your modeling abilities also improve.

tel11• 11 years ago

The thing about "the outside world" is that it is just one form of interpretation of a chunk of code. Inarguably, it is the most important one, but once you recognize that it is not alone in that regard you get a very new appreciation for "internal consistency".

Ultimately, this becomes an issue of "minimize your interfaces" which is widely known to be close to vital for writing successful code. If you can "purify" most of your code base then use types to ensure that it has internal consistency then the remaining task is to write (at least) one valid, trusty "interpreter" from your pure/trusted codebase into the real world.

This is undoubtedly the most fragile piece of your application!

But it's also eminently library-able and it places the risk-burden over a tiny fraction of your code. It's also the place where you want to property/unit/integration test the hell out of the world.

So all of the standard CS adages apply again, but thanks to purity/type-checking you've reduced the risk exposure to a tiny fraction of what it is while using other tools.

raiph• 11 years ago

Perl 6 elegantly blends static nominal typing and arbitrarily loose or tight dynamic constraints.

The following slides were published a week or so ago and should demolish most folks' overly simplistic view that one or other is best or indeed that they don't play well together:

http://jnthn.net/papers/2015-fosdem-static-dynamic.pdf

Seven deadly sins of talking about “types” (2014)

Related Stories