[CakeML] Adding records to CakeML

Mon Jun 13 19:56:49 UTC 2016

Hi Ramana,

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 <
http://www.cis.upenn.edu/~bcpierce/sf/current/index.html> 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.

On top of this, I also started a new job a few weeks ago, so that's
significantly reduced my free time!

Cheers,
Francis

On 12 June 2016 at 07:04, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:

> Hi Francis,
>
> I just wanted to check in on how you're going. Did the prospect of working
> on compiler optimisations seem appealing?
> Is there something I could do to help with understanding the semantics or
> type system?
>
> Cheers,
> Ramana
>
> On 25 April 2016 at 23:54, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
>
>> Francis,
>>
>> 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.
>>
>> 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.
>>
>> Scott
>>
>> > On 2016/04/22, at 21:37, Francis Southern <francis.southern at gmail.com>
>> wrote:
>> >
>> > Hi both,
>> >
>> > Thank you for your replies.
>> >
>> > 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 <
>> http://www.cl.cam.ac.uk/~mom22/fp/lec9-types.pdf> (although I found some
>> of the other lectures were a bit beyond my current knowledge in parts).
>> >
>> > 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.
>> >
>> > 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.
>> >
>> > I hope that answers your questions,
>> > Francis
>> >
>> >
>> > On 22 April 2016 at 14:38, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
>> > 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.
>> >
>> > Scott
>> >
>> > > On 2016/04/22, at 06:55, Magnus Myreen <magnus.myreen at gmail.com>
>> wrote:
>> > >
>> > > Hi Francis,
>> > >
>> > > I'm very happy to hear that you are interested in contributing to
>> > > CakeML. For records and type annotations, Yong Kiam, Scott and Ramana
>> > > are the right people to consult. They should all be on this mailing
>> list.
>> > >
>> > > I can imagine that records might be a difficult one to start with,
>> > > while type annotations are probably a more gentle introduction.
>> > >
>> > > There are also some obvious optimisations missing in the compiler. Let
>> > > me know if you are interested in implementing and verifying compiler
>> > > optimisations. Some of the optimisations should be well contained
>> > > within specific intermediate languages.
>> > >
>> > > Cheers,
>> > > Magnus
>> > >
>> > >
>> > >
>> > >
>> > >
>> > > On 21 April 2016 at 22:24, Francis Southern <
>> francis.southern at gmail.com> wrote:
>> > >> Dear CakeML developers,
>> > >>
>> > >> I want to start by saying that I find your work on CakeML
>> fascinating and
>> > >> I'm eager to find ways to begin contributing, so I'm looking for a
>> small
>> > >> project to get my feet wet with (since I haven't got that much
>> experience
>> > >> with formal development or programming language implementation).  Of
>> course
>> > >> I've seen the list at <https://cakeml.org/projects.html> and I am
>> hopeful I
>> > >> can start working on one of these projects (possibly related to
>> pattern
>> > >> matching) in the near future, but I'm trying to find something
>> smaller that
>> > >> I can make progress on more quickly.  Since I'm working
>> independently at the
>> > >> moment, I suppose I want to get feedback and that buzz of
>> contribution as
>> > >> soon as possible!
>> > >>
>> > >> So, whilst poking around in the code looking for interesting leads,
>> I came
>> > >> across a list of unimplemented features including records and type
>> > >> annotations in the file documentation/reference.tex.  These seem to
>> me like
>> > >> self-evidently desirable features which are hopefully reasonably
>> simple to
>> > >> implement.  I don't mean to suggest they'll be easy, but they're the
>> easiest
>> > >> meaningful contributions I've been able to identify!
>> > >>
>> > >> Adding records seemed the more interesting of the two, so I started
>> thinking
>> > >> about it and discussed it a little in the IRC channel.  First off,
>> since I
>> > >> understand CakeML has diverged from Standard ML in other areas,
>> there are
>> > >> choices to be made about the semantics we want (basically, along the
>> lines
>> > >> of SML vs OCaml).  Do we want them to be declared or anonymous?  Do
>> we want
>> > >> unique field names?  Do we want to support field reordering?  Mutable
>> > >> fields?  Subtyping?!  There are probably other possibilities I've
>> either
>> > >> forgotten about or am ignorant of.  The answers to some of these
>> questions
>> > >> also have implications for pattern matching and type inference, of
>> course.
>> > >>
>> > >> And then there's the implementation.  I think the main decision here
>> is
>> > >> whether we implement records on top of tuples or vice versa.  The
>> > >> implementation will obviously require changes to several parts of the
>> > >> codebase (the type system and inference, the parser, the compiler,
>> etc).
>> > >> This is, of course, the purpose of the whole exercise, but still
>> rather
>> > >> intimidating to me, so any advice on how to approach this (which
>> files would
>> > >> need to be worked on, which could be enlightening to study, etc)
>> would be
>> > >> much appreciated.
>> > >>
>> > >> In fact, after thinking about all that, I'm wondering if it's
>> actually a
>> > >> better idea to start with type annotations instead!  But anyway, I'm
>> looking
>> > >> forward to hearing your opinions.  I hope that I don't come across
>> as too
>> > >> clueless, and naïve only in the optimistic sense.
>> > >>
>> > >> Cheers,
>> > >> Francis
>> > >>
>> > >> P.S.  Thanks to xrchz and YK from the #cakeml IRC channel for the
>> advice and
>> > >> encouragement that led me to write this email.
>> > >>
>> > >> _______________________________________________
>> > >> Users mailing list
>> > >> Users at cakeml.org
>> > >> https://lists.cakeml.org/listinfo/users
>> > >>
>> > >
>> > > _______________________________________________
>> > > Users mailing list
>> > > Users at cakeml.org
>> > > https://lists.cakeml.org/listinfo/users
>> >
>> >
>>
>> _______________________________________________
>> Users mailing list
>> Users at cakeml.org
>> https://lists.cakeml.org/listinfo/users
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20160613/a639ff10/attachment.html>