Stdlib array extension #1195
Stdlib array extension #1195
Conversation
stdlib/array.ncl
Outdated
| if array == [] then | ||
| array | ||
| else | ||
| let first = %elem_at% array 0 in | ||
| let rest = %array_slice% 1 (%length% array) array in | ||
| fold_left f first rest, |
There was a problem hiding this comment.
I don't think returning an empty array when given one makes sense here (How does this even typecheck?). It would probably be best to somehow fail on an empty array; maybe by applying the array.NonEmpty contract somewhere?
There was a problem hiding this comment.
It doesn't make any sense, I think I thought about returning None and may brain then failed. We should fail on this, probably.
The issue I had with more specific contracts like NonEmpty is that they make those standard functions a pain to use in statically typed code. On one hand it's a shame, because we have those nice contracts with argument tracking and whatnot which could provide really good error messages. On the other hand, making folds, reduce and map a pain to use in typed code is also kind of a show stopper. One solution could be to separate them in submodules (having a more loosely typed version, and a tight contract-protected version), but that isn't satisfying either.
Maybe one solution at some point would be the ideas exposed in #420.
There was a problem hiding this comment.
You could delegate the contract check explicitly to the runtime, by doing something like
reduce_left : forall a. (a -> a -> a) -> Array a -> Array a
= fun f array' =>
let array = array' | NonEmpty in
...
I wouldn't be great for error reporting, because the blame label would point into the standard library. But it would be usable in statically checked code now.
There was a problem hiding this comment.
Would that work? Now array has type NonEmpty, and you can't do anything with it in typed code anymore, I fear.
There was a problem hiding this comment.
Or maybe something like %seq% (array | NonEmpty) ...restofthefunction... but this starts to be really convoluted 😅
There was a problem hiding this comment.
Maybe this calls for a construct to check a contract without influencing typechecking
There was a problem hiding this comment.
How does this even typecheck?
Well, it doesn't, that's why the tests are failing 🙃
There was a problem hiding this comment.
Oh, we could use a type annotation for the static type we want + an additional contract annotation, for more checks. Those won't influence static typechecking (which picks the first annotation it find as the apparent type). On one side it sounds slightly like a hack, but on the other, it's not too bad
There was a problem hiding this comment.
So, we'd write
reduce_left
: forall a. (a -> a -> a) -> Array a -> a
| forall a. (a -> a -> a) -> NonEmpty -> a
= ...
I guess? That's a little bit of duplication, but I think it's a price worth paying here 👍
There was a problem hiding this comment.
We can also just add the "differential" contract, so to speak:
reduce_left
: forall a. (a -> a -> a) -> Array a -> a
| Dyn -> NonEmpty -> Dyn
That might make for a slightly worse error message, though. We could also duplicate the type fully as you propose, and rely on contract elision (yet to be added) to not do too much work.
Adds a batch of functions to the array stdlib module.
Add a `array_slice` primitive operation, which takes a slice of an array in constant time.
Co-authored-by: Viktor Kleen <viktor.kleen@tweag.io>
Co-authored-by: Viktor Kleen <viktor.kleen@tweag.io>
Co-authored-by: Viktor Kleen <viktor.kleen@tweag.io>
yannham
force-pushed
the
feature/stdlib-array-extension
branch
from
82db787
to
6592fd2
Compare
Following #935, add a batch of missing functions to the array stdlib. This PR adds a
sliceprimitive operation as well, required to implement the corresponding function of the stdlib. This PR adds a newenumstdlib module as well, moving a few functions/contracts from thestringmodule.Doing so, we also expanded the documentation of folds, by adding a more informal description as well as a paragraph on
fold_rightvsfold_left. This is useful as a reference for the documentation ofreduce_rightandreduce_lefttoo.Follow-up
We can now get rid of the
%tail%primop, which is subsumed by%slice% 1 (%length% <.>). In the same spirit, we should probably get rid of%head%in favor of%elem_at% 0. This is planned in a follow-up PR.