leostera / caramel

:candy: a functional language for building type-safe, scalable, and maintainable applications
https://caramel.run
Apache License 2.0
1.06k stars 25 forks source link

Verify inferred typedtree is consistent with the original typedtree #31

Closed leostera closed 4 years ago

leostera commented 4 years ago

One we can parse in the entire Erlang AST that we can generate from caramelc, the translation should end up in an OCaml Parsetree that we can typecheck successfully.

Even if we do typecheck correctly, we need to make sure that the inferred types are isomorphic to the source types used to generate the Erlang code to begin with.

So that the following identity law holds: types_of(parse(compile(ml))) = types_of(ml).

This may be doable at the source level as well.

As an example of the flow:

(* compile 2 modules *)
$ caramelc compile a.ml b.ml

(* perform an obviously wrong verification *)
$ caramelc verify a.erl b.ml
ERROR: inconsistent modules

(* perform a verification that should work *)
$ caramelc verify a.erl a.ml
OK

I need to do some thinking here, but this should be the intended flow.

leostera commented 4 years ago

After a chat with @Drup on the OCaml discord, it seems that a plausible way of doing this is to compare the Parsetree instead, since the Typedtree isn't quite a tree, and it has cycles through type references, making if implausible to do a straightforward comparison.

So I'm closing this, since the method is there, we just need to start testing it and get it to cover the entire Parsetree successfully.