Lambda the Ultimate

"Many people in the lightweight community seem to have a certain antipathy to type systems. I would class them into a few off-the-cuff categories:

1. Never programmed in a typed language.
2. Can't stand the type annotations.
3. Believe the idea of constraint (which is fundamental to a type system) is evil, especially during prototyping.
4. Have a deep understanding of types of all sorts, but aren't comfortable with them for reasons that'll take hours to explain.

Most people I've encountered in this community who claim to dislike types fall in the first three categories. Shockingly often, they have never programmed in ML (SML or OCaml). I contend that most of them can be cured of most of their antipathy by a sound dose of ML.

Of course, types are only a starting point for making claims about the robustness of a program's behavior. There are much more sophisticated means of validating programs that go far beyond the very simplistic set of (mis)behaviors covered by most type systems."

from Lightweight Languages list

5. Have programmed in various statically type checked languages from C and Java to Haskell and ML, but have not found a productivity increase over simpler, dynamically safe languages accompanied by test-driven design.

Interesting patterns may well emerge. I suspect that most ML and Haskell fans spend a lot more time writing programs that need to manipulate complex data structures than I do. (If not, that would be very interesting!)

If people knew how embarrassingly simple the types in most of my programs are, I wonder if they'd bother recommending static checking to me. :-)

Possibly true, but I think that has more to do with the way ML/Haskell people implement things than it has to do with the sorts of (specifications of) programs they write. In a typed language one tends, unsurprisingly, to want to exploit the type system to preserve static invariants and to avoid as much as is possible (or practical) forcing things to share the same representation.

For example, if I need to represent the days of the week in Haskell, I might introduce a new type:

data Week = Sunday | Monday | Tuesday | ...

whereas in C one would just typedef int and in Scheme one would use symbols, both of which unnecessarily force a choice of representation.

Now if I want to represent a weekly schedule, I might define:

data Schedule = Schedule (Week -> [Event])

whereas in C or Scheme one could just use an array/vector, since the indices are numbers. So you see how these things tend to propagate.

Now, of course, there is nothing preventing me from representing Week as a subset of the integers in Haskell; neither is there anything preventing me from representing Week as an abstract datatype in C or Scheme (well, assuming a module system or using procedural abstraction to hide the implementation type).

However, because C's type system is so weak, and because Scheme doesn't catch static type errors, it's not practical; as I see it, these languages tend to place more burden on the programmer to remember when something is implemented abstractly or not. So one tends to reduce that burden by not implementing things abstractly.

whereas in C or Scheme one could just use an array/vector, since the indices are numbers. So you see how these things tend to propagate.

Is this a good time to mention Smalltalk or Python? Or even a more abstract implementation in Scheme?

Frank's post seems to be a bit of a strawman argument otherwise.

Frank's post seems to be a bit of a strawman argument otherwise.

I'm a bit bewildered by your response. In the part you quote, I try to explain why in statically typed languages types tend to get more complex as a program grows larger. And then you accuse me of setting up a strawman argument....?

This reminds me a bit of the scene in High Fidelity where Barry brings a tape in to the record store on Monday morning.

                         BARRY
            Don't you want to hear what's next?


                         ROB
            What's next?


                         BARRY
            Play it.


                         ROB
            Say it.


                         BARRY
                   (sighs)
            "Little Latin Lupe Lu."


Rob groans.


                         DICK
            Mitch Ryder and the Detroit Wheels?


                         BARRY
                   (defensive)
            No.  The Righteous Brothers.


                         DICK
            Oh well.  Nevermind.


Barry bristles and moves slowly in on Dick.


                         BARRY
            What?


                         DICK
            Nothing.


                         BARRY
            No, not nothing.  What's wrong with
            the Righteous Brothers?


                         DICK
            Nothing.  I just prefer the other
            one.


                         BARRY
            Bullshit.


                         ROB
            How can it be bullshit to state a
            preference?

Also, is the definition of "type error" likely to be broader than I might expect? If so, can you give a surprising example?

(Actually, it seems a bit silly to ask these questions. Obviously serious first-hand experience is required to appreciate both ML-like type systems and Lisp/Smalltalk/Erlang-like interactive programming. Otherwise we'd all understand each other perfectly after the many debates around the 'net.)

Some type systems let you express things that require program logic otherwise. Whether this is a good thing depends on the situation.

Consider a simple example. My students just had to turn in an assignment (using Ada) in which a DFA (finite state machine) was implemented, and used to search for occurrences of a pattern inside a longer string.

Ada generic units are the subject of this exercise, so we ask them to create an Ada package that is parameterized by the parameters of a DFA: Sigma (the Alphabet), the set of states (Q), the starting state (q0), the transition function (delta) and the set of final or accpeting states (F).

Since this is Ada, the set of states can be represnted using an Ada enumeration type (similar to the weekday type Frank showed in Haskell). Ada generic units can have type parameters. The same thing can be done with sigma (in fact the builtin type Character is an enumeration type).

Now consider the question of representing the transition function. You can pass a funcion parameter. However, you can also pass a matrix. Since arrays in Ada are normal arrays (not associative arrays) they can only have indexes that are discrete types. Enumeration types qualify. So if we represent Q and sigma as enumeration types, we can pass a matrix (with indexes of type Q and Sigma) for delta. Had we chosen to represent Q as a list (or array) of state names (strings), we would have needed to translate these names into array indexes ourselves. Using enumeration types in this, array indexes come for free.

It's not a matter of good vs. bad. It's just the enumeration types add to the expressiveness of the language.

While I am discussing this example, let me mention one more thing. The DFA package provides an operation Consume_Char that takes a char from sigma and advances the DFA. Notice that this routine doesn't need to check that the char belongs to sigma, since Consume_Char is defined as receiveing a parameter of type sigma.

Only last example: If we represent delta as a matrix, we can be certain the the package is provided with information about what to do for each (char,state) pair, since the matrix spans both indexes.

There's a lot more to this simple example, but I think it's enough to give a flavor of what typeful programming can mean, even in a language with a type system weaker than H-M (with function types etc.)

in my (limited) experience, it helps in the following four ways. since i've not had that much experience of dynamic typed languages, these are mainly positive things that seem to be related to the type system; maybe there are alternative approaches if you don't have types.

- like you said, it catches bugs. to be honest, it's not as big a step (in my experience) as going from weak typing (ie c) to strong checking (eg python) (i'm currently working in a weird language that's fortan plus c's dynamic memory, with untyped pointers, and it can be *hell* to debug, but that's mostly because of lack of checking, rather than static typing) (sorry, i tell a lie, for the last month i've been working in the scripting "language" for the system, which - get this - doesn't even have functions (it has arrays, but they're broken, so in practice you use temporary files on disk as arrays.... sigh))

- when you're hacking code around ("refactoring") you can exploit the type system to tell you where things have changed. this is hugely useful when you're dealing with a pile of horrible ill maintained code. in practical, get-your-job-done terms, this seems like the biggest advantage of static typing (i used to work with java and this saved my ass so many times...)

- it clarifies higher level functional programming. maybe this is just because i'm still not so good at it, but i find type annotations really useful in understanding what's happening when messing around with haskell. i'd tried programming in a similar style in lisp, but got lost. no doubt that's largely because i was so clueless (i can't separate out the two effects without going back to lisp, and i really can't be bothered; if i were doing it again, i'd add type annotations to the lisp, even if they were just comments).

- it lets you specify interfaces (i guess this is partly catching bugs and partly documentation). i debated including this, but cardelli mentions it too (i believe there are quite sophisticated package systems for some of the schemes, but i don't know how they work or what they do, exactly).

i don't pretend for a minute that these are fixed things that apply to everyone, or that there's no disadvantges to static types (there certainly are!). it's just personal experience. at the moment, i think haskell is fun, but i couldn't promise that in 10 years time i won't be playing with scheme and enjoying myself just as much...

hmm, having written all that, and read it, i guess i can state things more succinctly: it provides formal documentation, in a style that helps understand and specify complex behaviour, and which can be verified automatically. the system (documentation and verification) can be exploited to find code that is inconsistent with changes in the specification.

andrew

Andrew: Your experience is so familiar that it reminds me of something I had forgotten completely: that I have been a static typing fan for most of my life, and only began to take dynamic typing seriously a few years ago. It feels like another life :-)

Today Amazon shipped my copy of The Haskell School of Expression, so perhaps I'll be a static typing fan again soon enough. (I mostly bought it for the lazy evaluation, since that clearly matters).

I see your types as a good thing, better than just using "representations", i.e. integers and arrays.

But I also see objects in a language like Smalltalk as a good thing, maybe better than types in Haskell. And I see the use of either functions or "home-grown objects" in Scheme as being at least as good as Haskell's types.

Both types in Haskell and objects in Smalltalk are better than "representation" conventions in C.

I thought the straw man was comparing types to "representations" only in Scheme. Clearly types are better in this dichotomy.

However, to suggest this is only a dichotomy, and this example as a typical use of Scheme is what concerned me. Maybe it is "typical", I don't know. But it's not "good" and so it's not what a good Scheme programmer would recommend.

For some of us, static typing feels like it helps with creativity. Once the roles of a few major data structures and/or components in a program have been decided, this partial structuring can serve as a spur, a guide to further creative development.

I think of this effect as analogous to writers restricting their writing to a certain form (a sonnet, or a book that avoids the letter "e"); or to a songwriter tuning his guitar to unusual or unfamiliar tunings, in order to "stir the muse".

http://www.ai.mit.edu/~gregs/ll1-discuss-archive-html/msg04543.html http://www.ai.mit.edu/~gregs/ll1-discuss-archive-html/msg04551.html

... in two of the more sensible postings I've seen in any of the current eternal DT vs ST debates. See comp.lang.lisp and comp.lang.functional if the discussions here and on the LL1 list aren't extensive enough for you. :-)

type Angle = Double
type Age = Double

data Angle = Angle Double<br/>
data Age = Age Double

(Hmm. Subclassing would work just fine.)

(All this modulo whatever simple and patently obvious solution Frank posts in a moment...)

Andrew

i deleted that from my list before posting! :o)

newtype Angle = Angle Double
newtype Age = Age Double

will get you two typesafe aliases for Double. The 'newtype' declaration declares that Age and Angle are synonyms for 'Double', but can't be used interchangeably. If you did this with 'data' instead of 'newtype', you'd be declaring a record with one Double field, whereas 'type' and 'newtype' declare aliases for some other type, in this case Double. The 'newtype' version does require the constructors to be used, but the compiler strips them once it's sure you're using them safely. At run time it's just a Double.

I don't like to post solutions to exercises on the net, bu I am sure I will be able to find something to send you by email if you want.

I guess that depends on you. If you exploit the type system, it will catch errors for you, including some kinds of errors that can provably never be caught by any form of testing, for example violations of desired properties quantified over an infinite domain. If you don't exploit it, well, then it won't catch such errors.

Frankly, though, I think the practical value of a type system lies at least as much in its role as formal documentation, as Andrew noted. It provides an abstract overview of a system. If you think of a program as two-layer entity, then with the top layer being the types, and the bottom layer being the values, then a type is a top-down abstraction of the overall behavior, so types are useful for planning and designing. It gives you something concrete and formal which you can write down, and even run through a compiler to check consistency and so on, even if you haven't fully conceived the program behavior.

In that particular sense, I think, types encourage incremental program development and experimentation, contrary to what dynamic typing advocates claim. DT also encourages that sort of thing, but the way it does is very different. The difference is like the difference between recursion and iteration. In recursion, you are always dealing with a `complete' data object, though that object may be a subobject of some other. In iteration, for example a for-loop, you are only dealing with bits and pieces of a complete object. Similarly, in an ST language, a type also describes a `complete' object, namely a program or expression; it's an incremental description in the sense that it doesn't give details about behavior. In a DT language, one gets incrementality (is that a word?) rather by leaving out definitions of names that, at the present stage in develop, won't get evaluated, or by only handling branches that won't, presently, be taken; in that sense you are dealing only with bits and pieces of the desired program.

Patrick: But I also see objects in a language like Smalltalk as a good thing, maybe better than types in Haskell. And I see the use of either functions or "home-grown objects" in Scheme as being at least as good as Haskell's types.

I think this is comparing apples with oranges. You can have objects and functions in statically typed languages as well, after all.

I thought the straw man was comparing types to "representations" only in Scheme. Clearly types are better in this dichotomy.

OK, but my point was rather that DT discourages abstraction because it leads to what some people (not me, though) consider `spurious' errors. For example, if the days of the week are represented as numbers (inabstractly) then you can use the usual arithmetic addition operator to increment a day. If you represent them abstractly, then if a programmer inadvertantly tries to add 1 to a day, you get a dynamic type error. The program would have `worked' if you hadn't abstracted the type. In that sense, there is a risk factor attached to abstraction in DT languages. In a statically typed language, though, errors of this sort are always caught statically, so there is no risk associated with making a type abstract.

scruzia: For some of us, static typing feels like it helps with creativity.

Yes, I feel that way. At the very least, writing down a type gives me something concrete to look at and think about. Sometimes I recognize a pattern, and can pull in knowledge from other areas like category theory.

Andrew: [re: Angle and Age]All this modulo whatever simple and patently obvious solution Frank posts in a moment...

First, observe that this has nothing to do with static typing. In a DT language, you would have to insert the constructors as well.

Second, no, sorry, there is no good solution for this in Haskell. I agree it's irksome and people complain about it a lot. In Generic Haskell, you could write a generic addition function which works on both those types, as well as normal arithmetic types, but it's a bit annoying because you have to mention the type anyways:

add{|Angle|} angle1 angle2

In Arrow, I think, you'll be able to do something similar, without needing to mention the type in brackets.

Here's my twopenn'orth on this. I opine that Python (DT) beats languages with primitive type systems, but is the poorer for not having a sophisticated type system. Bear in mind that as I'm a scarcely-literate savage myself, my idea of a "sophisticated" type system is basically Haskell...

Generic Haskell doesn't handle existential types. I would say that any extension to GH which did handle them should preserve such abstractions, otherwise it is broken.

Generic Haskell doesn't handle existential types. I would say that any extension to GH which did handle them should preserve such abstractions, otherwise it is broken.

Too bad; I was hoping the answer was "yes" and you had some simple, obvious mechanism for implementing it that would make me shout "D'oh!" when you explained it. :)