Contracts and Type Annotations

[vyzo]

Following some prototype work some years ago in #417, I have reached some conclusions about the functionality that we want.

• We want def/lambda forms (they don't have to be in the core prelude, it can be a redef from :std/contract or :std/typed).
• We want to be able to declare both checked contracts and type assertions
  • Checked contracts will have the form (arg :: predicate-expr) and they imply a contract generated check and an assertion propagated once the check passes.
  • Assertions will have the form (arg -: predicate-expr) and will have the form of programmer declarations. The assertions will be propagated as gospell (trust the programmer, hopefully he is not holding his footgun).
  • Return type assertions will have the form >: predicate-expr and provide information for the compiler to propagate return values. Note that it is not reasonable to generate checks for those, as it will break tail recursion. The compiler can however check (or infer) the return value and emit a warning (or error) if the programmer has made a mistake.
• We want to attach them to interfaces
• We want the compiler to take action on propagated type assertions and emit check eliding code.
• We want a :gerbil/typed language prelude that integrates all of the above.

[vyzo]

A better syntax proposal that doesn't use keywords:

• := for checked contracts
• :- for type assertions
• :> for return types

So here is a definition for a procedure that mixes all of them:

(def (do-something (a := A?) (b :- fixnum?)) :> fixnum?
  ... ; body
)

This could also be attached to an interface:

(interface X
  (method-a (a := A?) (b := fixnum?)) :> fixnum?
  ...)

And method can simply make type assertions because the interface facade has already checked the contracts:

(defmethod {X x-class}
  (lambda (self (a :- A?) (b :- fixnum?)) :> fixnum?
   ...))

[vyzo]

We can also extend struct and class definitions to add type annotations to members:

(defstruct X ((a :- fixnum?) ...) ...)
(defclass X ((a :- fixnum?) ...) ...)

[fare]

: or :: is a widely accepted standard for type annotations (including return type annotations), and I see no reason to depart from it. For other annotations, sure do our own things.

[fare]

Don't we need a regular prefix syntax, too? Or are we becoming Rhombus? Better read the Rhombus paper, then... is it out?

[vyzo]

Yes, the prefix syntax will be raw annotation: (begin-annotation (type ...) expr).

The :std/contract macros will expand to that.

[vyzo]

ok, fair enough, we can us :: for return type.

[vyzo]

although... I don't want a keyword really, I want a syntactic token.

[vyzo]

: is unclear -- is it contract or type assertion? We have both, hence the discriminant with :- and :=.

[vyzo]

Return type annotation can also use :- and := -- Semantics:

• :- is assertion, compiler just trusts you
• := is soft, compiler will verify the return type statically and reject if it doesn't work

[vyzo]

Note that this opens the door for the inevitable dependent types further down the road.

[vyzo]

Following discussion with fare, we have reached consensus, although we are not sure about the exact assertion operator name.

The current proposal:

• : for checked type contracts, both for input and output parameters. The compiler will perform (best effort) checks at compile time, and if the type contract is not satisfied, it will emit an error. If the contract is satisfied at compile time, it should generate code that avoids the runtime check. If it is unknown, then the contract will be checked at runtime for input parameter. We also have the option of checking output parameters at call sites, perhaps we could enable this with a strict compilation option.
• :- for unchecked type assertions. If the compiler sees a violation at compile time, it will emit a warning.

[vyzo]

Other possible symbols for type assertions (@fare wants to uglify them, I want to keep them tidy):

• :~
• :&
• :!

[vyzo]

Preliminaries in #934; here is the syntactic tokens we settled on:

• : checked type declaration; it will emit an instance check at the boundary.
• :~ checked predicate contract; it will emit a predicate check at the boundary.
• :- unchecked type assertion; the big gun, hopefully unsuitable for feet.

[vyzo]

this is mostly done with types gerbil, awaiting the v0.18.2 release.