Support default implementations

[coord-e]

Problem

an example in mlx1:

 class<T> Num {
   zero :: T,
   sub :: T -> T -> T,
   neg :: T -> T = sub zero
 } in
 impl Num for Int {
   zero = 0,
   sub x y = x - y
 } in
 neg 1

direct translation (mlx1-like syntax):

 type Num = ΛT. constraint numD (T, T -> T -> T, T -> T) in
 overload (∀'a. Num 'a) in
 let zero = numD#0 in
 let sub = numD#1 in
 let neg = numD#2 in
 instance (Num Int) = (0, sub_int, sub zero) in
 neg 1

It is possible (by adding the instance itself to the context in translation of rhs of instance) to type and translate this example to OCaml, however, the resulting translation cannot be compiled because a value recursion happens in the dictionary for Num Int.

A possible translation is shown below. Here, numD_37 is occurred in the rhs of its definition.

let zero = (fun numD_22 -> fst3 (numD_22)) in
let sub = (fun numD_29 -> snd3 (numD_29)) in
let neg = (fun numD_36 -> thd3 (numD_36)) in
let numD_37 = (0, sub_int, sub (numD_37) (zero (numD_37))) in
neg (numD_37) (1)

Possible solution

Using lazy evaluation:

let zero = (fun numD_22 -> fst3 (numD_22)) in
let sub = (fun numD_29 -> snd3 (numD_29)) in
let neg = (fun numD_36 -> Lazy.force (thd3 (numD_36))) in
let rec numD_37 = (0, sub_int, lazy (sub (numD_37) (zero (numD_37)))) in
print_int (neg (numD_37) (1))

[coord-e]

...and mutable recursion

 class<T> Eq {
   eq :: T -> T -> Bool = \x. \y. not (ne x y)
   ne :: T -> T -> Bool = \x. \y. not (eq x y)
 } in
 impl Eq for Int {
   eq = eq_int
 } in
 impl Eq for Float {
   ne = \x. \y. not (eq_float x y)
 } in
 ne 1 2

translation:

type Eq = ΛT. constraint eqD (T -> T -> Bool, T -> T -> Bool) in
overload (∀'a. Eq 'a) in
let eq = eqD#0 in
let ne = eqD#1 in
instance (Eq Int) = (eq_int, \x. \y. not (eq x y)) in
instance (Eq Float) = (\x. \y. not (ne x y), \x. \y. not (eq_float x y)) in
ne 1 2

It seems that lazy evaluation can be applied this case:

let eq = (fun eqD_22 -> Lazy.force (fst (eqD_22))) in
let ne = (fun eqD_22 -> Lazy.force (snd (eqD_22))) in
let rec eqD_37 = (lazy eq_int, lazy (fun x y -> not (eq (eqD_37) x y))) in
let rec eqD_39 = (lazy (fun x y -> not (ne (eqD_39) x y)), lazy (fun x y -> not (eq_float x y))) in
print_bool (ne (eqD_37) (1) (2))