This repository has been archived by the owner on Nov 23, 2022. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 1
Support default implementations #1
Labels
enhancement
New feature or request
Comments
...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)) |
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Problem
an example in mlx1:
direct translation (mlx1-like syntax):
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 forNum Int
.A possible translation is shown below. Here,
numD_37
is occurred in the rhs of its definition.Possible solution
Using lazy evaluation:
The text was updated successfully, but these errors were encountered: