[racket-dev] My experience with Typed Racket

On Mon, Nov 5, 2012 at 5:46 PM, Dan Burton <danburton.email at gmail.com> wrote:
> I've published a blog post about Typed Racket that I've been holding on to
> for a while.
> Mainly I intended it as feedback for Sam about what areas of TR I think can
> be improved,
> though it does provide a sort of tour through lots of Typed Racket features,
> so it should be readable by anyone with familiarity with Racket.
>
> http://unknownparallel.wordpress.com/2012/11/05/my-experience-with-typed-racket/

Thanks for the feedback.

I think there are three main areas where you point to things that
frustrated you about Typed Racket.

1. Some features of the structure system aren't supported across
typed/untyped boundaries.

This is certainly true, and we hope to address this in the future.
Racket, and Racket's structure system, is big and complicated, and not
all of it is easy to handle with Typed Racket.  I will say that Typed
Racket was never targeted at R5RS, and it's included struct support
from the beginning.  We called it Typed Scheme back then because the
larger system was called PLT Scheme.

2. The grammar of types isn't user-extensible (and we need better
syntax for optional arguments).

This is a real limitation, and one that others (such as Neil and Eli)
have complained about.  We should just do both of these.

However, it's wrong to say "Typed Racket hijacks macros, and happens
before them".  What happens in your example is that types are not
expressions, and thus the macro expander doesn't apply to them at all.
This is just like how macro expansion doesn't happen in the parameter
lists of functions.  Typed Racket, in particular, happens roughly
after macro expansion (for a full discussion of this, see our PLDI
2011 paper).  Instead, we would add a new way to define type
expanders, similar to `match` expanders or `provide` transformers.

3. Typed Racket often can't tell when a user-written function is a
predicate for a type.

You point to a number of places where this comes up (note that your
`match` example has nothing to do with `match` -- writing the function
out by hand doesn't affect the outcome).  The main cause of this is
that the problem is hard.  Nothing short of sophisticated automatic
theorem prover for a higher-order language (not something that
currently exists) will allow the `valid-xexpr` function to be a
predicate for a rich xexpr type.  You also point out a genuine
weakness in the reasoning system, that it doesn't recognize the
special case when an expression has the *type* `False`, but doesn't
come with a useful filter.  I will look into addressing this.

However, many of the cases where you're having trouble with this are
places where you're probably trying to enforce things with the type
system that TR isn't set up to do.  Xexpressions are good example of
this -- if you want a strongly-typed XML representation in TR, I'd do
it the way you'd do it in haskell, with new structs.  Otherwise, I'd
just take a weak s-expression type, and impose dynamic checks, the way
you'd do in untyped Racket.  The same is true with character subsets
-- you can stick with the `Char` type, or use a constructor to enforce
a particular invariant.

Thanks again for the feedback, and I hope you'll keep using Typed Racket.
--
sam th
samth at ccs.neu.edu