Closed yannham closed 21 hours ago
:tada: All dependencies have been resolved !
:tada: All dependencies have been resolved !
I didn't quite understand the part about needing an extra return variant for the immediate part. If we could destructure contracts back into immediate and delayed, couldn't we write Nullable like this?
let Nullable = fun Contract => std.contract.custom (fun value => if value == null then 'Ok else (%contract/immediate% Contract) value ) (%contract/delayed% Contract)
I believe, in this case, that the delayed part of Contract
will be applied in all situations. This is not what you want if value == null
(for Nullable {foo | Number}
, it doesn't make sense to try to map Number
somewhere in a null
value). I think we need to let the immediate part decide if it should short circuit and stops now, or proceed with the delayed part. The delayed part might assume that the immediate part must have run and thus doesn't need to be defensive; for {foo | Number}
, it would assume without checks that what it gets is a record.
Oh, wait, were you talking about the 'Apply
thingy?
Yes, exactly. (I was also initially confused about 'Ok
vs 'Proceed
, but reading the changes sorted that part out for me)
Then you're right, you don't technically need the 'Apply
variant, provided that std.contract.get_immediate/delayed
exist and work across all kind of contracts. It's more of an API design question: would that make writing custom contracts nicer, more intuitive and less error prone?
let Nullable = fun Contract =>
std.contract.custom
(fun value =>
if value == null then
'Ok
else
(%contract/immediate% Contract) value
)
(%contract/delayed% Contract)
versus
let Nullable = fun Contract =>
std.contract.parametrized (fun value
if value == null then
'Ok
else
'Apply {contract = Contract}
)
It's worth discussing the possibility, I think.
Depends on #1970 #1978.
Continuing the preliminary work toward a
one_of
combinator, it appeared that explicitly separating contracts into an immediate part (more or less a predicate) and a delayed part (the partial identity) is very compelling, both theoretically and semantically, and as a user interface. It makes the behavior of boolean contract combinators trivial to explain and to implement.This PR thus changes both the documentation and the representation of general custom contracts to adhere to this vision: that is, a custom contract is now a pair
immediate: Option<RichTerm>, delayed: Option<RichTerm>
. A nice consequence is that the Rust implementation is simplified: instead of having a lot of ad-hoc cases (predicates, validators, custom, delayed) and corresponding primops, they can all be encoded as general custom contract using only one primop constructor%contract/custom% : Option ImmediatePart -> Option DelayedPart -> Contract
. Their treatment is more uniform throughout the code base.Follow-up work
Builtin contracts
Ideally, all builtin contracts - that is the one derived from records and from static types - would be represented this way, or at least have explicit immediate and delayed part. This is the role of the new primop
contract/get_immediate
andcontract/get_delayed
. For custom contracts, they can just extract the corresponding component. The next step is that they also work on records and static types. However, this requires a non trivial rewrite of builtin contracts, and how they are generated from static types. While migrating builtin contracts to the new paradigm will be required to have boolean operators that work on them, it's not strictly necessary - for now, we keep them as naked functions, which still works. Because this PR is already big, we'll defer the migration of builtin contracts to follow-up work.Parametrized contracts
Currently, the immediate part can only return
'Ok
(early success),'Proceed
(success but apply delayed part) and'Error
(early failure). This means that, to be able to apply another contract, one needs to implement it in the delayed part. For example, the Nullable contract.The consequence is that although we could (we have all the required information) very much compute a purely immediate contract for
Nullable Number
, we currently can't. I think one possibility is to add a new return value for the immediate part,'Apply contract
, which would indicates to the contract system that the immediate part should proceed with a contract application. The immediate part of the resulting contract would thus be the (obvious) composition of both immediate parts, and we would have thatNullable {foo | String}
has a delayed part, butNullable Number
doesn't.This is left for future work as well.