[CakeML-dev] Constructor syntax
magnus.myreen at gmail.com
Tue May 9 19:16:51 UTC 2017
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?
>> 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
>> The infix operators that are not constructors should also be made curried (otherwise h::t translates to Cons h t, but x + y translates to +(x,y)).
> They already are curried.
>> Are you (i.e., Scott) going to change gramScript? I can adjust proofs, but can do the grammar too if you don’t want to.
> Go ahead. I don’t think I’ll be able to get to it until next week.
>> On 8/5/17, 23:44, "Scott Owens" <S.A.Owens at kent.ac.uk> wrote:
>>> On 2017/05/08, at 12:53, Magnus Myreen <magnus.myreen at gmail.com> wrote:
>>> I object to Haskell-style syntax.
>> Do you object because there’s something bad about it, or just because of SML compatibility?
>>> I've been all too busy in the last few days to reply and I wanted to
>>> reply properly. I've all along thought that option 2 is best, because
>>> we shouldn't break compatibility with SML.
>> I think this is the point where we either have to decide that SML compatibility is critical and commit to keeping it in the long term, or decide that we can improve the syntax of the language when needed. So it’s not just about the constructors. Essentially, the amount of work to switch to curried constructors is very small, and the amount of work needed to keep tupled ones is much more, so we don’t want to put in the work unless we’re convinced about the usefulness of SML syntax.
>> As I see it, the disadvantages of tupled constructors compared to curried ones are:
>> - They are ugly
>> - CakeML generally encourages currying
>> - They are less flexible because they don’t support partial application
>> - They aren’t like HOL, so when doing a combined translator and cf development, this could lead to confusion
>> - They require some compiler work to implement efficiently
>> The only advantage is that they are how SML does it.
>> What are the advantages of staying with SML? It is a real language, but it (sadly) doesn’t appear to have a vibrant community, especially compared to other functional languages. Furthermore, there aren’t that many SML programs that we will be able to run without changes, since there are still quite a few features that we don’t plan to implement any time soon.
>> The disadvantages are that we can’t improve the syntax later on, for example by adding end to case, or removing it from let (depending on whether you like end or not, but it makes no sense to have it only sometimes). When we get around to implementing records and functors we’d have to use SML’s approach, even though these might not be the best design for our purposes.
>>> We should implicitly define functions for each constructor (at each
>>> Dtype) so that one can write `map SOME xs` and `SOME (1,2)` without
>>> problems, and then rely on an optimisation in BVL to inline the
>>> primitive Con syntax in the right places and get rid of the tupling.
>>> Patterns need to be treated more carefully. I think the syntax should
>>> only take zero or one argument in patterns. However, the type system
>>> and type inference should inspect the shape of the argument to check
>>> that the constructor is given the right number of elements as a tuple
>>> in the argument to the constructor. The relevant part of the compiler
>>> knows enough about arities of constructors to produce the right code
>>> from this cons-applied-to-tuple pattern. I think we should ban
>>> applying a constructor to something too abstract in patterns, e.g. |
>>> Foo x => when Foo is defined as Foo of int * int.
>> It would still be good to be able to write Foo _, but that shouldn’t be too difficult.
>> Developers mailing list
>> Developers at cakeml.org
> Developers mailing list
> Developers at cakeml.org
More information about the Developers