To describe Pyret, its primary purpose is to be a teaching language, and I think its most remarkable feature on a technical basis seems to be the way it does type annotations and unit tests. I think these are just run time contracts for now, but they'll somehow pave the way for a static type system, limited by a policy that there must always be a way to understand the static type system in terms of run time behavior (https://news.ycombinator.com/item?id=6704276).

I don't see very much value (but I do see some) in a static type system if all it does is promote some run time errors to compile time. Module API enforcement and program inference are what I mainly care about as far as static types go, and Pyret doesn't seem to provide either of these. (Contracts don't quite reassure me that a client module will continue to obey the API throughout the lifetime of a multi-step interaction like a handshake or a higher-order loop. A contract violation error can occur partway through.)

If they ever weaken their policy about the type system mimicking run time checks, I think Pyret could support some special types and tests which require compile time processing if they're used. At the same time, it could still use all its expressive run time contracts. I'd really like to see this synthesis, but I don't really expect to; the implementors probably have enough to worry about just to build a static typechecker at all. :)