<div dir="ltr"><div><div>Hi Ramana,<br><br></div>Thanks for the email and I apologise for my previous silence.  I suppose the short answer is that I got cold feet!  It's not that compiler optimisations were unappealing, and I definitely appreciate the advice about better places to start, but I was worried that I didn't have the requisite knowledge.  I think I should probably read a serious book on compilers (Has anyone got any recommendations? I'm thinking about Appel's `Modern Compiler Implementation in ML'.), but what I've been doing in the meantime is the `Software Foundations' course <<a href="http://www.cis.upenn.edu/~bcpierce/sf/current/index.html">http://www.cis.upenn.edu/~bcpierce/sf/current/index.html</a>> as I thought it could develop my mechanised proof skills, whilst simultaneously reinforcing PL/type theory fundamentals.  So, I'm still interested and still around, but I'm sort of biding my time and trying to get myself into a better position to be able to contribute.  Perhaps I was a little too eager to jump in when l wasn't ready.<br></div><div><br></div><div>On top of this, I also started a new job a few weeks ago, so that's significantly reduced my free time!<br><br></div><div>Cheers,<br></div><div>Francis<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 12 June 2016 at 07:04, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div>Hi Francis,<br><br></div>I just wanted to check in on how you're going. Did the prospect of working on compiler optimisations seem appealing?<br></div>Is there something I could do to help with understanding the semantics or type system?<br><br></div>Cheers,<br></div>Ramana<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 25 April 2016 at 23:54, Scott Owens <span dir="ltr"><<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Francis,<br>
<br>
I think Magnus suggestion of getting started by working on optimisations is a good fit for your background. Additions to the type system are not localised in one place, many of them would require changing the parse implementation, context-free grammar, type inferencer, declarative type system, and all of their various proofs of correctness. This means that it’s almost impossible to get quickly started by doing something that feels rewarding and productive on the front-end of the system.<br>
<br>
In a sense, all of the work that we’ve been doing on the new back end with 12 intermediate languages is to make sure that people (ourselves included) can try out optimisations and verify them with a relatively localised understanding of the system.<br>
<span><font color="#888888"><br>
Scott<br>
</font></span><div><div><br>
> On 2016/04/22, at 21:37, Francis Southern <<a href="mailto:francis.southern@gmail.com" target="_blank">francis.southern@gmail.com</a>> wrote:<br>
><br>
> Hi both,<br>
><br>
> Thank you for your replies.<br>
><br>
> Regarding my knowledge in PL theory and type systems, it's a difficult question to answer, because I don't want to under- or overstate my knowledge.  I first encountered type theory a couple of years ago when I was at university studying mathematical logic, where I attended a reading group discussing the simply typed lambda calculus, the Curry-Howard correspondence and related topics (using the lecture notes by Sørensen and Urzyczyn, if you know them).  Around the same time I began learning OCaml, which got me interested in more applied aspects of the subject as well (in fact, I first came across CakeML via Owens' paper on the semantics of OCaml light).  Recently I've been reading Pierce's `Types and Programming Languages' to build a more solid foundation for my knowledge, and I'm comfortable with exposition at this level.  In short, I know I'm coming at this as somewhat of an amateur, but I'm not a complete outsider.  For example, I am able to easily follow the slides at <<a href="http://www.cl.cam.ac.uk/~mom22/fp/lec9-types.pdf" rel="noreferrer" target="_blank">http://www.cl.cam.ac.uk/~mom22/fp/lec9-types.pdf</a>> (although I found some of the other lectures were a bit beyond my current knowledge in parts).<br>
><br>
> As for mechanised proof, I don't have much practical experience at all.  I did some tutorials with Coq a couple of years ago, and have done the same with HOL4 in the last week in preparation for working on CakeML.  I know this is the main skill I need to develop in order to contribute to CakeML, and it's one of the primary motivators of my interest in the project too!  I'm more than happy to be told to come back after reading/doing X, Y or Z, if you think I need more background here.<br>
><br>
> I am also interested in implementing and verifying compiler optimisations, because, to be honest, I'm excited by the thought of CakeML being a viable choice for industrial software development, but I'm even less knowledgeable about compiler optimisations than type systems and I don't want to keep biting while I'm still chewing.<br>
><br>
> I hope that answers your questions,<br>
> Francis<br>
><br>
><br>
> On 22 April 2016 at 14:38, Scott Owens <<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>> wrote:<br>
> There are several possible ways to approach extending the CakeML type system, and several different directions that extensions could go in. I’d be happy to outline some possible projects, but would like to get a sense of your expertise in PL theory and type systems and/or mechanised proof. There are projects suitable for a variety of interests and expertise, but it might be helpful to know before suggesting a concrete approach.<br>
><br>
> Scott<br>
><br>
> > On 2016/04/22, at 06:55, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>> wrote:<br>
> ><br>
> > Hi Francis,<br>
> ><br>
> > I'm very happy to hear that you are interested in contributing to<br>
> > CakeML. For records and type annotations, Yong Kiam, Scott and Ramana<br>
> > are the right people to consult. They should all be on this mailing list.<br>
> ><br>
> > I can imagine that records might be a difficult one to start with,<br>
> > while type annotations are probably a more gentle introduction.<br>
> ><br>
> > There are also some obvious optimisations missing in the compiler. Let<br>
> > me know if you are interested in implementing and verifying compiler<br>
> > optimisations. Some of the optimisations should be well contained<br>
> > within specific intermediate languages.<br>
> ><br>
> > Cheers,<br>
> > Magnus<br>
> ><br>
> ><br>
> ><br>
> ><br>
> ><br>
> > On 21 April 2016 at 22:24, Francis Southern <<a href="mailto:francis.southern@gmail.com" target="_blank">francis.southern@gmail.com</a>> wrote:<br>
> >> Dear CakeML developers,<br>
> >><br>
> >> I want to start by saying that I find your work on CakeML fascinating and<br>
> >> I'm eager to find ways to begin contributing, so I'm looking for a small<br>
> >> project to get my feet wet with (since I haven't got that much experience<br>
> >> with formal development or programming language implementation).  Of course<br>
> >> I've seen the list at <<a href="https://cakeml.org/projects.html" rel="noreferrer" target="_blank">https://cakeml.org/projects.html</a>> and I am hopeful I<br>
> >> can start working on one of these projects (possibly related to pattern<br>
> >> matching) in the near future, but I'm trying to find something smaller that<br>
> >> I can make progress on more quickly.  Since I'm working independently at the<br>
> >> moment, I suppose I want to get feedback and that buzz of contribution as<br>
> >> soon as possible!<br>
> >><br>
> >> So, whilst poking around in the code looking for interesting leads, I came<br>
> >> across a list of unimplemented features including records and type<br>
> >> annotations in the file documentation/reference.tex.  These seem to me like<br>
> >> self-evidently desirable features which are hopefully reasonably simple to<br>
> >> implement.  I don't mean to suggest they'll be easy, but they're the easiest<br>
> >> meaningful contributions I've been able to identify!<br>
> >><br>
> >> Adding records seemed the more interesting of the two, so I started thinking<br>
> >> about it and discussed it a little in the IRC channel.  First off, since I<br>
> >> understand CakeML has diverged from Standard ML in other areas, there are<br>
> >> choices to be made about the semantics we want (basically, along the lines<br>
> >> of SML vs OCaml).  Do we want them to be declared or anonymous?  Do we want<br>
> >> unique field names?  Do we want to support field reordering?  Mutable<br>
> >> fields?  Subtyping?!  There are probably other possibilities I've either<br>
> >> forgotten about or am ignorant of.  The answers to some of these questions<br>
> >> also have implications for pattern matching and type inference, of course.<br>
> >><br>
> >> And then there's the implementation.  I think the main decision here is<br>
> >> whether we implement records on top of tuples or vice versa.  The<br>
> >> implementation will obviously require changes to several parts of the<br>
> >> codebase (the type system and inference, the parser, the compiler, etc).<br>
> >> This is, of course, the purpose of the whole exercise, but still rather<br>
> >> intimidating to me, so any advice on how to approach this (which files would<br>
> >> need to be worked on, which could be enlightening to study, etc) would be<br>
> >> much appreciated.<br>
> >><br>
> >> In fact, after thinking about all that, I'm wondering if it's actually a<br>
> >> better idea to start with type annotations instead!  But anyway, I'm looking<br>
> >> forward to hearing your opinions.  I hope that I don't come across as too<br>
> >> clueless, and naïve only in the optimistic sense.<br>
> >><br>
> >> Cheers,<br>
> >> Francis<br>
> >><br>
> >> P.S.  Thanks to xrchz and YK from the #cakeml IRC channel for the advice and<br>
> >> encouragement that led me to write this email.<br>
> >><br>
> >> _______________________________________________<br>
> >> Users mailing list<br>
> >> <a href="mailto:Users@cakeml.org" target="_blank">Users@cakeml.org</a><br>
> >> <a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
> >><br>
> ><br>
> > _______________________________________________<br>
> > Users mailing list<br>
> > <a href="mailto:Users@cakeml.org" target="_blank">Users@cakeml.org</a><br>
> > <a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
><br>
><br>
<br>
_______________________________________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org" target="_blank">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>