[CakeML-dev] Adding polymorphic compare to CakeML

[Scott Owens]

> On 2016/11/28, at 23:54, Magnus Myreen <magnus.myreen at gmail.com> wrote:
> 
> On 29 November 2016 at 10:29, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
>> So, what would the source semantics do for values that contain refs or closures? I suppose that closures can always return 0, to be compatible with =, but what about references? In OCaml, compare traverses the references, as does =. But our = does a pointer comparison on refs, and we probably want compare to do so as well, but we can’t do < on the pointer since the GC can move them. We could go back to raising exceptions, but then compare can’t use the quick pointer equality check as an optimisation for non-references.
> 
> compare would not follow references. It would return default values
> for references and closures that are compatible with equality, as we
> currently have it. This means that for references that are not the
> same it would have to return a default: either less-than or
> greater-than. This is why I didn't promise a clean semantics for these
> cases!

Ick. So compare wouldn’t be a total order for references. One of the big uses of compare in OCaml is to stick things into balanced binary trees simply and easily. Doing so with this design will silently give wrong results without warning if references are involved.

> An alternative is to have compare have type 'a -> 'a -> bool (instead
> of int) and have it mean that compare the intuition is that it is <=
> for most types. However, for values with non-equal references it
> returns false (i.e. we avoid saying whether it is less-than or
> greater-than).

I don’t think this helps; it’s still not a total order. The int is better since you only need 1 comparison to determine between <, =, >, which you need to implement a binary search tree.

> However, if we add compare then I'd like it to be type compatible with
> OCaml so that one can more easily port OCaml code to CakeML (e.g.
> the sources of HOL light).

Agreed.

Have we checked carefully what types HOL light uses compare on, that there are no refs?

You can actually implement this correctly with the cooperation of the GC, so it might be of to have the confusing semantics at first and fix it later. There are two approaches:

1) The GC never re-orders a ref cell in memory. You could even put all ref cells in their own mark/sweep/compact collected area, exactly how you do this with a generational collection depends on how you’re doing the write barriers to detect when a ref in the old generation is made to point to the nursery.

2) Each ref gets an extra field that is an index used for comparison. This has some cost even when not using compare. Also once you overflow the index, you need to compact the index space. The GC seems like the natural place to do this.

Hybrid strategies are possible, e.g. #2 for the nursery and #1 for the older generation. A nice side effect of doing one of these is that you can also implement hashCode:’a -> int

Scott

> 
> Cheers,
> Magnus
> 
> 
>>> On 2016/11/28, at 23:17, Magnus Myreen <magnus.myreen at gmail.com> wrote:
>>> 
>>> Hi all,
>>> 
>>> I'm currently re-implementing recursive equality in wordLang.
>>> 
>>> It occurred to me that it's easy to add support for something
>>> similar to OCaml's polymorphic compare function. Example:
>>> 
>>>   # compare;;
>>>   - : 'a -> 'a -> int = <fun>
>>>   # compare 0 1;;
>>>   - : int = -1
>>>   # compare 0 2;;
>>>   - : int = -1
>>>   # compare 1 1;;
>>>   - : int = 0
>>>   # compare 2 1;;
>>>   - : int = 1
>>>   # compare 3 1;;
>>>   - : int = 1
>>> 
>>> The CakeML semantics of this primitive would be pretty clean for
>>> values that do not contain closures or references.
>>> 
>>> If no one is against having compare in CakeML, then I'll add it to BVL
>>> and downwards. I would need help in propagating it all the way to the
>>> source semantics.
>>> 
>>> Cheers,
>>> Magnus
>>> 
>>> _______________________________________________
>>> Developers mailing list
>>> Developers at cakeml.org
>>> https://lists.cakeml.org/listinfo/developers
>>