[racket] typed racked questions

On Tue, May 1, 2012 at 11:58 AM, Hendrik Boom <hendrik at topoi.pooq.com> wrote:
> On Mon, Apr 30, 2012 at 08:48:38AM -0400, Sam Tobin-Hochstadt wrote:
>>
>> > 5) Is there a Hindlye/Milner style type inferencing algorithm for typed
>> > racket being worked on?
>>
>> The Typed Racket type system contains a number of features that go
>> beyond what's supported in Hindley/Milner style type systems, and so
>> we can't use that inference system.  Currently, Typed Racket uses
>> local type inference to infer many of the types in your program, but
>> we'd like to infer more of them -- this is an ongoing area of
>> research.  However, inferring all the types in the program, the way
>> that ML and Haskell do, is not a goal of Typed Racket -- having type
>> annotations there makes the program self-documenting and easier to
>> understand, improves type error messages, and supports advanced type
>> system features.
>
> ML and such go too far.  Don't go there.  I really like having
> tatically checked type annotations.  They make life a lot easier.
> It's types I want, not typability,

I agree with this.  The reason that we are looking at more inference
for Typed Racket is two-fold:

1. Currently, Typed Racket requires annoying type annotations that
don't add any useful information, such as:
   (map (lambda: ([x : Integer]) (+ x 4)) (list 1 2 3))
Fortunately, there are systems that solve this, while preserving the
other nice properties Typed Racket has.

2. Macro-generated code from macros that aren't typed (like `for')
often needs more inference than we currently provide, leading TR users
to have to avoid those macros, or us to have to provide alternative
implementations that don't work in all cases.  I hope that improving
inference will alleviate some of this problem.

-- 
sam th
samth at ccs.neu.edu