Polymorphism support #848

2021-11-24T19:19:54+09:00

ghallak commented

2021-11-24 19:19:54 +09:00

(Migrated from gitlab.com)

Fixes: #307

ghallak commented

2021-11-25 20:57:46 +09:00

(Migrated from gitlab.com)

I have noticed that the type for the function declaration entrypoint init : () => unit is:

{fun_t,_,[],[],{id,_,"unit"}}

While the type of the function entrypoint init() = () is:

{tuple_t,_,[]}

The function aeso_ast_infer_types:unfold_types_in_type replaces {id, _, "unit"} with {tuple_t, _, []}, but it does not seems to be called on the fun_t type.

@hanssv Do you know if this is a bug or if it's done on purpose?

I have noticed that the type for the function declaration `entrypoint init : () => unit` is: ``` {fun_t,_,[],[],{id,_,"unit"}} ``` While the type of the function `entrypoint init() = ()` is: ``` {tuple_t,_,[]} ``` The function `aeso_ast_infer_types:unfold_types_in_type` replaces `{id, _, "unit"}` with `{tuple_t, _, []}`, but it does not seems to be called on the `fun_t` type. @hanssv Do you know if this is a bug or if it's done on purpose?

zxq9 commented

2021-11-25 21:31:16 +09:00

(Migrated from gitlab.com)

Created by: hanssv

I have no recollection of it being done on purpose...

*Created by: hanssv* I have no recollection of it being done on purpose...

zxq9 commented

2021-11-26 00:51:43 +09:00

(Migrated from gitlab.com)

Created by: hanssv

I think we are soon approaching the point where this should become a record, something to consider for the next addition 😅

*Created by: hanssv* I think we are soon approaching the point where this should become a record, something to consider for the _next_ addition 😅

zxq9 commented

2021-11-26 00:53:39 +09:00

(Migrated from gitlab.com)

Created by: hanssv

This looks like an exponential blowup - we should consider a rewrite some day...

*Created by: hanssv* This looks like an exponential blowup - we should consider a rewrite some day...

zxq9 commented

2021-11-26 00:55:09 +09:00

(Migrated from gitlab.com)

Created by: hanssv

Review: Dismissed

Looks good to me 👍

*Created by: hanssv* **Review:** Dismissed Looks good to me 👍

zxq9 commented

2021-12-16 01:08:38 +09:00

(Migrated from gitlab.com)

Created by: radrow

Review: Changes requested

I would like to see tests for:

Implementing many interfaces
Implementing two interfaces with entrypoints of same names and types
Implementing two interfaces with entrypoints of same names and different types
Variance switching case, in particular that assuming contract Cat : Animal:
- let f(x : Cat) : Animal = (g : Animal => Cat) works
- let f(x : Animal) : Animal = (g : Cat => Cat) does not work
- let f(x : Cat) : Cat = (g : Cat => Animal) does not work
- let f(x : Animal => Cat) : Animal = (g : (Cat => Animal) => Cat) works
- let f(x : Cat => Cat) : Animal = (g : (Animal => Animal) => Cat) does not work
Interface implementing an interface
Interface implementing an interface with an entrypoint of the same name and type
Interface implementing an interface with an entrypoint of the same name and different type

*Created by: radrow* **Review:** Changes requested I would like to see tests for: - Implementing many interfaces - Implementing two interfaces with entrypoints of same names and types - Implementing two interfaces with entrypoints of same names and different types - Variance switching case, in particular that assuming `contract Cat : Animal`: - `let f(x : Cat) : Animal = (g : Animal => Cat)` works - `let f(x : Animal) : Animal = (g : Cat => Cat)` does not work - `let f(x : Cat) : Cat = (g : Cat => Animal)` does not work - `let f(x : Animal => Cat) : Animal = (g : (Cat => Animal) => Cat)` works - `let f(x : Cat => Cat) : Animal = (g : (Animal => Animal) => Cat)` does not work - Interface implementing an interface - Interface implementing an interface with an entrypoint of the same name and type - Interface implementing an interface with an entrypoint of the same name and different type

zxq9 commented

2021-12-16 20:54:18 +09:00

(Migrated from gitlab.com)

Created by: radrow

Also, please refer some runtime tests in aeternity repo, so we are sure nothing breaks there.

*Created by: radrow* Also, please refer some runtime tests in aeternity repo, so we are sure nothing breaks there.

ghallak commented

2021-12-20 22:34:17 +09:00

(Migrated from gitlab.com)

@hanssv @UlfNorell In the case of implementing two interfaces with entrypoints of the same name and same type

contract interface I =
    entrypoint f : () => int

contract interface J =
    entrypoint f : () => int

contract C : I, J =
    entrypoint f() = 1

Do you think this should pass as a function called f with the type () => int is already implemented? Or should it fail since only one of the interfaces is implemented, and not the other?

I already have this test and it's failing, but I'm wondering if it should.

@hanssv @UlfNorell In the case of implementing two interfaces with entrypoints of the same name and same type ``` contract interface I = entrypoint f : () => int contract interface J = entrypoint f : () => int contract C : I, J = entrypoint f() = 1 ``` Do you think this should pass as a function called `f` with the type `() => int` is already implemented? Or should it fail since only one of the interfaces is implemented, and not the other? I already have [this test](https://github.com/aeternity/aesophia/blob/8c42f69407778e946fd0ba2dff400bc941a2721b/test/contracts/contract_polymorphism_same_decl_multi_interface.aes) and it's failing, but I'm wondering if it should.

zxq9 commented

2021-12-20 22:50:26 +09:00

(Migrated from gitlab.com)

Created by: UlfNorell

I think the least error prone option is to not allow implementing interfaces with overlapping entrypoints. So in this case it should give an error already on contract C : I, J =. I don't see any great harm in allowing it though, so if there are convincing use cases where you want overlapping interfaces we could accept it.

*Created by: UlfNorell* I think the least error prone option is to not allow implementing interfaces with overlapping entrypoints. So in this case it should give an error already on `contract C : I, J =`. I don't see any great harm in allowing it though, so if there are convincing use cases where you want overlapping interfaces we could accept it.

zxq9 commented

2021-12-21 06:35:21 +09:00

(Migrated from gitlab.com)

Created by: radrow

Do we have a test if C does not implement f?

*Created by: radrow* Do we have a test if C does not implement f?

ghallak commented

2021-12-22 03:32:17 +09:00

(Migrated from gitlab.com)

Yes, contract_polymorphism_missing_implementation and it shows an error.

Yes, [contract_polymorphism_missing_implementation](https://github.com/aeternity/aesophia/blob/8c42f69407778e946fd0ba2dff400bc941a2721b/test/contracts/contract_polymorphism_missing_implementation.aes) and it shows an error.

zxq9 commented

2021-12-22 08:06:45 +09:00

(Migrated from gitlab.com)

Created by: marc0olo

@ghallak I agree with Ulf, as long as there is no valid usecase to argue for we shouldn't allow implementing interfaces with overlapping entrypoints

*Created by: marc0olo* @ghallak I agree with Ulf, as long as there is no valid usecase to argue for we shouldn't allow implementing interfaces with overlapping entrypoints

zxq9 commented

2021-12-26 03:47:13 +09:00

(Migrated from gitlab.com)

Created by: radrow

I'd also modify some tests to involve tuples, maps, lists etc and custom types, so we are sure that subtyping works on them too

*Created by: radrow* I'd also modify some tests to involve tuples, maps, lists etc and custom types, so we are sure that subtyping works on them too

zxq9 commented

2022-02-13 20:24:20 +09:00

(Migrated from gitlab.com)

Created by: radrow

this could be a separate function imo

*Created by: radrow* this could be a separate function imo

zxq9 commented

2022-02-13 20:31:59 +09:00

(Migrated from gitlab.com)

Created by: radrow

I guess?

                    bivariant     -> is_subtype(Env, NameA, NameB) orelse is_subtype(Env, NameB, NameA)

*Created by: radrow* I guess? ```suggestion:-0+0 bivariant -> is_subtype(Env, NameA, NameB) orelse is_subtype(Env, NameB, NameA) ```

zxq9 commented

2022-02-13 20:33:40 +09:00

(Migrated from gitlab.com)

Created by: radrow

This could be a is_subtype/4 that calls is_subtype/3, less indentation

*Created by: radrow* This could be a `is_subtype/4` that calls `is_subtype/3`, less indentation

zxq9 commented

2022-02-13 20:35:10 +09:00

(Migrated from gitlab.com)

Created by: radrow

Would you verify if it does not explode exponentially if you hack it?

*Created by: radrow* Would you verify if it does not explode exponentially if you hack it?

ghallak commented

2022-02-24 20:54:10 +09:00

(Migrated from gitlab.com)

Done here 7b5c9778b4f39dd6a96c1ea07d5978031ca90bc8

ghallak commented

2022-02-24 21:04:08 +09:00

(Migrated from gitlab.com)

Done here cd3da44973ca25574079ae4f1c1a930c8828d6d6

ghallak commented

2022-02-24 21:04:17 +09:00

(Migrated from gitlab.com)

Done here cd3da44973ca25574079ae4f1c1a930c8828d6d6

zxq9 commented

2022-04-11 19:13:59 +09:00

(Migrated from gitlab.com)

Created by: radrow

Why do you destroy and immediately create?

*Created by: radrow* Why do you destroy and immediately create?

zxq9 commented

2022-04-11 19:14:13 +09:00

(Migrated from gitlab.com)

Created by: radrow

This check should go to a separate function imo

*Created by: radrow* This check should go to a separate function imo

zxq9 commented

2022-04-11 19:14:49 +09:00

(Migrated from gitlab.com)

Created by: radrow

Move out

*Created by: radrow* Move out

zxq9 commented

2022-04-11 19:15:52 +09:00

(Migrated from gitlab.com)

Created by: radrow

infer1 should read like a prose, otherwise we a growing a hydra

*Created by: radrow* `infer1` should read like a prose, otherwise we a growing a hydra

zxq9 commented

2022-04-11 19:29:29 +09:00

(Migrated from gitlab.com)

Created by: radrow

Function interfaces should be checked as well.

*Created by: radrow* Function interfaces should be checked as well.

zxq9 commented

2022-04-11 19:30:29 +09:00

(Migrated from gitlab.com)

Created by: radrow

Add a test for that:

contract interface I0 =
  entrypoint f() : int

contract interface I1 : I0 =
  entrypoint f() : int

main contract C : I1 =
  entrypoint f() = 3

*Created by: radrow* Add a test for that: ``` contract interface I0 = entrypoint f() : int contract interface I1 : I0 = entrypoint f() : int main contract C : I1 = entrypoint f() = 3 ```

zxq9 commented

2022-04-11 19:39:35 +09:00

(Migrated from gitlab.com)

Created by: radrow

You can write check_implemented_interfaces/4 that runs /5 with the accumulator. This is generally cleaner.

*Created by: radrow* You can write `check_implemented_interfaces/4` that runs `/5` with the accumulator. This is generally cleaner.

zxq9 commented

2022-04-11 19:48:30 +09:00

(Migrated from gitlab.com)

Created by: radrow

Add a comment that you are solving the diamond problem here, it took me a while to get to this XD

*Created by: radrow* Add a comment that you are solving the diamond problem here, it took me a while to get to this XD

zxq9 commented

2022-04-11 19:52:00 +09:00

(Migrated from gitlab.com)

Created by: radrow

Add comments on these functions, the name does not capture the point entirely and the logic is not super trivial

*Created by: radrow* Add comments on these functions, the name does not capture the point entirely and the logic is not super trivial

zxq9 commented

2022-04-11 19:53:24 +09:00

(Migrated from gitlab.com)

Created by: radrow

Empty lists don't match?

*Created by: radrow* Empty lists don't match?

zxq9 commented

2022-04-11 19:54:38 +09:00

(Migrated from gitlab.com)

Created by: radrow

Var args are Chain exclusive and they should imo remain this way, so no need to worry about them. Regarding named args, you can just match them by name and type

*Created by: radrow* Var args are `Chain` exclusive and they should imo remain this way, so no need to worry about them. Regarding named args, you can just match them by name and type

zxq9 commented

2022-04-11 19:58:17 +09:00

(Migrated from gitlab.com)

Created by: radrow

What is compare_types for? Why not just check for names (and maybe arity) and then rely on subtyping?

*Created by: radrow* What is `compare_types` for? Why not just check for names (and maybe arity) and then rely on subtyping?

zxq9 commented

2022-04-11 20:06:17 +09:00

(Migrated from gitlab.com)

Created by: radrow

What does it mean here?

*Created by: radrow* What does it mean here?

zxq9 commented

2022-04-11 20:08:25 +09:00

(Migrated from gitlab.com)

Created by: radrow

I think you can just have a set for co and contra and then

case {Co, Contra} of
  {t, f} -> co
  {f, t} -> contra
  {t, t} -> inv
  {f, f} -> bi

*Created by: radrow* I think you can just have a set for co and contra and then ``` case {Co, Contra} of {t, f} -> co {f, t} -> contra {t, t} -> inv {f, f} -> bi ```

zxq9 commented

2022-04-11 20:10:23 +09:00

(Migrated from gitlab.com)

Created by: radrow

I think it would be easier and simpler to use infer_type_vars_variance to dive into the type and just maintain an additional argument that tells what the current variance is. Then you won't need to count this.

*Created by: radrow* I think it would be easier and simpler to use `infer_type_vars_variance` to dive into the type and just maintain an additional argument that tells what the current variance is. Then you won't need to count this.

zxq9 commented

2022-04-11 20:12:15 +09:00

(Migrated from gitlab.com)

Created by: radrow

I need explanation on this, I totally don't get what's going on here. Also, why do you check only the result type and don't touch the args?

*Created by: radrow* I need explanation on this, I totally don't get what's going on here. Also, why do you check only the result type and don't touch the args?

zxq9 commented

2022-04-16 03:10:34 +09:00

(Migrated from gitlab.com)

Created by: radrow

The error messages here could be more elaborate. I can already see people scratching their heads why Cat does not unify with Animal, but sometimes the other way around. I think it would be valuable to mention the variance in the message:

Cannot unify A with B in a contravariant context

Or something. Even if one does not know the concept of variance, they know at least what to google.

*Created by: radrow* The error messages here could be more elaborate. I can already see people scratching their heads why Cat does not unify with Animal, but sometimes the other way around. I think it would be valuable to mention the variance in the message: ``` Cannot unify A with B in a contravariant context ``` Or something. Even if one does not know the concept of variance, they know at least what to google.

zxq9 commented

2022-04-16 03:12:34 +09:00

(Migrated from gitlab.com)

Created by: radrow

Add tests for custom datatypes, records and type aliases. Please consider various variances. Also there should be tests for tuples, maps, lists and oracles.

*Created by: radrow* Add tests for custom datatypes, records and type aliases. Please consider various variances. Also there should be tests for tuples, maps, lists and oracles.

zxq9 commented

2022-04-16 03:15:04 +09:00

(Migrated from gitlab.com)

Created by: radrow

Note that they serve for remote contracts as well!

*Created by: radrow* Note that they serve for remote contracts as well!

zxq9 commented

2022-04-16 03:18:40 +09:00

(Migrated from gitlab.com)

Created by: radrow

I make this note here because I couldn't find any better place; what about builtin types such as option, oracle and oracle_query? How do you handle them?

*Created by: radrow* I make this note here because I couldn't find any better place; what about builtin types such as option, oracle and oracle_query? How do you handle them?

ghallak commented

2022-04-19 22:39:54 +09:00

(Migrated from gitlab.com)

Removing that was causing a failed test, but I've just found out that the failing test was failing because of another mistake that I've made.

Fixed here: 4790566f427a3f9ec01b41a61217a7fe319d2525

Removing that was causing a failed test, but I've just found out that the failing test was failing because of another mistake that I've made. Fixed here: 4790566f427a3f9ec01b41a61217a7fe319d2525

ghallak commented

2022-04-20 19:00:13 +09:00

(Migrated from gitlab.com)

Done here 0a2e11e4e69b68ab10ee1f01e10b776172379664

ghallak commented

2022-04-20 19:00:25 +09:00

(Migrated from gitlab.com)

Done here 0a2e11e4e69b68ab10ee1f01e10b776172379664

ghallak commented

2022-04-20 19:00:38 +09:00

(Migrated from gitlab.com)

Done here 0a2e11e4e69b68ab10ee1f01e10b776172379664

ghallak commented

2022-04-20 19:00:52 +09:00

(Migrated from gitlab.com)

Done here 0a2e11e4e69b68ab10ee1f01e10b776172379664

ghallak commented

2022-04-20 23:45:53 +09:00

(Migrated from gitlab.com)

This is not solving the diamond problem, it's just there to recursively make sure that interfaces implemented by the interface in hand are also implemented by the contract.

Also, does the diamond problem happen in the case when implementing interfaces? Isn't it a problem with inheritance?

This is not solving the diamond problem, it's just there to recursively make sure that interfaces implemented by the interface in hand are also implemented by the contract. Also, does the diamond problem happen in the case when implementing interfaces? Isn't it a problem with inheritance?

ghallak commented

2022-04-20 23:52:36 +09:00

(Migrated from gitlab.com)

There is a comment in this commit 0a2e11e4e6 explaining what the function is doing.

There is a comment in this commit https://github.com/aeternity/aesophia/commit/0a2e11e4e69b68ab10ee1f01e10b776172379664 explaining what the function is doing.

ghallak commented

2022-04-21 00:04:40 +09:00

(Migrated from gitlab.com)

What is the point of duplicating the declaration of f in both I0 and I1 when I'm already checking recursively that C is implementing I1 and all interfaces extended by I1 (only I0 in this case)?

What is the point of duplicating the declaration of `f` in both `I0` and `I1` when I'm already checking recursively that `C` is implementing `I1` and all interfaces extended by `I1` (only `I0` in this case)?

ghallak commented

2022-04-21 00:35:56 +09:00

(Migrated from gitlab.com)

It's been a long time since I wrote this. I didn't know about is_list/1 back then and thought this is the only way to check if a variable is a list.

Fixed here: 55bc58286e224ab54fff62a3b8ae2cd0ca87adcb

It's been a long time since I wrote this. I didn't know about `is_list/1` back then and thought this is the only way to check if a variable is a list. Fixed here: 55bc58286e224ab54fff62a3b8ae2cd0ca87adcb

ghallak commented

2022-04-22 22:05:57 +09:00

(Migrated from gitlab.com)

Done here 62b095affc17a12ff634da242e212c51cbd36a99

ghallak commented

2022-04-22 22:21:12 +09:00

(Migrated from gitlab.com)

Done here bdd3f0dde2f4423722808cdd5478a7a54d62f85f

ghallak commented

2022-04-24 23:59:13 +09:00

(Migrated from gitlab.com)

Done here 39b9bb66cca29f836f8c36a3569df494dbd19aff

ghallak commented

2022-04-25 01:49:07 +09:00

(Migrated from gitlab.com)

This is supposed to work in the case where the function is a type constructor. So it would work for something like:

let x = T(f)

where f is defined as:

function f(_ : Animal) : Cat = some_cat

and T is a type constructor for the datatype tc:

datatype tc('a) = T('a => 'a)

In the above example, when trying to infer the type for T(f), the FunType for T(f) would look something like:

{fun_t,
    Ann1,
    [],
    [{fun_t, Ann2, [], [{uvar, Ann3, Ref}], {uvar, Ann4, Ref}}],
    {app_t, Ann5, {qid, Ann6, ["Main", "tc"]}, [{uvar, Ann7, Ref}]}}

Note that Ref in the return type is the same as the Ref from the args, since the type above is datatype tc('a) = TC('a => 'a), so it's enough to keep track of the Ref in the return type.

This is supposed to work in the case where the function is a type constructor. So it would work for something like: ``` let x = T(f) ``` where `f` is defined as: ``` function f(_ : Animal) : Cat = some_cat ``` and `T` is a type constructor for the datatype `tc`: ``` datatype tc('a) = T('a => 'a) ``` In the above example, when trying to infer the type for `T(f)`, the `FunType` for `T(f)` would look something like: ``` {fun_t, Ann1, [], [{fun_t, Ann2, [], [{uvar, Ann3, Ref}], {uvar, Ann4, Ref}}], {app_t, Ann5, {qid, Ann6, ["Main", "tc"]}, [{uvar, Ann7, Ref}]}} ``` Note that `Ref` in the return type is the same as the `Ref` from the args, since the type above is ` datatype tc('a) = TC('a => 'a)`, so it's enough to keep track of the `Ref` in the return type.

ghallak commented

2022-04-25 01:55:14 +09:00

(Migrated from gitlab.com)

Would it be better to say that Animal is not a subtype of Cat instead of mentioning the variance part? Someone would scratch his head saying that why didn't the compiler check if Cat is a subtype of Animal instead of checking if Animal is a subtype of Cat, but people will always scratch their heads for some reason, and I don't see that mentioning the type of variance making it easier for people to find out what went wrong.

Would it be better to say that `Animal` is not a subtype of `Cat` instead of mentioning the variance part? Someone would scratch his head saying that why didn't the compiler check if `Cat` is a subtype of `Animal` instead of checking if `Animal` is a subtype of `Cat`, but people will always scratch their heads for some reason, and I don't see that mentioning the type of variance making it easier for people to find out what went wrong.

ghallak commented

2022-04-25 02:06:44 +09:00

(Migrated from gitlab.com)

I probably don't get the question.

Here we have access to the datatype's type variables Xs and the constructors for the datatype Cons, and I use that to infer the type variance for these type variables.

Are you asking about something else?

I probably don't get the question. Here we have access to the datatype's type variables `Xs` and the constructors for the datatype `Cons`, and I use that to infer the type variance for these type variables. Are you asking about something else?

ghallak commented

2022-04-25 03:13:40 +09:00

(Migrated from gitlab.com)

I don't think that compare_types is needed, that was meant to be a version of unify that does not give a type error (only returns true or false).

If I use unify here instead of compare_types, I will be getting 2 errors, one cannot_unify error and another unimplemented_interface_function where I only need the second one.

I can modify unify to not give a type error in one of three ways:

Pass a value to When and use that to indicate that we don't need to throw an error in this case (Probably a bad idea since the value When is only used for output)
Add a flag to Env (e.g. unify_no_thorw) and only throw if it's set to true
Add an argument to unify (e.g. ShouldThrow) and only throw if it's set to true (That would cause changes in multiple lines of the code in each definition of unify)

I don't think that `compare_types` is needed, that was meant to be a version of `unify` that does not give a type error (only returns true or false). If I use `unify` here instead of `compare_types`, I will be getting 2 errors, one `cannot_unify` error and another `unimplemented_interface_function` where I only need the second one. I can modify `unify` to not give a type error in one of three ways: 1. Pass a value to `When` and use that to indicate that we don't need to throw an error in this case (Probably a bad idea since the value `When` is only used for output) 2. Add a flag to `Env` (e.g. `unify_no_thorw`) and only throw if it's set to `true` 3. Add an argument to `unify` (e.g. `ShouldThrow`) and only throw if it's set to `true` (That would cause changes in multiple lines of the code in each definition of `unify`)

ghallak commented

2022-04-25 19:28:53 +09:00

(Migrated from gitlab.com)

In the files polymorphism_variance_switching.aes and polymorphism_variance_switching_custom_types.aes there are tests for:

custom datatypes
tuples
maps
lists

I'll add to that tests for:

~~options~~
~~oracles~~
~~oracle queries~~
~~records~~
~~type aliases~~

In the files `polymorphism_variance_switching.aes` and `polymorphism_variance_switching_custom_types.aes` there are tests for: * custom datatypes * tuples * maps * lists I'll add to that tests for: * ~options~ * ~oracles~ * ~oracle queries~ * ~records~ * ~type aliases~

ghallak commented

2022-05-01 01:26:25 +09:00

(Migrated from gitlab.com)

Actually, I have faced the same issue while working on a different PR. I think that adding something like unify_throws = true to the record env could be the best idea here.

Actually, I have faced the same issue while working on a different PR. I think that adding something like `unify_throws = true` to the record `env` could be the best idea here.

zxq9 commented

2022-05-08 18:53:58 +09:00

(Migrated from gitlab.com)

Created by: radrow

My point is to make it behave nicely when you use I1 as an interface for a remote contract. Note that interfaces in Sophia are not abstract like in Java.

Alternatively, the following code should work:

contract interface I0 =
  entrypoint f() : int

contract interface I1 : I0 =
  entrypoint something_else() : int

main contract C =
  entrypoint f(x : I1) = x.f() // Here we should know that x has f

*Created by: radrow* My point is to make it behave nicely when you use `I1` as an interface for a remote contract. Note that interfaces in Sophia are not abstract like in Java. Alternatively, the following code should work: ``` contract interface I0 = entrypoint f() : int contract interface I1 : I0 = entrypoint something_else() : int main contract C = entrypoint f(x : I1) = x.f() // Here we should know that x has f ```

zxq9 commented

2022-05-08 18:56:11 +09:00

(Migrated from gitlab.com)

Created by: radrow

I think the previous name was better, this _recursive is mentioned in the comment anyway

*Created by: radrow* I think the previous name was better, this `_recursive` is mentioned in the comment anyway

zxq9 commented

2022-05-08 18:58:09 +09:00

(Migrated from gitlab.com)

Created by: radrow

Are you sure that named args are sorted at this point? If not, you will have false-negatives on this check.

*Created by: radrow* Are you sure that named args are sorted at this point? If not, you will have false-negatives on this check.

zxq9 commented

2022-05-08 19:02:31 +09:00

(Migrated from gitlab.com)

Created by: radrow

What's wrong with unification errors here?

*Created by: radrow* What's wrong with unification errors here?

ghallak commented

2022-05-09 17:30:57 +09:00

(Migrated from gitlab.com)

I just want to check whether two types are the same or not, and move on if they are not. Unification errors will stop the compilation, and I don't want that.

ghallak commented

2022-05-09 17:49:40 +09:00

(Migrated from gitlab.com)

I have renamed it to check_implemented_interfaces1 here 1e965681cb595dac95828b0f3d2680f89e96f5a1

I have renamed it to `check_implemented_interfaces1` here 1e965681cb595dac95828b0f3d2680f89e96f5a1

ghallak commented

2022-05-11 22:15:17 +09:00

(Migrated from gitlab.com)

This is fixed now, check commits e74c75558b7a1fc5e48740f7f2f17ad7bbe2c76d and 831903e675091883688b43c1753aede892e4d8ab

ghallak commented

2022-05-11 23:39:45 +09:00

(Migrated from gitlab.com)

~~I should probably rename all new test files to have a common prefix related to this PR before merging it.~~ (I have done that here e4db742c72)

~I should probably rename all new test files to have a common prefix related to this PR before merging it.~ (I have done that here https://gitlab.com/gajumaristas/aesophia/-/merge_requests/357/commits/e4db742c72b7e76f1ba72afdc29eae9b2b1d793f)

ghallak commented

2022-05-20 23:50:17 +09:00

(Migrated from gitlab.com)

I have implemented that here 28bf14cc7cbda129dc7d4525e642b145698c1fea

ghallak commented

2022-05-20 23:51:44 +09:00

(Migrated from gitlab.com)

I have tests for all the above now after 114010b8e1ff9a978912f736bd143364666bd89c, 8e995429aa6bd184b3d690f97dacf3ea6fb1b555, eab8eae9c1b97174fa93cb31201805aa45a4a578, and a6f1d8107713baa0379ecbacd06c1e51b4bd112c.

ghallak commented

2022-05-24 20:13:15 +09:00

(Migrated from gitlab.com)

Done that here da6d22717cf3410b97792894aba371f353078ea1

zxq9 commented

2022-05-25 02:31:52 +09:00

(Migrated from gitlab.com)

Created by: radrow

what is x for here?

*Created by: radrow* what is `x` for here?

zxq9 commented

2022-05-25 02:32:22 +09:00

(Migrated from gitlab.com)

Created by: radrow

Shouldn't f0 call g0?

*Created by: radrow* Shouldn't `f0` call `g0`?

zxq9 commented

2022-05-25 02:37:49 +09:00

(Migrated from gitlab.com)

Created by: radrow

this test is duplicated in h0

*Created by: radrow* this test is duplicated in h0

zxq9 commented

2022-05-25 03:24:49 +09:00

(Migrated from gitlab.com)

Created by: radrow

I guess this is supposed to fail? Maybe make a note

*Created by: radrow* I guess this is supposed to fail? Maybe make a note

zxq9 commented

2022-05-25 03:26:09 +09:00

(Migrated from gitlab.com)

Created by: radrow

this fails as well, right?

*Created by: radrow* this fails as well, right?

zxq9 commented

2022-05-25 03:27:41 +09:00

(Migrated from gitlab.com)

Created by: radrow

Would you make the names more descriptive? Don't have to be elaborate, but so it is not necessary to constantly lookup their defs

*Created by: radrow* Would you make the names more descriptive? Don't have to be elaborate, but so it is not necessary to constantly lookup their defs

zxq9 commented

2022-05-25 03:28:07 +09:00

(Migrated from gitlab.com)

Created by: radrow

make names descriptive

*Created by: radrow* make names descriptive

zxq9 commented

2022-05-25 03:28:15 +09:00

(Migrated from gitlab.com)

Created by: radrow

missing bivariant

*Created by: radrow* missing bivariant

zxq9 commented

2022-05-25 03:43:44 +09:00

(Migrated from gitlab.com)

Created by: radrow

Imo oracle queries should be covariant on both positions:

the latter type carries a result that can be retrieved by Oracle.get_answer
the former type carries the question as a plain value under Oracle.get_question

*Created by: radrow* Imo oracle queries should be covariant on both positions: - the latter type carries a result that can be retrieved by `Oracle.get_answer` - the former type carries the question as a plain value under `Oracle.get_question`

zxq9 commented

2022-05-25 03:53:11 +09:00

(Migrated from gitlab.com)

Created by: radrow

...and now I am happy that we don't have recursive datatypes

*Created by: radrow* ...and now I am happy that we don't have recursive datatypes

ghallak commented

2022-05-25 22:29:23 +09:00

(Migrated from gitlab.com)

Done here 530940edd635da436cc737686f57b16f2f420009

ghallak commented

2022-05-25 22:44:41 +09:00

(Migrated from gitlab.com)

Done here c767cd48a4c6399de89cd0eda9046fcd82e92f25

zxq9 commented

2022-05-26 01:44:50 +09:00

(Migrated from gitlab.com)

Created by: radrow

Please move this resolution to another function

*Created by: radrow* Please move this resolution to another function

zxq9 commented

2022-05-26 01:55:53 +09:00

(Migrated from gitlab.com)

Created by: radrow

Wait, is this really ('a => unit) => 'a?! It should be parsed as 'a => (unit => 'a) what would make it invariant. Please check how it parsers and if it parses wrong then create issue to fix it. Also add parens so it is clear that it's ('a => unit) => 'a

*Created by: radrow* Wait, is this really `('a => unit) => 'a`?! It should be parsed as `'a => (unit => 'a)` what would make it invariant. Please check how it parsers and if it parses wrong then create issue to fix it. Also add parens so it is clear that it's `('a => unit) => 'a`

zxq9 commented

2022-05-26 01:56:22 +09:00

(Migrated from gitlab.com)

Created by: radrow

Or is it supposed to be invariant?

*Created by: radrow* Or is it supposed to be invariant?

zxq9 commented

2022-05-26 01:56:38 +09:00

(Migrated from gitlab.com)

Created by: radrow

Same as above. Add parens.

*Created by: radrow* Same as above. Add parens.

zxq9 commented

2022-05-26 02:03:49 +09:00

(Migrated from gitlab.com)

Created by: radrow

In Haskell both 'a and 'b would be contra if you write it this way

*Created by: radrow* In Haskell both 'a and 'b would be contra if you write it this way

zxq9 commented

2022-05-26 03:07:22 +09:00

(Migrated from gitlab.com)

Created by: radrow

write explicit types as I believe both DT_BIV would default args to units which is not what you test I guess.

*Created by: radrow* write explicit types as I believe both `DT_BIV` would default args to units which is not what you test I guess.

zxq9 commented

2022-05-26 03:13:50 +09:00

(Migrated from gitlab.com)

Created by: radrow

should pass

*Created by: radrow* should pass

zxq9 commented

2022-05-26 03:14:16 +09:00

(Migrated from gitlab.com)

Created by: radrow

should pass

*Created by: radrow* should pass

zxq9 commented

2022-05-26 03:15:20 +09:00

(Migrated from gitlab.com)

Created by: radrow

What does the rvalue type to? dt_co_twice(Animal)?

*Created by: radrow* What does the rvalue type to? `dt_co_twice(Animal)`?

zxq9 commented

2022-05-26 03:15:40 +09:00

(Migrated from gitlab.com)

Created by: radrow

But it should fail, just curious what's going on

*Created by: radrow* But it should fail, just curious what's going on

zxq9 commented

2022-05-26 03:26:44 +09:00

(Migrated from gitlab.com)

Created by: radrow

I would also like to see the following scenario with some basic checks:

record xy('a) = {x : 'a, y : 'a}

let c = Chain.create() : Cat
let a : Animal = c

let _ : xy(Animal) = {x = c, y = c} // success
let _ : xy(Animal) = {x = c, y = a} // ???
let _ : xy(Animal) = {x = a, y = c} // ???
let _ : xy(Animal) = {x = a, y = a} // success
let _ : xy(Cat) = {x = c, y = c} // success
let _ : xy(Cat) = {x = c, y = a} // fail
let _ : xy(Cat) = {x = a, y = c} // fail
let _ : xy(Cat) = {x = a, y = a} // fail

*Created by: radrow* I would also like to see the following scenario with some basic checks: ``` record xy('a) = {x : 'a, y : 'a} let c = Chain.create() : Cat let a : Animal = c let _ : xy(Animal) = {x = c, y = c} // success let _ : xy(Animal) = {x = c, y = a} // ??? let _ : xy(Animal) = {x = a, y = c} // ??? let _ : xy(Animal) = {x = a, y = a} // success let _ : xy(Cat) = {x = c, y = c} // success let _ : xy(Cat) = {x = c, y = a} // fail let _ : xy(Cat) = {x = a, y = c} // fail let _ : xy(Cat) = {x = a, y = a} // fail ```

zxq9 commented

2022-05-26 03:27:48 +09:00

(Migrated from gitlab.com)

Created by: radrow

The trick is that the last 3 rvalues must not be inferred to be Cat. It should be either Animal or a type error

*Created by: radrow* The trick is that the last 3 rvalues must not be inferred to be `Cat`. It should be either `Animal` or a type error

zxq9 commented

2022-06-14 06:07:49 +09:00

(Migrated from gitlab.com)

Created by: radrow

Review: Approved

*Created by: radrow* **Review:** Approved

zxq9 commented

2022-06-14 06:09:58 +09:00

(Migrated from gitlab.com)

Created by: radrow

It's not perfect, but it's usable. We should consider improvements in the inference, but what is important now is:

System is correct (no barking cats)
Whenever type inference fails, an explicit type annotation should solve the problem

*Created by: radrow* It's not perfect, but it's usable. We should consider improvements in the inference, but what is important now is: - System is correct (no barking cats) - Whenever type inference fails, an explicit type annotation should solve the problem

zxq9 commented

2022-06-17 17:39:21 +09:00

(Migrated from gitlab.com)

Created by: hanssv

Review: Approved

Looks ok to me! Please squash before merging 😅

*Created by: hanssv* **Review:** Approved Looks ok to me! Please squash before merging 😅

zxq9 commented

2022-06-17 18:09:07 +09:00

(Migrated from gitlab.com)

Merged by: ghallak at 2022-06-17 09:09:07 UTC

*Merged by: ghallak at 2022-06-17 09:09:07 UTC*

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: QPQ-AG/sophia#848