On 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).
Sorry, this warning wasn't about 'you' I would have warned everyone else in the
same way :-) or perhaps :-( What I wanted to say in short was:
-- "you" can build and extend any given system
-- "you" may end up spending a ton of time on it
-- "you" may discover in the end that it feels wrong, it is wrong, it is
incomplete and must remain so.
As someone who always has his advisor hat on and as someone who has seen other
young people fail -- and hate this kind of failure to the point of rejecting
all future engagement with research-y things -- I had to warn you. Now that you
have been warned, your rights have been read to you, and you made your one
phone call -- go for it. Just don't ever say, you hadn't been warned. Fork is
good.
A lot of what you say below is spot-on. You have picked up and absorbed the
ideas behind Typed Racket, incremental types, and type-system design. But here
is the neat thing about academic research:
we can set a high bar, we can set goals that look nearly unreachable, and
we can strive to get there w/o compromise.
In the process, we will fail, we will learn, we will have fun. We will weep,
cry, scream for disappointment and for joy. But, unlike industrial types or
faux academic types, we don't ever have to say "let's compromise right now for
good because we want to be relevant immediately." We can say that and we can
equally well move toward our unreachable goal.
Society has given us this space. It expects that most of us will fail. It
expects that others learn from our failures. And in return, we have a moral
obligation to search.
Think of Typed Racket in this spirit. Think of the short-cuts and compromises
you encounter as human failings of certain participants in this endeavor. And
think of me as the guy who goes for the big goal and whose job it is to remind
others to go for that.
-- Matthias
> 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/6F50BFBC-45BA-42B5-99FA-3757F85C15A5%40ccs.neu.edu.
For more options, visit https://groups.google.com/d/optout.
