Handling traits in Clarity 2

[jcnelson]

TBD -- we got issues. Need a full specification and test battery.

[jcnelson]

Look at this file here for starters: https://github.com/sskeirik/clarity-trait-experiments/blob/master/run-tests.sh

[gregorycoppola]

Here is a trait issue to think about, "allow trait inside of optional": #3179

[whoabuddy]

I tired to grab all the trait-related issues here, there were a few more about language design outside of that (e.g. #2921).

• Trait Aliases can be Overridden by Local Trait Definition #3215
• Traits with Duplicate Names in Function Signatures are Allowed #3214
• Clarity should permit local binding of global symbols #3182
• Consider: Allow trait reference inside of optional #3179
• Allow the use of addresses stored in constants in contract-call #2811
• read-only functions can not call trait functions even if the implementation uses a read-only function #1981

[sskeirik]

So, here's an issue to discuss that I found in my trait experiments repo.

This contract works:

pass-let-rename-trait

(use-trait math 'SP8CW062DS1XAZJJXWKSM9EMMDD51BRVFMY8MBX6.math-trait.math)

(define-public (add-call (math-contract <math>) (x uint) (y uint))
  (contract-call? math-contract add x y)
)

(define-public (add-call-indirect (math-contract <math>) (x uint) (y uint))
  (let ((new-math-contract math-contract))
    (add-call new-math-contract x y)
  )
)

But this contract doesn't work:

call-let-rename-trait

(use-trait math 'SP8CW062DS1XAZJJXWKSM9EMMDD51BRVFMY8MBX6.math-trait.math)

(define-public (sub-call (math-contract <math>) (x uint) (y uint))
  (let ((new-math-contract math-contract))
    (contract-call? new-math-contract sub x y)
  )
)

So, after the call today, my understanding is that trait-likeness is supposed to be dropped after a let-renaming. However, the checker still lets it be used as a parameter to a trait-valued function.

For consistency, I think that pass-let-rename-trait should fail analysis if call-let-rename-trait does. If this is a real issue, I am happy to file a bug report.

[sskeirik]

I have another example from the trait experiments repo that I'm unsure of.

The checker accepts this contract:

renamed-trait-cast

(use-trait empty      'SP8CW062DS1XAZJJXWKSM9EMMDD51BRVFMY8MBX6.empty-trait.empty)
(use-trait empty-copy 'SP8CW062DS1XAZJJXWKSM9EMMDD51BRVFMY8MBX6.empty-trait.empty)

(define-public (use-empty (empty-contract <empty>))
  (ok true)
)

(define-public (use-empty-copy (empty-contract <empty-copy>))
  (use-empty empty-contract)
)

This contract uses the same trait twice but with a different name and then the checker allows those two trait aliases to be used interchangeably.
Do we consider these two aliases to be different types or the same type?

EDIT: I am happy to file an issue on this too if this is not the intended behavior.

[kantai]

For trait-checking and dynamic invocation, here would be a proposed set of changes that would make traits behave more coherently and less surprisingly to trait users:

1. Eliminate traits from the type system in Clarity2. Trait arguments to methods always have a principal type. The type checker only uses traits to perform type validation of arguments to contract-call and the result of the contract-call (it doesn't validate that the first argument is a trait, and if the function itself has trait arguments, the type checker only checks them as if they were principal arguments.).
2. Add a new static pass which:
   a. Iterates over the AST, tagging each AST node as "dyn-callable" if that node is a direct reference to a trait argument (so that if you let assign a trait argument, or store it in a data-map, etc., it loses "dyn-callable").
   b. Tags each "dyn-callable" node with that node's trait.
3. Add another static pass, which depends on the previous pass, that checks if a contract-call is dynamic or if it has any trait arguments. This pass uses the annotations from the previous pass to validate those calls.
4. During runtime, contract-call checks the AST to ensure that any use of a trait has been marked dyn-callable or is a Literal.

This should result in the following semantics:

1. The contract invoked in any dynamic call during a transaction would be explicitly listed as an argument in the transaction's contract-calls.
2. Literals may continue to be used as trait arguments in a contract call.
3. "Trait objects" are always contract principals -- they are not part of the type system, rather they are markers for whether or not a dynamic call can be made using a supplied principal.
4. The ability to dynamic call using a supplied principal does not survive any data-flows. Only direct references to the trait argument may be dynamic call targets.

[kantai]

This wouldn't be a simple set of changes for Clarity2 -- extricating Traits from the type system may require two different ClarityType types so that Stacks nodes remain capable of executing Clarity1 contracts.

[obycode]

Two comments come to mind:

• The limitations on a trait "marker" surviving data-flow seems unnecessary. I'm not clear on what benefit that has. I don't think it adds anything to the readability or analyzability of the contract.
• If a trait is not a type, then contract-of seems unnecessary. In that case, I would expect that a trait should implicitly cast to a principal.

[obycode]

Can we also explore the other path, fully embracing a trait as a type?

The related pain points that I've seen for developers are:

1. Can't store a trait (in a data-var, constant, or map)
2. Can't pass a trait embedded in an optional, list, response

(1) is not doable while maintaining the ability to do complete static analysis on a contract call without state info, but (2) seems reasonable. The let-binding discussed above seems to fall into the same category of functionality as (2). (2) should come naturally if trait is treated as a type, but there may be some problems with the current implementation that could be addressed.

[kantai]

I can support this approach -- does this mean extending the clarity::types::Value enum to include a new Trait variant (or maybe CallableContract)? Then, enforcing storage by something like gating the storage methods?

[obycode]

Yes, that sounds like the right approach to me.

I'm going to start really digging into the type-checker this afternoon to better understand what is currently in place and what needs to be changed. The key pieces in the type-checker seem to be:

1. Type-check contract call to trait
2. Type-check implicit cast from principal literal to trait as argument to call with trait parameter type
3. Type-check implicit cast from trait A to trait B as argument to call with trait parameter type (legal when B ⊆ A)
4. Type-check definitions for data-vars and maps (traits not allowed)

If the trait is treated as other types, then the type inference at a let binding should function properly, and the embedding of traits in other types should function properly.

[njordhov]

Eliminate traits from the type system in Clarity2. Trait arguments to methods always have a principal type.

Perhaps this is an opportunity to make traits a refinement type of principal, as proposed in clarity-lang/reference#24

[obycode]

That's interesting. I hadn't looked at that proposal before. I like the syntax you use there. The challenge is that our time is running out for 2.1... I will spend some time to think about how much work this would be. We can also discuss if others would be open to a syntactical change like that.