[CakeML] Adding records to CakeML

Sun Jun 12 06:04:56 UTC 2016

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/20160612/bc3b5817/attachment.html>