[CakeML-dev] Adding polymorphic compare to CakeML

Magnus Myreen magnus.myreen at gmail.com
Mon Nov 28 23:54:47 UTC 2016


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!

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).

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).

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
>



More information about the Developers mailing list