[CakeML-dev] Array library
Ramana.Kumar at cl.cam.ac.uk
Fri Apr 14 05:01:38 UTC 2017
I don't see how it matters much. So go with the easiest then.
On 14 April 2017 at 02:55, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
> 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.
> > On 2017/04/13, at 07:16, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> > 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.
> > On 13 April 2017 at 01:44, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
> > 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
> > fun fromList l =
> > let val arr = array (List.length l) 0
> > fun f l i =
> > case l of
> >  => arr
> > | (h::t) => (update arr i h; f t (i + 1))
> > in f l 0 end
> > fun tabulate n f =
> > let val arr = array n 0
> > fun u x =
> > if x = n then arr
> > else (update arr x (f x); u (x + 1))
> > in
> > u 0
> > end
> > 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.
> > - Make fromList and tabulate be primitives in the source semantics
> (which could be implemented in source_to_mod rather than a later phase).
> > - Add a new array_empty primitive with type unit -> ‘a array
> > - Make an attempt to create an empty array raise an exception
> > Any preferences?
> > Scott
> > _______________________________________________
> > Developers mailing list
> > Developers at cakeml.org
> > https://lists.cakeml.org/listinfo/developers
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Developers