type safety

I’d really like it if there was static type checking in a python-like language that could be turned on after initial prototype development. That way I could hack something quick and dirty together, and then I could turn on type safety level 1, and find some places that have type problems, and then fix them, then turn it up to level 2, with more crunching, that would find more problems, up to some level of maximal safety where the code is as safe as ML or OCaml or Haskell.

This could serve as a nice bridge from traditional programming techniques to more PLs-ish programming techniques. Sort of a trojan horse that you could sneak into a more traditional software house that could lead to type-safe practices, but it wouldn’t get in the way of rapid prototype development or quick hacks.

Sort of like ‘use strict;’ in perl, but instead of taking the language from wretched to almost-not-wretched it would take the language from ‘type unsafe’ to ‘type safe’ in a gradual fashion. Perhaps it would also be analogous to adding stricter compilation flags to C code, (-Wall and -Werror come to mind here) but the guarantees would be stronger.

Published 27 July 2005

Filed in

mphair

I've been learning Lisp recently and I think that it the answer. Specifically, CLOS allows you to be as specific as you want to be.
if you want to stick with python, don't decorators provide something of that nature?
Peter

Expanding on that notion of a gradual transition from flexibility and development speed -
Type safety provides a bunch of guarantees beyond those provided by unit tests, and does so in a programmatic way that compilers and interpreters can take advantage of. So this gradual transition from the loosey-goosey system should also be a gradual transition from a slower system to a speedier system.
Much like people saying that "speed is a feature - add it in at the end if it's required", I think this should be expanded to "type safety is a feature - add it in at the end if it's required".
Peter

Right - we'd need some sort of early binding semantics that exactly matched the late-binding semantics.
The system I'm also envisioning, would, for each chunk of code, spit out 'known to break', 'known to be safe', 'maybe safe, depending on X', or 'uncheckable'.
Also, while I really like late binding and Alan Kay's ideas, systems tend to ossify and harden over time. They get too many dependencies to be effectively changeable. So, in reflection of this fact, it would be nice if we could harden the underlying code via type safety guarantees.
But for system development, late binding and loosey-goosey types are where it's at. I just think it's unfortunate that people tend to write their prototypes and their final products in different languages. There could be a big win if we could provide a gradual transition from the development speed and flexibility of the first to the safety of the second.
mphair

the problem would be the actual transition from level 0 to level 1. python is quick and easy partially because you dont need to worry about type at all. to go to the next level, you would need to add all of the types in. it'd be like people going back to add in documentation: (1) wouldn't happen, (2) might not be correct, because they dont remember what the function was for. i guess you could have it allow you to type things upfront and just not check them...
in addition, with static type checking you lose the late-binding nature, don't you? alan kay would hate you. of course, he's unemployed right now, so what does he know? ;)
Peter

The issue is that type checking is like unit tests you get for free! Whether people are test-infected or not, it's still nice to be assured that at no point are you ever going to do an operation that is impermissible. The entirety of academia is completely sold on type-theory, and it does seem to provide benefits in practice as well, but there's a whole set of bondage-and-discipline and waterfall design practices implicit in their approach.
I'm proposing that we steal their good ideas (type theory) but get rid of the languages that force you to do a big design up front by refusing to run code that only 50% works.
I'd like the benefits of SML and Haskell typing, combined with the loosey-goosey "code it up right now and then refine each level as you go" style of Python and Perl and Ruby and Lisp. This is the best way I can think of getting those.
Unit tests are nice, and they help a lot, but guarantees about code that are backed up by theory are really nice as well. If we could combine rapid application development and unit tests with strong typing, then I think it could be a huge win.
The way I tend to develop systems is I write a halfass hack, and then I extend and change and refactor it into something even biugger and better. So my ideas start out wispy and thin, but as I go they get more and more concrete. A nice type system could really be a helpful solidifier for that concrete, as long as it didn't force me to pour concrete for my first pass through the problem.
Peter

Comments problem should be fixed now...
misuba

Well, if you're willing to accept "writing some unit tests" as a means of "turning on typesafety level 1," you can get this most anywhere...
type safety

comments appear on wrong post
jes5199

get test infected
http://www.artima.com/weblogs/viewpostP.jsp?thread=4639

blog comments powered by Disqus

learning »
« organic systems

Impromptus

type safety

About Peter

Photostream

Bookmarks feed

Twitter

Meta