[CakeML] Adding records to CakeML

Francis Southern francis.southern at gmail.com
Thu Apr 21 20:24:02 UTC 2016

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.


P.S.  Thanks to xrchz and YK from the #cakeml IRC channel for the advice
and encouragement that led me to write this email.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20160421/54ee1ff6/attachment.html>

More information about the Users mailing list