Thank you for your warnings. I certainly didn’t anticipate it to be straightforward, but yes, it’s also probable I’m not up to the task. I definitely haven’t tried very much just yet, and I’m still undecided if I want to pursue this at all (at least for the time being).
I do want to take a moment to discuss something that I was talking with Eric (and briefly with Andrew) about on IRC a short while ago because it’s something that I think puts Typed Racket in an interesting position. I encountered Typed Racket as an end user—someone who was just interested in using it for ordinary programming—and I came upon it at a time in which it’s honestly a very practical drop-in replacement for a large portion of Racket. Especially with the newly added support for the class system, it’s remarkably capable language, and I find it to be a superior experience to using untyped Racket in most ways. Of course, what’s curious about Typed Racket is its approach to taking an existing untyped language and adding static typing to it without altering any idioms whatsoever of the underlying language. This is an admirable research project as well as a highly practical goal since it means converting to Typed Racket is extremely straightforward. I’ve found occurrence typing absolutely stunning at times in the pure spectrum of situations it can accurately type. (Especially with the new DrRacket tooltips that I think Asumu added, which show how occurrence typing propagates, and it’s awesome.) The downside, of course, is that TR’s abstraction is leaky at times—I have wrangled with the type system more than I would have liked, and especially when typed code interacts with untyped code, it can be rough around the edges. Despite this, there are still soundness holes in weird edge cases because, well, enforcing types everywhere with the level of fined-grained control that TR’s type system provides is really hard (especially when things can be mutable). So on the one hand, I totally understand Typed Racket as a research project, and it’s a fascinating and highly successful one at that. I am deeply grateful for all the work and ingenuity that has been poured into it. On the other hand, I also view TR has a practical tool I want to use in programming, and sometimes it’s very easy to run into its shortcomings when pushing it to its limits in real-world code. In some cases, Typed Racket has already sacrificed soundness for practicality (whether originally intentional or not), but honestly I don’t think that’s much of a problem since people will never stumble upon it unless they are explicitly trying to break the type system. Anyway, I guess what I’m really saying is that I feel like maintaining all untyped Racket idioms and being able to interact with untyped code makes it almost impossible to maintain perfect soundness everywhere. So whatever, that’s my opinion. (I’d be possibly interested in writing a different, non-Racket-like typed language on top of Racket, but that is an entirely different conversation for another time.) What does any of this have to do with generics? Some of it doesn’t, it was really just me wanting to have a tangentially-related discussion. That said, I’d also argue the following: Typed Racket’s implementation of generics is already going to be highly restricted based on Racket’s implementation of generics since all dispatch has to be purely dynamic. It couldn’t use static dispatch, anyway, due to subtyping. Building upon that, I’m not sure it’s even possible to design an adequate generics system with no soundness problems given Racket’s capability for struct subtyping. (It probably could be possible by introducing some additional contract mechanisms, possibly to the core, but that’s far out of my scope.) As far as I can tell, a large number of the current issues with soundness already revolve around struct subtyping—Eric is obviously much more aware of that than I am, though. Fundamentally, given the constraints placed on the system, it doesn’t feel like there are all that many possibilities for introducing Racket’s generics to TR. Since it’s something I’d find incredibly helpful in real code, my first instinct is to just bolt it on. Obviously, “just bolt it on” isn’t satisfactory for something of this significance, but even if I tried it and subsequently failed horribly and ended up with a half-functional mess that could be easily broken, I’m still tempted to try anyway because I think even a broken implementation would have real utility, and it could help to serve as an illustration for what doesn’t work and how it could be fixed. Basically, I’m considering forking TR and adding a hacky generics implementation without much thought so people can break it. Feel free to try to talk me out of it (I haven’t even decided if I want to try yet or not), but I think that’s currently my frame of mind. Alexis > On Mar 12, 2015, at 13:20, Matthias Felleisen <[email protected]> wrote: > > > On Mar 9, 2015, at 12:13 PM, Vincent St-Amour <[email protected]> wrote: > >> I'd say: go for it! :) >> >> I recommend you design the type system aspects first, then work on the >> implementation. It's easier to iterate on the design that way, and >> conceptual bugs should be apparent earlier in the process. >> >> I won't lie, this is probably not going to be easy work, but it would >> definitely be a good addition to TR, not to mention a major learning >> experience for you. :) >> >> If you need pointers/advice, feel free to ask Sam/Asumu/Eric/Andrew/myself. >> From that group, Sam and Asumu are probably the ones most familiar with >> the relevant type systems literature, and can probably point you to >> papers with potential starting points. > > > Alexis, I am usually all in favor of encouraging contributions. The > more, the merrier. But this time around, I'd like to spell out what > such a project implies realistically before you go on an incredibly > difficult expedition. > > 1. I consider this project research, not just advanced development. > > 2. I tell all my PhD students > > Research is when it can fail. > > A failure might be a serious investment here. > > 3. Typed Racket has a design plan and philosophy. I think you're > basically familiar with the ideas -- your email touches on many > of these. > > Here is how we proceeded with adding types to classes, and I think > our experience shows that this is a good routine: > > -- collect examples of uses [hard, because as Vincent says, > generics are new] > -- explore literature [the very original papers on Haskell's > generics might be a good fit here; I am having Ben G. > read up on this because many are interested in this] > -- pick a few examples from step 1 as 'formative tests' > > -- design syntax of types, meaning > -- design type system and make sure your examples go through > [a Redex model worked really well, easy prototyping > and can run existing Racket examples usually] > -- repeat these steps until stable > > -- argue that the type system is sound (all of its predictions > are true) > > -- design type to contract compiler > -- argue the combination is sound > -- repeat these steps until stable > > == You may have to backtrack all the way up to syntax/meaning > to fix problems here > > -- evaluate expressiveness > -- evaluate performance > > == You may have to backtrack again all the way up to syntax/meaning > to fix problems here > > Some of these steps call for novel ways of doing things. > Some just call for doing old things right. I am sure you > can call on help for some of the implementation and/or > work-intensive parts. But if people didn't follow along > with your development, they need ways to find out what > your design decisions are. > > You will need to keep writing little essays on these steps > so that people can join you. > > We have been through this twice now for significant projects (classes, > units). We have done it smaller things. If I considered generics small, > I wouldn't write this message. > > Adding type isn't just an implementation project. If you're still > up for it, make a plan, Add it to your project pages. Develop a > work routine. Develop a writing routine. Ask for help. A lot. Be > prepared to spend a serious amount of time. > > -- Matthias > > > > -- You received this message because you are subscribed to the Google Groups "Racket Developers" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-dev/058D9870-1F58-436C-A94D-8C25CE2AC0EC%40gmail.com. For more options, visit https://groups.google.com/d/optout.
