On Mon, Nov 5, 2012 at 5:46 PM, Dan Burton <danburton.em...@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 sa...@ccs.neu.edu _________________________ Racket Developers list: http://lists.racket-lang.org/dev