monte-language / typhon

A virtual machine for Monte.
Other
67 stars 10 forks source link

Transparent value objects can't carry custom guards #228

Open MostAwesomeDude opened 3 years ago

MostAwesomeDude commented 3 years ago

Yet another stumbling block on the road to data classes.

erights commented 3 years ago

I know I am without context beyond my E understanding. But from the title this sounds like something I should understand. Could you explain, starting from nothing but knowledge of E and very little understanding of Monte?

cc @dckc

dckc commented 3 years ago

My vague understanding is: we have makeTransparentKit (sp?) that gives you pieces for building transparent objects. The claim here is that when you build them, they can't be DeepFrozen... Presumably because of some gordian knot that's tied with promises.

dckc commented 3 years ago

Presumably because of some gordian knot that's tied with promises.

to wit, these def / bind pairs turn into promises:

object Transparent as DeepFrozenStamp:
...
    to makeAuditorKit():
...
        def _valueAuditor
        def _serializer
...
        bind _valueAuditor.audit(audition) implements DeepFrozenStamp:
...
        bind _serializer implements DeepFrozenStamp:
...
        def valueAuditor :Same[_valueAuditor] := _valueAuditor
        def serializer :Same[_serializer] := _serializer
        return [makerAuditor, &&valueAuditor, &&serializer]

https://github.com/monte-language/typhon/blob/master/mast/prelude/transparent.mt#L34-L35

MostAwesomeDude commented 3 years ago

I will go in reverse.

In fd7a9ba96fa520cad9bd48e6926ccf6e4e2ec6a2, I wanted to have a Transparent object specifically so that I could take advantage of .sameEver/2 equality comparisons and use them as map keys. However, I also wanted my wrapper maker to guard that it is not built with invalid data, because it refines an Int value.

Our current implementation of Transparent does not allow guards on the maker's parameters. If a user tries to guard them, then they will receive a message like, "Makers of Transparent objects currently must have only unguarded FinalSlot patterns in their signature, not Int <= 0". When the guard is DeepFrozen then the message says "DeepFrozen", as in the old title of this issue.

Our implementation does allow for DeepFrozen to transparently distribute over Transparent objects. This does require Typhon runtime support and is specific to DeepFrozen.

I suspect @washort or @kpreid may have specific memories of why the implementation does this. There's an obvious complication to simply adding guards onto the maker; it breaks the round-trip properties that Transparent is meant to certify in the first place! The workaround I checked in for lib/natset, running guards inside the maker, is acceptable in terms of readability and maintenance, but it would be nice to be able to statically encode those guards in the maker's signature.

kpreid commented 3 years ago

I suspect @washort or @kpreid may have specific memories of why the implementation does this. There's an obvious complication to simply adding guards onto the maker; it breaks the round-trip properties that Transparent is meant to certify in the first place! The workaround I checked in for lib/natset, running guards inside the maker, is acceptable in terms of readability and maintenance, but it would be nice to be able to statically encode those guards in the maker's signature.

I haven't been following your work, but I can comment on what I remember of my thoughts at the time I was working on E-on-CL. A guard is essentially an arbitrary function, so if a maker has a guard in its parameters that modifies the value in a non-idempotent fashion, then it can't be used for Transparent purposes since it would modify the state.

The natural solution here is that guards may be guaranteed idempotent (which could be checked by an auditor of the guard's code / rubberstamped for primitive guards), and a maker of Transparent objects (or at least Selfless ones) must require that any guards that are used are idempotent.

For example, a guard whose code, as observed by an IdempotentGuard auditor, is of the form

  1. Check if some particular auditor A approved the given object. If so, return it.
  2. Try coercions as desired (arbitrary code).
  3. Check if auditor A approved the result of the coercion. If so, return it.
  4. Report failure.

must be idempotent since (a) it only returns objects approved by a specific auditor and (b) if given such an object, always returns it and not some other.