nachivpn / mt Goto Github PK

Clause unification uses "pairwiseChunk" - this is ridiculous - and leads to an error. for example this will pass the type checker:

foo() -> 1.0;
foo() -> 1.0;
foo() -> true;
foo() -> false.

Instead, it should make a "chain" of unification constraints..

Currently, this program is rejected although it is semantically valid:

x() -> 
    if
      true -> X = 1;
      false -> X = 3
    end,
    X.    %%line 24

with error:

test.erl: error in parse transform 'etc': {"Type Error: 'X' not bound on line 24

Currently the A is funt (A,B) -> {funt, A, B} is a parameter for one type, this needs to be changed to a list of types

Currently function types look like Haskell types, they need to look like "Erlang types"! That is: (a,b) -> a instead of a -> (b -> c)

Requires implementation of (basic) type classes. Being able to type expressions like int + float depends on this.

Example:

-type tree(A) :: nil | {node, A, tree(A), tree(A)}.

Types of

foo11(N) -> N = 3, foo12(N).
foo12(N) -> N.

are:

foo11 :: (integer)->integer
foo12 :: (integer)->integer

Moreover, this causes a type error (!) :

foo10(N) -> N = 3, foo12(N).
foo11(N) -> N = "", foo12(N).
foo12(N) -> N.

Make prettify return a string. This would be easier to format etc.

Do a pre-pass and assign a fresh type to each function in the environment before attempting to infer the types of each function

Currently, X=3 overshadows an X in scope. Instead, it should unify both the types if in scope, and extend environment otherwise.

This requires adding line numbers to constraint tuples

already implemented by c438e15, but needs testing..

Implement union of predicates instead of ++

Let the unifier continue unification in spite of failing to unify a constraint, and collect the problematic constraints separately. Printing the errors with "relevant bindings" and solved types (to the extent possible) could lead to a lot more readable errors.

Inferred type of lets(x,app(idterm(y),int(5)),X) is A !!

Trace:

Type of y = {tvar,#Ref<0.1275695646.2152202243.105277>}
Fresh Type of y = {tvar,#Ref<0.1275695646.2152202243.105277>}
App Type1 = {funt,[{tvar,#Ref<0.1275695646.2152202243.105277>}],
                  {tvar,#Ref<0.1275695646.2152202243.105277>}}
 Constraints1 = []
App Type2 = {bt,int}
 Constraints2 = []
LETX Type1 = {tvar,#Ref<0.1275695646.2152202243.105280>}
 Constraints1 = [{{funt,[{tvar,#Ref<0.1275695646.2152202243.105277>}],
                        {tvar,#Ref<0.1275695646.2152202243.105277>}},
                  {funt,[{bt,int}],
                        {tvar,#Ref<0.1275695646.2152202243.105280>}}}]
----------Env = []
Type of x = {forall,{tvar,#Ref<0.1275695646.2152202243.105280>},
                    {tvar,#Ref<0.1275695646.2152202243.105280>}}
Fresh Type of x = {tvar,#Ref<0.1275695646.2152202243.105286>}
LETX Type2 = {tvar,#Ref<0.1275695646.2152202243.105286>}
 Constraints2= []
A
Generated constraints are:
(B)->B :==: (int)->C
Inferred type: A