Type warnings

[pozorvlak]

Here's something that occurred to me the other day: consider duck-typed languages like Python. The idea of duck typing is that if something walks like a duck, and quacks like a duck, then it might as well be a duck. Or rather, if something walks and quacks in a sufficiently ducklike manner, it doesn't really matter for your purposes whether it actually is a duck or not. Less metaphorically, we don't specify that the arguments to our functions can only accept (say) Integers, we only specify that they have to have an add() method. In fact, duck typing as commonly understood goes further: we don't explicitly specify a necessary interface at all, we specify it implicitly by the methods we call on our arguments.

An example is probably in order. Consider the Python code

def foo(bar, baz) :
    bar.spoffle()
    bar.buffy(baz.willow())
    baz.xander(bar.angel())

From that code, we can deduce that the first argument to foo must have methods called spoffle, buffy and angel, and the second argument must support methods called willow and xander. Now, here comes the clever bit. That's all that's necessary for foo to work. Supposing some clever hacker comes along later and invents a new datatype which it would make sense to foo, all they need to do to allow your code to work on theirs is to implement those methods in a sensible way. This can be done without any knowledge or forethought on your part. Maybe you honestly believe that fooing is something that can only be done to ScoobyGang objects, but in fact the algorithm is much more general, and will work with any TeenSuperHeroTeam. It doesn't matter: your code will still work. To achieve the same effect in Java or Haskell, you'd have to have defined a Fooable interface explicitly, and users of your library would have to start their code with a raft of

instance Fooable TheThem where ...
instance Fooable AquaTeenHungerForce where ...
instance Fooable PowerRangers where ...

type stuff. This is in fact how most of my Haskell code ends up looking: I find typing it almost physically painful. Until the RSI starts to kick in, at which point it becomes actually physically painful. And that's in the good case, where the author of the library I'm trying to use has thought about the kind of generalisation I want to make and defined the relevant interfaces.

OK, so far so standard. Now, most duck-typed languages are dynamic, which means that we only try to determine if bar has a spoffle method at runtime, and die with an error message when it doesn't (possibly after trying some error recovery, e.g. by calling an AUTOLOAD method or similar). But it occurred to me that in simple cases (which is to say, the majority), we could work out most of this stuff statically. For each function definition, see what methods are called on its arguments. Recurse into functions called from that function. Now, each time a function is called, try to work out what methods the arguments will support, and see if that includes the interface required by the function. Issue an error if not. Thus we get the code reuse benefits of duck typing, and the correctness benefits of static checking. If the static checking is slowing down your development cycle too much, drop back to fully dynamic checking, and only run the static checks on your nightly builds or something.

This also cleared up something else I'd been vaguely wondering about. In his splendid Drunken Blog Rant Rich Programmer Food, Steve Yegge says

Another problem is that they believe any type "error", no matter how insignificant it might be to the operation of your personal program at this particular moment, should be treated as a news item worthy of the Wall Street Journal front page. Everyone should throw down their ploughshares and stop working until it's fixed. The concept of a type "warning" never enters the discussion.

I'd wondered at the time what a type warning would mean. When is a type error mild enough to only warrant a warning? Here's one idea: a type warning should be issued when it cannot be proved that an argument to a function implements the interface that function needs; a type error should be issued when it can be proved that it doesn't.

This all seemed very interesting, and struck me as potentially a fun and reasonably easy hacking project, at least to get something workable going. But if it's occurred to me, it has probably occurred to someone else, so I asked the Mythical Perfect Haskell Programmer if he was aware of any work that had been done on static duck-typed languages. "Oh yes," he said, "O'Caml's one." Buhuh? Really? Well, that's O'Caml moved a couple of rungs up my "cool languages to learn" stack...

Comments

[ryani.livejournal.com]

In Haskell, you're right, you do this by putting every primitive function in its own typeclass.

And you're also right that generally you can figure that stuff out statically.

But in Haskell (or rather GHC), sadly, you generally don't get that static analysis, and instead you end up with functions passing dictionaries/virtual-function-table-pointers around all the time.

[pozorvlak.livejournal.com]

Interesting - I wasn't really thinking about the code generation end of things, just the correctness-checking end. I find it amusing, actually, that while the kind of optimizations that one could do are often cited as benefits of the Static Way, very few compilers seem to actually do them :-)

[Though dynamic/duck-typed languages could also be a lot faster (http://www.avibryant.com/2006/09/ruby-and-strong.html), apparently.]

[necaris.livejournal.com]

Seen any of the profiling bits of PyPy? That kind of runtime profiling and optimization seems to be entirely what they're after...

[pozorvlak.livejournal.com]

In Haskell, you're right, you do this by putting every primitive function in its own typeclass.

I think it's a bit harder than that: you'd need a typeclass for every function's interface and every intersection of those interfaces that occurs. So if you had

foo buffy = spoffle buffy (winnow buffy)
bar angel = spodify angel (winnow angel)

then you'd need typeclasses as follows:

class Winnow where
    winnow :: a -> Winnowed a

class Fooable where
    spoffle :: Winnow a => a->(Winnowed a)->(Foo a)

class Barable where
    spodify :: Winnow a => a->(Winnowed a)->(Bar a)

One typeclass per primitive function

[ryani.livejournal.com]

Assuming "spoffle", "spodify", and "winnow" are all primitive functions (that is, they need to be created for all combinations of types that can be passed as parameters):

class Winnow a b | a -> b where
    winnow :: a -> b

class Spoffle a b c | a b -> c where
    spoffle :: a -> b -> c

class Spodify a b c | a b -> c where
    spodify :: a -> b -> c

foo :: (Spoffle whedon winnowt ans, Winnow whedon winnowt) => 
       whedon -> ans
foo buffy = spoffle buffy (winnow buffy)

bar angel = spodify angel (winnow angel)
-- GHCi infers type of bar as
-- bar :: (Spodify a b c, Winnow a b) => a -> c

If instead, winnow was required to return an object that had a particular interface:

-- class Winnowed a where
--   winnowInterface1 :: a -> String
--   winnowInterface2 :: (Num b) => a -> [b]
-- or, more generally:

class WinnowInterface1 a where
  winnowInterface1 :: a -> String
class WinnowInterface2 a where
  winnowInterface2 :: (Num b) => a -> [b]
class (WinnowInterface1 a, WinnowInterface2 a) => Winnowed a

-- instance declaration needs -fallow-undecidable-instances
-- alternatively, you can manually instantiate for all types that
-- support the interface
instance (WinnowInterface1 a, WinnowInterface2 a) => Winnowed a

class Winnowed b => Winnow a b | a -> b where
  winnow :: a -> b

class Spoffle a c | a -> c where
  spoffle :: Winnowed b => a -> b -> c

class Spodify a c | a -> c where
  spodify :: Winnowed b => a -> b -> c

foo :: (Winnow whedon t, Spoffle whedon ans) => whedon -> ans
foo buffy = spoffle buffy (winnow buffy)

bar angel = spodify angel (winnow angel)
-- GHCi infers type of bar as
-- bar :: (Winnow a b, Spodify a c) => a -> c

Also

[ryani.livejournal.com]

The point I was trying to make, if it wasn't clear, was that foo & bar don't need their own typeclasses since they are wholly derived from primitive functions.

And for more fun:
s x y z = x z $ y z
bar = s spodify winnow
typechecks just fine to the correct type, which surprised me!

Re: Also

[pozorvlak.livejournal.com]

Ah, I see. Clever!