On Thu, Mar 12, 2015 at 11:50 PM, Alexis King <[email protected]> wrote: > 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.
Aw, thanks! > 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). I think this runs together two different issues which it's important to keep separate. First, Typed Racket has a complex and powerful type system because that's what's needed to handle idiomatic Racket code. Furthermore, we're continuing to make it more complicated to handle things like classes, units, and hopefully generics as you propose. To the best of my knowledge, the statically-typed portion of this type system is sound; places where it isn't are simple bugs. This has required a bunch of new research to get right, of course. Second, Typed Racket is embedded in Racket, and must defend itself against against accidental or malicious programs. This includes both simple interaction with untyped code, as well as reflection and other complex features. Unfortunately, this is also easy to get wrong, and we've gotten it wrong plenty of times. There are indeed some holes that continue to exist, and unfortunately closing these holes in the most conservative way would fundamentally break some existing programs, which we'd prefer not to do. However, we're working on this, and I look forward to the day that Typed Racket's soundness is as reliable as plain Racket's memory safety. > 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. I disagree with both of these claims. First, unsoundness is a real problem, and one that people stumble upon even when they aren't trying. We need only to look at the long history of C vulnerabilities to see this. Second, Typed Racket isn't sacrificing soundness for practicality. Sometimes, we have bugs, and we have not fixed them all. We're also not always willing to fix a bug if we don't have a fix that works well for existing users -- if they've relied on something working, we shouldn't make their whole program break permanently. > 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. I think maintaining untyped idioms doesn't require compromises -- except on amount work and research we need to do. I encourage you to start in on that work, and I'm happy to help. But an important part of that is maintaining the philsophy of Typed Racket, including soundness and faithfulness to existing Racket programs. > 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. This is not, I think, correct about subtyping. For example, Scala does static determination of implicits, despite the presence of subtyping. But if you mean that Typed Racket's generics won't be the same as Haskell's, since Racket's generics aren't either, then yes, that's correct. But you can still do many impressive things with them -- for example, Tony's monad implementation here: http://www.eighty-twenty.org/2015/01/25/monads-in-dynamically-typed-languages/ > 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. Again, I don't think this is true, and it's confusing the two issues that I distinguished earlier. If we don't yet know how to generate contracts for generic function types, we can simply not implement that, but that doesn't require soundness holes. > 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. As Matthias said, research can always fail. If you make an effort in one direction and show that it doesn't work, or that more is required to make it work, that would be highly valuable. But I don't think that approaching this as "forking TR" is a good idea. TR has managed to successfully handle a wide variety of tricky Racket features, and I'm sure we can do generics too. A separate issue, which you mention in passing, is whether Typed Racket is the be-all and end-all of types in the Racket ecosystem. Currently it's the most popular, but I think there's room for other systems as well. If you, or anyone else, want to develop a Haskell-like or ML-like or Scala-like system in Racket, that sounds like a great idea to me. You wouldn't be constrainted by existing Racket programs, and who knows what interesting things would develop. Sam -- 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/CAK%3DHD%2BaEh%2BnwY29uWDkZqFcDCRYcQgpM6YFeejro4MgUKsEnmQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
