[CakeML-dev] Constructor syntax

Fri May 19 08:30:51 UTC 2017

Hi developers,

My impression is that everyone to some degree wants:

A) Haskell syntax because it is nicer and matches HOL, and
B) SML compatibility for porting / benchmarking purposes.

So far in this discussion there has been an implicit assumption that
we cannot have both A and B at the same time. I just realised that we
can have both and should have both!

For constructors with one or no arguments, Haskell and SML syntax are
the same. So no changes needed.

For constructors with more than one argument, I think we should make
CakeML accept both syntaxes. I'll explain using an exmaple: let's say
Foo is a constructor that takes 3 arguments. I think we should parse
the Haskell syntax as follows:

  Foo x1 x2 x3
  -->
  Con (SOME (Short "Foo"))
    [Var (Short "x1"); Var (Short "x2"); Var (Short "x3")]

and the SML syntax as follows:

  Foo (x1, x2, x3)
  -->
  Con (SOME (Short "Foo"))
    [Con NONE [Var (Short "x1"); Var (Short "x2"); Var (Short "x3")]]

The type system and compiler have semantic information about Foo and
can thus tell if they see Con (SOME (Short "Foo")) applied to only one
argument, then the argument must be a tuple of size 3 since Foo
requires 3 arguments. The compiler can turn the SML-style AST into
Haskell style AST.

This has one drawback: we won't be able to have partially apply
constructors, e.g. `map Some xs` and `map (Foo 1)` won't be
possible (but they are not possible now either). Users who want this
have to define their own helper functions:

  fun some x = Some x
  fun foo x1 x2 x3 = Foo x1 x2 x3

This solution:
 - allows for Haskell syntax,
 - makes the parser's conversion into AST simpler, and
 - allows for compatibility with SML.

Cheers,
Magnus

On 10 May 2017 at 09:21,  <Michael.Norrish at data61.csiro.au> wrote:
> I think this is a fine idea. It makes cmlPtreeConversion simpler for one thing, and that’s got to be a good thing.
>
> Michael
>
> On 10/5/17, 16:28, "Magnus Myreen" <magnus.myreen at gmail.com> wrote:
>
>     > I suppose “I object a bit” because I generally like the SML syntax
>     > for most things, and changing smacks a little of “we couldn’t be
>     > bothered to do the hard yards and so we made the interesting problem
>     > easier to suit ourselves”.  Now, I don’t really believe that,
>     > because syntax is not really an interesting problem, and having to
>     > handle tupled constructors and all the associated cruft is just
>     > masochism.  (The same might be said of giving up on left-to-right
>     > evaluation.)
>
>     True
>
>     > The disadvantage of switching will clearly be that we make it harder
>     > for people to port code.  But how much such porting did we ever
>     > expect?
>
>     I don't think porting is the main driver. However, being able to
>     copy-and-paste CakeML code into Poly/ML or compile it with MLton is
>     useful both for benchmarking against established compilers and
>     understanding errors in the code. Established ML compilers have much
>     better type and parse error reporting.
>
>     This suggests to me that we want to keep compatibility. Currently we
>     have a mostly working treatment of tupled constructors.
>
>     Scott writes:
>
>         The biggest problem is that the constructor application syntax and
>         tuple creation syntax are ambiguous.
>
>     How about solving this in two steps:
>
>      1. Make the AST directly reflect what is written in concrete syntax,
>         i.e. Foo (1,2) would be something like Con "Foo" (Tuple [IntLit 1;
>         IntLit 2]) in the AST regardless of the arity of Foo. Similarly for
>         patterns.
>
>      2. Make the semantics and compiler (both of which know the arity of
>         Foo) treat the tuple as the arguments, if Foo takes 2 arguments.
>
>     Conceptually, I think this change would be sensible because the
>     abstract syntax is then *only* an abstraction of the concrete syntax
>     in this respect. The semantics then interprets the abstract syntax
>     according to the semantic information that it has access to (which is
>     what one has to do when reading SML for Foo (1,2)).
>
>     At present I'm leaning towards keeping SML compatibility because
>     it seems to me that we can easily get around Scott's biggest
>     problem, and we maintain the benefits of SML compatibility
>     mentioned above.
>
>     Cheers,
>     Magnus
>
>
>     On 10 May 2017 at 07:21,  <Michael.Norrish at data61.csiro.au> wrote:
>     > I suppose “I object a bit” because I generally like the SML syntax for most things, and changing smacks a little of “we couldn’t be bothered to do the hard yards and so we made the interesting problem easier to suit ourselves”.  Now, I don’t really believe that, because syntax is not really an interesting problem, and having to handle tupled constructors and all the associated cruft is just masochism.  (The same might be said of giving up on left-to-right evaluation.)
>     >
>     > The disadvantage of switching will clearly be that we make it harder for people to port code.  But how much such porting did we ever expect? On a more trivial note, I also think that having to know a constructor’s arity just to pattern match against it is a little ugly.  In SML you can write
>     >
>     >    C _ => …
>     >
>     > and you know you’ve matched regardless of the arity. Having to remember the arity is a (minor!) burden, both when writing and when maintaining code.  This is why I suggested that “C _” could be a magic form that would match regardless of arity.
>     >
>     > Michael
>     >
>     > On 10/5/17, 07:43, "Scott Owens" <S.A.Owens at kent.ac.uk> wrote:
>     >
>     >
>     >     > On 2017/05/09, at 20:16, Magnus Myreen <magnus.myreen at gmail.com> wrote:
>     >     >
>     >     > On 9 May 2017 at 10:13, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
>     >     >>
>     >     >>> On 2017/05/09, at 01:19, michael.norrish at data61.csiro.au wrote:
>     >     >>>
>     >     >>> I don’t object too strongly to switching to Haskell syntax.
>     >     >
>     >     > So you object a bit?
>     >
>     >     Even though I am advocating the switch, I am a little trepidatious about losing compatibility, since there is almost certainly no going back. So we do need to be sure that we aren’t overlooking any important reasons not to switch.
>     >
>     >     >
>     >     >>> I’m curious as to how you will treat the Foo _ pattern though.  If Foo is really of arity 2, something presumably has to convert the convenient Foo _ syntax to the more accurate Foo _ _. Is this going to happen in the type inferencer?
>     >     >>>
>     >     >>> Or is there a new constructor in the pat type called something like ConstructorPattern, which takes an id and whose semantics is to test for a constructor and not to care about the arguments?
>     >     >>
>     >     >> We don’t support it at the moment. To add it, I think a new pattern AST for Ctor_any would be the cleanest.
>     >     >
>     >     > Why would we allow Foo _ in the curried setting if Foo is of arity 2?
>     >     > I think that should be a type error. I read Scott's original reply as
>     >     > a response in the context of tupled constructors, where Foo _ makes
>     >     > sense.
>     >
>     >     I did mention that originally n terms of tupled constructors. Then I mentioned that we could support it with curried constructors. But maybe we don’t want to.
>     >
>     >     Scott
>     >
>     > _______________________________________________
>     > Developers mailing list
>     > Developers at cakeml.org
>     > https://lists.cakeml.org/listinfo/developers
>
>