<div dir="ltr">I don't see how it matters much. So go with the easiest then.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 14 April 2017 at 02:55, Scott Owens <span dir="ltr"><<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">That’s also the hardest option to implement, since it involves changing the structure of the source_to_mod proof. I currently favour adding an empty array allocation primitive because I think it is the easiest option.<br>
<span class="HOEnZb"><font color="#888888"><br>
Scott<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
> On 2017/04/13, at 07:16, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:<br>
><br>
> I prefer making fromList and tabulate primitives. Maybe some day they could then be more efficient primitives than the obvious implementation in source_to_mod. The other two options seem to make empty arrays too special.<br>
><br>
> On 13 April 2017 at 01:44, Scott Owens <<a href="mailto:S.A.Owens@kent.ac.uk">S.A.Owens@kent.ac.uk</a>> wrote:<br>
> At the moment we define Array.fromList and Array.tabulate as follows, which is operationally correct, but the type inferencer gives them types that are too specific: int list -> int array and int -> (int -> int) -> int array.<br>
><br>
>   fun fromList l =<br>
>     let val arr = array (List.length l) 0<br>
>       fun f l i =<br>
>        case l of<br>
>           [] => arr<br>
>         | (h::t) => (update arr i h; f t (i + 1))<br>
>     in f l 0 end<br>
><br>
>  fun tabulate n f =<br>
>     let val arr = array n 0<br>
>       fun u x =<br>
>         if x = n then arr<br>
>         else (update arr x (f x); u (x + 1))<br>
>     in<br>
>       u 0<br>
>     end<br>
><br>
> This is because of the initialisation of the array to 0, before overwriting all of the 0s with the real values. Now I can update the code to initialise the array with one of the values that will go into the array (the head of the list, and f 0, for example). However, this is not possible for fromList [] and tabulate 0, which both produce empty arrays, and the type of the contents are not constrained. I can see several ways to fix this, but none are great.<br>
><br>
> - Make fromList and tabulate be primitives in the source semantics (which could be implemented in source_to_mod rather than a later phase).<br>
> - Add a new array_empty primitive with type unit -> ‘a array<br>
> - Make an attempt to create an empty array raise an exception<br>
><br>
> Any preferences?<br>
><br>
> Scott<br>
> ______________________________<wbr>_________________<br>
> Developers mailing list<br>
> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
><br>
<br>
</div></div></blockquote></div><br></div>