Contracts and Type Annotations #912

New issue

2023-09-22T19:57:26Z

vyzo commented

2023-09-22 19:57:26 +00:00

(Migrated from github.com)

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.

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 commented

2023-09-25 12:20:49 +00:00

(Migrated from github.com)

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?
   ...))

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? ...)) ```

👍 1

vyzo commented

2023-09-25 13:30:53 +00:00

(Migrated from github.com)

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

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

We can also extend struct and class definitions to add type annotations to members: ``` (defstruct X ((a :- fixnum?) ...) ...) (defclass X ((a :- fixnum?) ...) ...) ```

fare commented

2023-09-25 13:35:15 +00:00

(Migrated from github.com)

: 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.

`:` 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 commented

2023-09-25 13:36:00 +00:00

(Migrated from github.com)

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

vyzo commented

2023-09-25 13:39:18 +00:00

(Migrated from github.com)

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

The :std/contract macros will expand to that.

Yes, the prefix syntax will be raw annotation: `(begin-annotation (type ...) expr)`. The `:std/contract` macros will expand to that.

vyzo commented

2023-09-25 13:40:16 +00:00

(Migrated from github.com)

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

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

vyzo commented

2023-09-25 13:40:52 +00:00

(Migrated from github.com)

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

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

vyzo commented

2023-09-25 13:41:37 +00:00

(Migrated from github.com)

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

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

vyzo commented

2023-09-25 13:44:21 +00:00

(Migrated from github.com)

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

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 commented

2023-09-25 13:44:49 +00:00

(Migrated from github.com)

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

vyzo commented

2023-09-26 08:52:49 +00:00

(Migrated from github.com)

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.

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 commented

2023-09-26 08:54:34 +00:00

(Migrated from github.com)

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

:~
:&
:!

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

vyzo commented

2023-09-28 10:56:37 +00:00

(Migrated from github.com)

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.

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 commented

2024-05-05 12:38:03 +00:00

(Migrated from github.com)

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

Sign in to join this conversation.