Trait system

[fmease]

There are several ideas already (in the design document) but there is no "final" decision yet. My tendency since forever is a manual trait system meaning records + implicit parameters type 2 (no normal type inference but a search through module-local bindings with unifiable types).

1^st Design Proposal: Records and Automatic Parameters

Trait (type class, interface, …) definitions are just records (#18, #42) and trait bounds (type class constraints) are automatic parameters.

Automatic parameters show similarities to implicit ones but the algorithm for "inferring" them is vastly different. For implicits, the type checker applies type inference (applying inference rules and synthesizing values to fill inference variables). For "automatics", the type checker searches the module scope (!) (implies trait impls need to be used) for bindings matching the required type probably substituting implicits or whatever. It will throw an error on ambiguity. Has a depth to not search endlessly (seems to be necessary in Idris 1 for some good reason). Temporary syntax is two single quotes ("double ticks") mirroring implicits which have merely a single single quote (assuming #63).

Example:

;; a trait declaration
data Monoid (A: Type): Type =
    monoid '(A: Type)
        (field empty: A)
        (field append: A -> A -> A): Monoid A
        ;; ^ generates field accessor of type
        ;; `'(A: Type) -> ''(Monoid A) -> (A -> A -> A)`

;; trait implementations
monoid-nat-sum: Monoid Nat =
    Monoid.monoid
        (empty = 0)
        (append = +)

monoid-nat-product: Monoid Nat =
    Monoid.monoid
        (empty = 1)
        (append = *)

;; trait bounds
append-thrice '(A: Type) ''(monoid: Monoid A) (a: A): A =
    use Monoid.monoid.append in
    append a (append a a)
    ;; ^ or `append ''monoid a (append ''monoid a a)`
    ;; or (with ergonomic record fields): `monoid#append a (monoid#append a a)`

;; usage (in this case, the trait implementation needs to be manually supplied as there are two
;; matching ones)
thing: Nat = append-thrice ''monoid-nat-product 2 ;; => 8
;; ^ or (with erg. r. fields): `monoid-nat-product#append-thrice 2`

Pros:

• less distinct concepts (primitives) in the surface language
  • interactions with other features don't need to be analyzed as it's already based on existing features
  • less to learn for newcomers
• less to implement (?)
• allows multiple implementations for a type (non-canonicity)
• requires users to name trait implementations and the names won't be beautiful in most cases but simply descriptive)

Cons:

• worse error messages (this phenomenon is always imposed by designs involving non-primitives)
• verbose, clunky, maybe less readable
• hacky because of "arbitrary" restrictions around resolving automatic parameters
• unclear how to realize default and especially minimal method implementations
• unclear how to alias trait methods (= record fields) to punctuation (e.g. Monoid.monoid.<> aliasing Monoid.monoid.append)
• allows multiple implementations for a type (non-canonicity)

2^nd Design Proposal: Records with Syntactic Sugar and Automatic Parameters

Introduce trait declarations (beginning with the keyword trait) which are lowered to records (but probably with the information of them being desugared traits preserved).

Meta: Expand upon this description.

3^rd Design Proposal

Meta: Design.

[fmease]

for constraints, we can reuse ? instead of using '':

test '(A: Type) ?(Monoid A) (a b c: A): A = ?test
;;; the ('(A: Type) -> ?(Monoid A) -> A -> A -> A -> A) test