Home

Eliminating Array Bound Checking through Non-dependent types

Oleg posted this pertinent message on the Haskell mailing list. It's always nice to see cool examples such as this.

Having saiod that, I must also say that I agree with Conor McBride who wrote that anyone who would argue (and I'm not saying you do) that work to try to make more advanced type systems and stronger static guarantees more convenient and well-supported is not necessary because it happens to be possible to bang out this or that example in Haskell as it stands if you think about it hard enough, is adopting the position of the ostrich.

Making type systems more expressive is a worthy goal. You want them to remain decidable (i.e., static), of course. Can we at least agree on that? ;-)

By Ehud Lamm at 2004-08-06 10:50 | Type Theory | other blogs | 9476 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

There is plenty of room within decidable kingdom

As mentioned earlier1, there are type systems that combine dependent types with nice meta-theoretical properties (including decidability - there is a simple terminating algorithm for type inference - see Section 6.2.2).

These type systems require more input from the programmer, but as Conor McBride said, one can see this as an asset, not a liability, and one can capitalize on that. Dependent types interplay in wonderful ways with interactive programming, establishing a closer dialog between type elaborator/interpreter/compiler and programmer.



Side-note: I wonder, why Conor is using Haskell, and not Prolog or Oz - one could implement a core of Epigram in about hundred Prolog lines :-)
These languages support logical programming directly, after all.


1This thesis was published in 1990, and certainly there are many more written during these years.

By Andris Birkmanis at Fri, 2004-08-06 14:23 | login or register to post comments

The Cult of Conor

I wonder, why Conor is using Haskell, and not Prolog or Oz - one could implement a core of Epigram in about hundred Prolog lines :-) These languages support logical programming directly, after all.

I could argue in support of Haskell for such tasks, but instead—why don't you ask him? I would love to see his answer.

By Frank Atanassow at Fri, 2004-08-06 15:18 | login or register to post comments

You're kidding?!

The Cult of Conor

If you point me to other practitioner who focuses on both dependent types and interactive programming, I will quote him as well.

Nobody gets irritated hearing names of Milner, Moggi, Wadler, or Atanassow, for that matter. Why should anyone object to a new name?

I agree that I might have gone overboard a bit. That may be a consequence of tedious type wars.

I could argue in support of Haskell for such tasks, but instead—why don't you ask him? I would love to see his answer.

I would prefer him to talk to LtU, as this is more productive than private mails. Now, though, it seems that I managed to alienate the whole audience, so I am in doubt...

By Andris Birkmanis at Fri, 2004-08-06 15:45 | login or register to post comments

Nonsense

I'm sure there are many here who'd be interested to hear what Conor has to say. Frank included, I imagine.

By Bryn Keller at Fri, 2004-08-06 15:58 | login or register to post comments

No, I'm serious!

You completely misunderstood my comment.

I love reading Conor's posts and presentations; I'm not a dependent types fan, but I think he's very witty and insightful. So I would look forward to seeing his response.

When I speak of "the Cult of Conor", I am referring to myself! :)

Nobody gets irritated hearing names of Milner, Moggi, Wadler, or Atanassow, for that matter.

I'm just a lowly grad student with a big mouth; you do me too much honor to place me in such august company...

By Frank Atanassow at Fri, 2004-08-06 16:00 | login or register to post comments

Great!

I'm just a lowly grad student with a big mouth; you do me too much honor to place me in such august company...

Why do you think I was refering to you? :-)

You completely misunderstood my comment.

My apologies, I am too jumpy today.

So I would look forward to seeing his response.

Great, anyone having closer contact than just reading presentations? He might accept an email from a complete stranger, though :-)

By Andris Birkmanis at Fri, 2004-08-06 16:04 | login or register to post comments

It would be an honor

If anyone feel like contacting him, please cc me. I'd love to have him post here.

By Ehud Lamm at Fri, 2004-08-06 17:51 | login or register to post comments

It may be worth to use Haskell, after all :)

Well, I gave it a try, and though the size of core type checker is indeed under 100 Prolog LOCs, I can now see the limitations of my approach to the problem. I tried to encode inference rules from the paper mechanically as Prolog rules, trying to stay very close to the original (without even using cuts).

One (minor) problem was implementing a substitution for terms. Unfortunately, Prolog implementation I use (a toy, actually) does not have metaprogramming capabilities (no reflection), so I had to do case analysis on all "constructors".

Another problem was with reporting of errors. If I make type() or eval() to fail when they cannot produce result, then they do not bind any parameters, including error messages. If I make them to always succeed, I have to implement all the backtracking by hands. And striving for purity I refrained from dynamically updating Prolog DB by error messages :) Well into the third hour of hacking I understood I need some monad :)

I am currently considering to use some embedded Prolog implementation to do the logic(al) part of job, while doing the dirty bookkeeping in (tada!) Java.

Disclaimer: this experiment does not diminish the value of Prolog, as I was using a very limited subset of the language. Also, my Prolog skills are even more limited, as last time I used it some 8 years ago, and even then just for passing a test in school.

PS: I hate to mention it, but lack of static type checking didn't help either.

By Andris Birkmanis at Tue, 2004-08-10 13:13 | login or register to post comments

"Cult of Conor"?

"I am Conor McBride of the clan McBride..."

Sorry...

By Matt Hellige at Fri, 2004-08-06 15:29 | login or register to post comments

*Ouch*

You should be. :-)

By Paul Snively at Fri, 2004-08-06 19:45 | login or register to post comments

In the end...

"There can be only one... type system!"

Double sorry...

By Anton van Straaten at Sat, 2004-08-07 00:31 | login or register to post comments

Scientist Mode

Somewhat but not entirely off-topic is the fact that array indexing can need more than a simple bounds check, useful as that is.

David McClain (of optimized Numerical ML fame, an OCaml variant) is being poetic with the torus metaphor. The point is that any numerical processing on arrays runs into edge (boundary) issues. These are handled according to various schemes like zero-padding and mirroring, via indexing tricks. It is surprising how often non-unity stride factors are needed, too.

This index trickery may be considered the more general case of bounds checking. The implication is simple. A person might want to allow out-of-bounds indexing that does something other than throw an exception. Please keep David's Scientist Mode in mind when you think about arrays. Scientists are the power users.

By Mark Evans at Fri, 2004-08-06 20:06 | login or register to post comments