From a100d11edd23373311bf353a25200ce6b6a17a2c Mon Sep 17 00:00:00 2001 From: Peter Date: Tue, 8 Feb 2022 15:17:47 +0100 Subject: [PATCH 01/18] better testing for terms --- eyg/bin/run-tests.js | 2 +- eyg/src/eyg/ast/expression.gleam | 8 + eyg/src/eyg/typer.gleam | 2 +- eyg/test/eyg/functions_test.gleam | 21 -- eyg/test/eyg/terms_test.gleam | 324 ++++++++++++++++++++++-------- 5 files changed, 249 insertions(+), 108 deletions(-) diff --git a/eyg/bin/run-tests.js b/eyg/bin/run-tests.js index 8abe37a84..d80e5c384 100644 --- a/eyg/bin/run-tests.js +++ b/eyg/bin/run-tests.js @@ -11,7 +11,7 @@ async function main() { let failures = 0; for await (let entry of await opendir(dir)) { - if (!entry.name.endsWith("test.js")) continue; + if (!entry.name.endsWith("terms_test.js")) continue; let path = "../" + dir + entry.name; process.stdout.write("\nlanguage/" + entry.name.slice(0, -3) + ":\n "); let module = await import(path); diff --git a/eyg/src/eyg/ast/expression.gleam b/eyg/src/eyg/ast/expression.gleam index ee35a34c8..f5674686f 100644 --- a/eyg/src/eyg/ast/expression.gleam +++ b/eyg/src/eyg/ast/expression.gleam @@ -192,3 +192,11 @@ pub fn tuple_(elements) { pub fn variable(label) { #(dynamic.from(Nil), Variable(label)) } + +pub fn row(fields) { + #(dynamic.from(Nil), Row(fields)) +} + +pub fn hole() { + #(dynamic.from(Nil), Hole) +} diff --git a/eyg/src/eyg/typer.gleam b/eyg/src/eyg/typer.gleam index 493802327..a7d2ac548 100644 --- a/eyg/src/eyg/typer.gleam +++ b/eyg/src/eyg/typer.gleam @@ -18,7 +18,7 @@ pub type Reason(n) { UnknownVariable(label: String) UnmatchedTypes(expected: t.Monotype(n), given: t.Monotype(n)) MissingFields(expected: List(#(String, t.Monotype(n)))) - UnexpectedFields(expected: List(#(String, t.Monotype(n)))) + UnexpectedFields(unexpected: List(#(String, t.Monotype(n)))) UnableToProvide(expected: t.Monotype(n), generator: e.Generator) } diff --git a/eyg/test/eyg/functions_test.gleam b/eyg/test/eyg/functions_test.gleam index f9650317d..beed21a6d 100644 --- a/eyg/test/eyg/functions_test.gleam +++ b/eyg/test/eyg/functions_test.gleam @@ -9,27 +9,6 @@ import eyg/typer/monotype as t import eyg/typer/monotype.{resolve} import eyg/typer/polytype -pub fn type_bound_function_test() { - let typer = init(fn(_) { todo }) - let scope = typer.root_scope([]) - let untyped = ast.function(p.Tuple([]), ast.binary("")) - let #(typed, typer) = infer(untyped, t.Unbound(-1), #(typer, scope)) - let typer.Typer(substitutions: substitutions, ..) = typer - let Ok(type_) = get_type(typed) - let t.Function(t.Tuple([]), t.Binary) = resolve(type_, substitutions) -} - -pub fn generic_function_test() { - let typer = init(fn(_) { todo }) - let scope = typer.root_scope([]) - let untyped = ast.function(p.Variable("x"), ast.variable("x")) - let #(typed, typer) = infer(untyped, t.Unbound(-1), #(typer, scope)) - let typer.Typer(substitutions: substitutions, ..) = typer - let Ok(type_) = get_type(typed) - let t.Function(t.Unbound(a), t.Unbound(b)) = resolve(type_, substitutions) - let True = a == b -} - pub fn call_function_test() { let typer = init(fn(_) { todo }) let scope = typer.root_scope([]) diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index 42f3d9461..3002b3c32 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -1,113 +1,267 @@ import gleam/io -import gleam/option.{None} +import gleam/option.{None, Some} import eyg import eyg/ast -import eyg/ast/expression -import eyg/typer.{get_type, infer, init} +import eyg/ast/editor +import eyg/ast/expression.{binary, call, function, hole, row, tuple_, variable} +import eyg/typer import eyg/typer/monotype as t +import eyg/ast/pattern as p import eyg/typer/polytype -pub fn expected_binary_test() { - let typer = init(fn(_) { todo }) - let scope = typer.root_scope([]) - let state = #(typer, scope) - let untyped = ast.binary("Hello") - let #(typed, _typer) = infer(untyped, t.Binary, state) - assert Ok(t.Binary) = get_type(typed) +// builder pattern for adding variables in test where this would be helpful +pub fn infer(untyped, type_) { + let native_to_string = fn(_: Nil) { "" } + let variables = [#("equal", typer.equal_fn())] + let checker = typer.init(native_to_string) + let scope = typer.root_scope(variables) + let state = #(checker, scope) + // TODO replace all variables + // + // sdo + typer.infer(untyped, type_, state) } -pub fn unexpected_binary_error_test() { - let typer = init(fn(_) { todo }) - let scope = typer.root_scope([]) - let state = #(typer, scope) - let untyped = ast.binary("Hello") - let #(typed, _typer) = infer(untyped, t.Tuple([]), state) - assert Error(reason) = get_type(typed) - assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason +fn unbound() { + t.Unbound(-1) +} + +fn get_type(typed, checker: typer.Typer(a)) { + try type_ = typer.get_type(typed) + let resolved = t.resolve(type_, checker.substitutions) + Ok(resolved) } -pub fn expected_empty_tuple_test() { - let typer = init(fn(_) { todo }) - let scope = typer.root_scope([]) - let state = #(typer, scope) - let untyped = ast.tuple_([]) - let #(typed, _typer) = infer(untyped, t.Tuple([]), state) - assert Ok(t.Tuple([])) = get_type(typed) +// TODO move to AST +fn get_expression(tree, path) { + let editor.Expression(expression) = editor.get_element(tree, path) + Ok(expression) } -pub fn expected_non_empty_tuple_test() { - let typer = init(fn(_) { todo }) - let scope = typer.root_scope([]) - let state = #(typer, scope) - let untyped = ast.tuple_([ast.tuple_([])]) - let #(typed, _typer) = infer(untyped, t.Tuple([t.Tuple([])]), state) - assert Ok(t.Tuple([t.Tuple([])])) = get_type(typed) +pub fn binary_expression_test() { + let source = binary("Hello") + let #(typed, checker) = infer(source, unbound()) + assert Ok(t.Binary) = get_type(typed, checker) + + let #(typed, checker) = infer(source, t.Binary) + assert Ok(t.Binary) = get_type(typed, checker) + + let #(typed, checker) = infer(source, t.Tuple([])) + assert Error(reason) = get_type(typed, checker) + assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason } -pub fn unexpected_tuple_size_test() { - let typer = init(fn(_) { todo }) - let scope = typer.root_scope([]) - let state = #(typer, scope) - let untyped = ast.tuple_([ast.binary("not needed")]) - let #(typed, _typer) = infer(untyped, t.Tuple([]), state) - assert Error(reason) = get_type(typed) +pub fn tuple_expression_test() { + let source = tuple_([binary("Hello")]) + let #(typed, checker) = infer(source, unbound()) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([t.Binary]) = type_ + + let #(typed, checker) = infer(source, t.Tuple([unbound()])) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([t.Binary]) = type_ + + let #(typed, checker) = infer(source, t.Tuple([t.Binary])) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([t.Binary]) = type_ + + let #(typed, checker) = infer(source, t.Tuple([])) + assert Error(reason) = get_type(typed, checker) assert typer.IncorrectArity(0, 1) = reason + + let #(typed, checker) = infer(source, t.Tuple([t.Tuple([])])) + // Type is correct here only internally is there a failure + assert Ok(t.Tuple([t.Tuple([])])) = get_type(typed, checker) + assert Ok(element) = get_expression(typed, [0]) + assert Error(reason) = get_type(element, checker) + assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason +} + +// TODO merge hole +pub fn pair_test() { + let source = tuple_([binary("Hello"), tuple_([])]) + + let tx = t.Unbound(-1) + let ty = t.Unbound(-2) + let #(typed, checker) = infer(source, t.Tuple([tx, ty])) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([t.Binary, t.Tuple([])]) = type_ + + // could check tx/ty bound properly + let #(typed, checker) = infer(source, t.Tuple([tx, tx])) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([t.Binary, t.Binary]) = type_ + assert Ok(element) = get_expression(typed, [1]) + assert Error(reason) = get_type(element, checker) + assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason } -pub fn unexpected_tuple_element_type_test() { - let typer = init(fn(_) { todo }) - let scope = typer.root_scope([]) - let state = #(typer, scope) - let untyped = ast.tuple_([ast.binary("Yo")]) - let #(typed, _typer) = infer(untyped, t.Tuple([t.Tuple([])]), state) - assert Ok(t.Tuple([t.Tuple([])])) = get_type(typed) - assert #(_context, expression.Tuple([child])) = typed - assert Error(reason) = get_type(child) +pub fn row_expression_test() { + // TODO order when row is called + let source = row([#("foo", binary("Hello"))]) + + let #(typed, checker) = infer(source, unbound()) + assert Ok(type_) = get_type(typed, checker) + assert t.Row([#("foo", t.Binary)], None) = type_ + + let #(typed, checker) = infer(source, t.Row([#("foo", t.Binary)], None)) + assert Ok(type_) = get_type(typed, checker) + assert t.Row([#("foo", t.Binary)], None) = type_ + + // TODO row with some + let #(typed, checker) = + infer(source, t.Row([#("foo", t.Binary), #("bar", t.Binary)], None)) + assert Error(reason) = get_type(typed, checker) + assert typer.MissingFields([#("bar", t.Binary)]) = reason + + let #(typed, checker) = infer(source, t.Row([], None)) + assert Error(reason) = get_type(typed, checker) + + // TODO resolve types in errors too + // assert typer.UnexpectedFields([#("foo", t.Binary)]) = reason + let #(typed, checker) = infer(source, t.Row([#("foo", t.Tuple([]))], None)) + assert Ok(type_) = get_type(typed, checker) + assert t.Row([#("foo", t.Tuple([]))], None) = type_ + assert Ok(element) = get_expression(typed, [0, 1]) + assert Error(reason) = get_type(element, checker) assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason + + // T.Row(head, option(more_row)) + // Means no such thing as an empty record. Good because tuple is unit + let #(typed, checker) = infer(source, t.Row([#("foo", t.Binary)], Some(-1))) + assert Ok(type_) = get_type(typed, checker) + // TODO should resolve to none + // assert t.Row([#("foo", t.Binary)], None) = type_ +} + +// TODO tag test +// TODO patterns +pub fn var_expression_test() { + let source = variable("x") + + let #(typed, checker) = infer(source, unbound()) + assert Error(reason) = get_type(typed, checker) + // TODO check we're on the lowest unbound integer + assert typer.UnknownVariable("x") = reason } -pub fn expected_row_test() { - let typer = init(fn(_) { todo }) - let scope = typer.root_scope([]) - let state = #(typer, scope) - let untyped = ast.row([#("foo", ast.tuple_([]))]) - let #(typed, _typer) = - infer(untyped, t.Row([#("foo", t.Tuple([]))], None), state) - assert Ok(t.Row([#("foo", t.Tuple([]))], None)) = get_type(typed) +pub fn function_test() { + let source = function(p.Variable(""), binary("")) + + let #(typed, checker) = infer(source, unbound()) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Unbound(_), t.Binary) = type_ + + let #(typed, checker) = infer(source, t.Function(unbound(), t.Unbound(-2))) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Unbound(_), t.Binary) = type_ + + let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Binary)) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Tuple([]), t.Binary) = type_ + + let #(typed, checker) = infer(source, t.Function(unbound(), unbound())) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Binary, t.Binary) = type_ + + let #(typed, checker) = infer(source, t.Binary) + assert Error(reason) = get_type(typed, checker) + + // TODO resolve errors + // assert typer.UnmatchedTypes(t.Binary, t.Function(t.Unbound(_), t.Tuple([]))) = + // reason + let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Tuple([]))) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Tuple([]), t.Tuple([])) = type_ + assert Ok(body) = get_expression(typed, [1]) + assert Error(reason) = get_type(body, checker) + assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason } -pub fn unexpected_fields_test() { - let typer = init(fn(_) { todo }) - let scope = typer.root_scope([]) - let state = #(typer, scope) - let untyped = ast.row([#("foo", ast.tuple_([]))]) - let #(typed, _typer) = infer(untyped, t.Row([], None), state) - assert Error(reason) = get_type(typed) - assert typer.UnexpectedFields([#("foo", x)]) = reason - // x is unbound but we probably have better info +pub fn id_function_test() { + let source = function(p.Variable("x"), variable("x")) + + let #(typed, checker) = infer(source, unbound()) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Unbound(i), t.Unbound(j)) = type_ + assert True = i == j + + let #(typed, checker) = infer(source, t.Function(unbound(), t.Binary)) + assert Ok(type_) = get_type(typed, checker) + // TODO check unbound is now binary + assert t.Function(t.Binary, t.Binary) = type_ + + let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Binary)) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Tuple([]), t.Binary) = type_ + assert Ok(body) = get_expression(typed, [1]) + assert Error(reason) = get_type(body, checker) + assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason + // Not this is saying that the variable is wrong some how } -pub fn missing_fields_test() { - let typer = init(fn(_) { todo }) - let scope = typer.root_scope([]) - let state = #(typer, scope) - let untyped = ast.row([]) - let #(typed, _typer) = - infer(untyped, t.Row([#("foo", t.Tuple([]))], None), state) - assert Error(reason) = get_type(typed) - assert typer.MissingFields([#("foo", x)]) = reason - // I think we might only need the name not type, BUT why throw away info +// equal bin bin +// equal bin tuple still returns true +pub fn call_function_test() { + let func = function(p.Tuple([]), binary("")) + let source = call(func, tuple_([])) + + let #(typed, checker) = infer(source, unbound()) + assert Ok(type_) = get_type(typed, checker) + assert t.Binary = type_ + + let #(typed, checker) = infer(source, t.Binary) + assert Ok(type_) = get_type(typed, checker) + assert t.Binary = type_ + // Error is internal + // let #(typed, checker) = infer(source, t.Tuple([])) + // assert Error(reason) = get_type(typed, checker) + // assert typer.UnmatchedTypes(t.Tuple([]), t.Tuple([])) = reason } -pub fn unexpected_field_type_test() { - let typer = init(fn(_) { todo }) - let scope = typer.root_scope([]) - let state = #(typer, scope) - let untyped = ast.row([#("foo", ast.tuple_([]))]) - let #(typed, _typer) = - infer(untyped, t.Row([#("foo", t.Binary)], None), state) - assert Ok(t.Row([#("foo", t.Binary)], None)) = get_type(typed) - assert #(_context, expression.Row([#("foo", child)])) = typed - assert Error(reason) = get_type(child) +pub fn call_generic_function_test() { + let func = function(p.Variable("x"), variable("x")) + let source = call(func, tuple_([])) + + let #(typed, checker) = infer(source, unbound()) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([]) = type_ + + let #(typed, checker) = infer(source, t.Tuple([])) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([]) = type_ + + // error in generic pushed to arguments + let #(typed, checker) = infer(source, t.Binary) + assert Ok(type_) = get_type(typed, checker) + assert t.Binary = type_ + assert Ok(body) = get_expression(typed, [1]) + assert Error(reason) = get_type(body, checker) assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason } + +pub fn call_not_a_function_test() { + let source = call(binary("no a func"), tuple_([])) + + let #(typed, checker) = infer(source, t.Binary) + assert Ok(type_) = get_type(typed, checker) + assert t.Binary = type_ + assert Ok(body) = get_expression(typed, [0]) + assert Error(reason) = get_type(body, checker) + assert typer.UnmatchedTypes(expected, t.Binary) = reason + // TODO resolve expected + // assert t.Function(t.Tuple([]), t.Binary) = expected +} + +pub fn hole_expression_test() { + let source = hole() + + let #(typed, checker) = infer(source, unbound()) + assert Ok(type_) = get_type(typed, checker) + // TODO check we're on the lowest unbound integer + assert t.Unbound(_) = type_ + + let #(typed, checker) = infer(source, t.Binary) + assert Ok(type_) = get_type(typed, checker) + assert t.Binary = type_ +} From 2bd4af631f478c485fc62fa990ebf4ad08508d96 Mon Sep 17 00:00:00 2001 From: Peter Date: Tue, 8 Feb 2022 22:08:43 +0100 Subject: [PATCH 02/18] big recursion spike --- eyg/src/eyg/typer.gleam | 100 +++++++++-------- eyg/src/eyg/typer/monotype.gleam | 17 ++- eyg/src/eyg/typer/polytype.gleam | 6 + eyg/test/eyg/patterns_test.gleam | 101 ----------------- eyg/test/eyg/terms_test.gleam | 182 +++++++++++++++++++++++++++++-- 5 files changed, 243 insertions(+), 163 deletions(-) diff --git a/eyg/src/eyg/typer.gleam b/eyg/src/eyg/typer.gleam index a7d2ac548..ac5835443 100644 --- a/eyg/src/eyg/typer.gleam +++ b/eyg/src/eyg/typer.gleam @@ -168,7 +168,7 @@ pub fn next_unbound(typer) { } // monotype function?? -// This will need the checker/unification/constraints data structure as it uses subsitutions and updates the next var value +// This will need the checker/unification/constraints data structure as it uses substitutions and updates the next var value // next unbound inside mono can be integer and unbound(i) outside pub fn unify(expected, given, state) { // Pass as tuple to make reduce functions easier to implement @@ -178,65 +178,63 @@ pub fn unify(expected, given, state) { let expected = t.resolve(expected, substitutions) let given = t.resolve(given, substitutions) - case occurs_in(expected, given) || occurs_in(given, expected) { - True -> Ok(typer) - False -> - case expected, given { - t.Native(e), t.Native(g) if e == g -> Ok(typer) - t.Native(_), t.Native(_) -> - // The typer is passed because some constrains should end up in typer i.e. if some values in Tuple are Ok - Error(#(UnmatchedTypes(expected, given), typer)) - t.Binary, t.Binary -> Ok(typer) - t.Tuple(expected), t.Tuple(given) -> - case list.zip(expected, given) { - Error(#(expected, given)) -> - Error(#(IncorrectArity(expected, given), typer)) - Ok(pairs) -> - list.try_fold( - pairs, - typer, - fn(pair, typer) { - let #(expected, given) = pair - unify(expected, given, #(typer, scope)) - }, - ) - } - t.Unbound(i), any -> Ok(add_substitution(i, any, typer)) - any, t.Unbound(i) -> Ok(add_substitution(i, any, typer)) - t.Row(expected, expected_extra), t.Row(given, given_extra) -> { - let #(expected, given, shared) = group_shared(expected, given) - let #(x, typer) = next_unbound(typer) - try typer = case given, expected_extra { - [], _ -> Ok(typer) - only, Some(i) -> - Ok(add_substitution(i, t.Row(only, Some(x)), typer)) - only, None -> Error(#(UnexpectedFields(only), typer)) - } - try typer = case expected, given_extra { - [], _ -> Ok(typer) - only, Some(i) -> - Ok(add_substitution(i, t.Row(only, Some(x)), typer)) - only, None -> Error(#(MissingFields(only), typer)) - } + // case occurs_in(expected, given) || occurs_in(given, expected) { + // // True -> todo("handle_occurs") + // _ -> + case expected, given { + t.Native(e), t.Native(g) if e == g -> Ok(typer) + t.Native(_), t.Native(_) -> + // The typer is passed because some constrains should end up in typer i.e. if some values in Tuple are Ok + Error(#(UnmatchedTypes(expected, given), typer)) + t.Binary, t.Binary -> Ok(typer) + t.Tuple(expected), t.Tuple(given) -> + case list.zip(expected, given) { + Error(#(expected, given)) -> + Error(#(IncorrectArity(expected, given), typer)) + Ok(pairs) -> list.try_fold( - shared, + pairs, typer, fn(pair, typer) { let #(expected, given) = pair unify(expected, given, #(typer, scope)) }, ) - } - t.Function(expected_from, expected_return), t.Function( - given_from, - given_return, - ) -> { - try x = unify(expected_from, given_from, state) - unify(expected_return, given_return, #(x, scope)) - } - expected, given -> Error(#(UnmatchedTypes(expected, given), typer)) } + t.Unbound(i), any -> Ok(add_substitution(i, any, typer)) + any, t.Unbound(i) -> Ok(add_substitution(i, any, typer)) + t.Row(expected, expected_extra), t.Row(given, given_extra) -> { + let #(expected, given, shared) = group_shared(expected, given) + let #(x, typer) = next_unbound(typer) + try typer = case given, expected_extra { + [], _ -> Ok(typer) + only, Some(i) -> Ok(add_substitution(i, t.Row(only, Some(x)), typer)) + only, None -> Error(#(UnexpectedFields(only), typer)) + } + try typer = case expected, given_extra { + [], _ -> Ok(typer) + only, Some(i) -> Ok(add_substitution(i, t.Row(only, Some(x)), typer)) + only, None -> Error(#(MissingFields(only), typer)) + } + list.try_fold( + shared, + typer, + fn(pair, typer) { + let #(expected, given) = pair + unify(expected, given, #(typer, scope)) + }, + ) + } + t.Function(expected_from, expected_return), t.Function( + given_from, + given_return, + ) -> { + try x = unify(expected_from, given_from, state) + unify(expected_return, given_return, #(x, scope)) + } + expected, given -> Error(#(UnmatchedTypes(expected, given), typer)) } + // } } fn group_shared(left, right) { diff --git a/eyg/src/eyg/typer/monotype.gleam b/eyg/src/eyg/typer/monotype.gleam index cf044696b..7256f013b 100644 --- a/eyg/src/eyg/typer/monotype.gleam +++ b/eyg/src/eyg/typer/monotype.gleam @@ -11,6 +11,7 @@ pub type Monotype(n) { Row(fields: List(#(String, Monotype(n))), extra: Option(Int)) Function(from: Monotype(n), to: Monotype(n)) Unbound(i: Int) + Recursive(i: Int, type_: Monotype(n)) } fn row_to_string(row, native_to_string) { @@ -114,6 +115,7 @@ pub fn literal(monotype) { fn do_occurs_in(i, b) { case b { + Recursive(j, inner) -> do_occurs_in(i, inner) Unbound(j) if i == j -> True Unbound(_) -> False Native(_) -> False @@ -142,15 +144,22 @@ fn occurs_in(a, b) { pub fn resolve(type_, substitutions) { case type_ { + Recursive(i, inner) -> Recursive(i, inner) Unbound(i) -> case list.key_find(substitutions, i) { Ok(Unbound(j)) if i == j -> type_ Error(Nil) -> type_ - Ok(substitution) -> { - let False = occurs_in(Unbound(i), substitution) - resolve(substitution, substitutions) - } + Ok(substitution) -> + case occurs_in(Unbound(i), substitution) { + False -> resolve(substitution, substitutions) + True -> { + io.debug("====================") + io.debug(substitution) + Recursive(i, substitution) + } + } } + // let False = Native(name) -> Native(name) Binary -> Binary Tuple(elements) -> { diff --git a/eyg/src/eyg/typer/polytype.gleam b/eyg/src/eyg/typer/polytype.gleam index 857e10fd5..a662c88a8 100644 --- a/eyg/src/eyg/typer/polytype.gleam +++ b/eyg/src/eyg/typer/polytype.gleam @@ -51,6 +51,11 @@ pub fn replace_variable(monotype, x, y) { True -> t.Unbound(y) False -> t.Unbound(i) } + t.Recursive(i, inner) -> + case i == x { + True -> t.Recursive(y, inner) + False -> t.Recursive(i, inner) + } } } @@ -116,6 +121,7 @@ fn free_variables_in_monotype(monotype) { t.Function(from, to) -> union(free_variables_in_monotype(from), free_variables_in_monotype(to)) t.Unbound(i) -> [i] + t.Recursive(_, inner) -> free_variables_in_monotype(inner) } } diff --git a/eyg/test/eyg/patterns_test.gleam b/eyg/test/eyg/patterns_test.gleam index 342acb94e..323c5b169 100644 --- a/eyg/test/eyg/patterns_test.gleam +++ b/eyg/test/eyg/patterns_test.gleam @@ -9,107 +9,6 @@ import eyg/typer/monotype as t import eyg/typer/polytype import platform/browser -// This is proablbly better called assignment tests, unless it grows too big and patterns should be separate -pub fn variable_of_expected_type_test() { - let typer = typer.init(browser.native_to_string) - let scope = - typer.Scope( - variables: [#("foo", polytype.Polytype([], t.Tuple([])))], - path: [], - ) - let untyped = ast.variable("foo") - assert #(typed, _typer) = infer(untyped, t.Tuple([]), #(typer, scope)) - assert Ok(t.Tuple([])) = get_type(typed) -} - -pub fn variable_of_unexpected_type_test() { - let typer = typer.init(browser.native_to_string) - let scope = typer.root_scope([#("foo", polytype.Polytype([], t.Tuple([])))]) - let state = #(typer, scope) - let untyped = ast.variable("foo") - assert #(typed, _typer) = infer(untyped, t.Binary, state) - assert Error(reason) = get_type(typed) - assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason -} - -pub fn missing_variable_test() { - let typer = typer.init(browser.native_to_string) - let scope = typer.root_scope([]) - let state = #(typer, scope) - let untyped = ast.variable("foo") - let #(typed, _state) = infer(untyped, t.Binary, state) - let Error(reason) = get_type(typed) - assert typer.UnknownVariable("foo") = reason -} - -// assignment -pub fn expected_assignment_test() { - let typer = typer.init(browser.native_to_string) - let scope = typer.root_scope([]) - let state = #(typer, scope) - let untyped = - ast.let_(pattern.Variable("foo"), ast.tuple_([]), ast.variable("foo")) - let #(typed, _typer) = infer(untyped, t.Tuple([]), state) - assert Ok(t.Tuple([])) = get_type(typed) -} - -pub fn unexpected_then_type_test() { - let typer = typer.init(browser.native_to_string) - let scope = typer.root_scope([]) - let state = #(typer, scope) - let untyped = - ast.let_(pattern.Variable("foo"), ast.binary("wrong"), ast.variable("foo")) - let #(typed, _typer) = infer(untyped, t.Tuple([]), state) - // Should the error be on the inner - assert Ok(t.Tuple([])) = get_type(typed) - assert #(_context, expression.Let(_pattern, _value, then)) = typed - assert Error(reason) = get_type(then) - assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason -} - -pub fn matched_expected_tuple_test() { - let typer = typer.init(browser.native_to_string) - let scope = - typer.root_scope([#("foo", polytype.Polytype([], t.Tuple([t.Binary])))]) - let state = #(typer, scope) - let untyped = - ast.let_(pattern.Tuple(["a"]), ast.variable("foo"), ast.variable("a")) - let #(typed, typer) = infer(untyped, t.Binary, state) - let Ok(t.Binary) = get_type(typed) - assert #(_context, expression.Let(_pattern, value, _then)) = typed - let typer.Typer(substitutions: substitutions, ..) = typer - let Ok(type_) = get_type(value) - let t.Tuple([t.Binary]) = t.resolve(type_, substitutions) -} - -pub fn expected_a_tuple_test() { - let typer = typer.init(browser.native_to_string) - let scope = typer.root_scope([#("foo", polytype.Polytype([], t.Binary))]) - let state = #(typer, scope) - - let untyped = - ast.let_(pattern.Tuple(["a"]), ast.variable("foo"), ast.variable("a")) - let #(typed, _state) = infer(untyped, t.Binary, state) - let Ok(t.Binary) = get_type(typed) - assert #(_context, expression.Let(_pattern, value, _then)) = typed - let Error(reason) = get_type(value) - let typer.UnmatchedTypes(t.Tuple([_]), t.Binary) = reason -} - -pub fn unexpected_tuple_size_test() { - let typer = typer.init(browser.native_to_string) - let scope = typer.root_scope([#("foo", polytype.Polytype([], t.Tuple([])))]) - let state = #(typer, scope) - - let untyped = - ast.let_(pattern.Tuple(["a"]), ast.variable("foo"), ast.variable("a")) - let #(typed, _state) = infer(untyped, t.Binary, state) - let Ok(t.Binary) = get_type(typed) - assert #(_context, expression.Let(_pattern, value, _then)) = typed - let Error(reason) = get_type(value) - let typer.IncorrectArity(1, 0) = reason -} - pub fn matched_expected_row_test() { let scope = typer.root_scope([ diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index 3002b3c32..bc964dbfb 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -1,10 +1,14 @@ import gleam/io +import gleam/list import gleam/option.{None, Some} import eyg import eyg/ast import eyg/ast/editor -import eyg/ast/expression.{binary, call, function, hole, row, tuple_, variable} +import eyg/ast/expression.{ + binary, call, function, hole, let_, row, tuple_, variable, +} import eyg/typer +import eyg/ast/expression as e import eyg/typer/monotype as t import eyg/ast/pattern as p import eyg/typer/polytype @@ -27,9 +31,18 @@ fn unbound() { } fn get_type(typed, checker: typer.Typer(a)) { - try type_ = typer.get_type(typed) - let resolved = t.resolve(type_, checker.substitutions) - Ok(resolved) + case typer.get_type(typed) { + Ok(type_) -> { + let resolved = t.resolve(type_, checker.substitutions) + Ok(resolved) + } + Error(typer.UnmatchedTypes(expected, given)) -> { + let expected = t.resolve(expected, checker.substitutions) + let given = t.resolve(given, checker.substitutions) + Error(typer.UnmatchedTypes(expected, given)) + } + Error(reason) -> Error(reason) + } } // TODO move to AST @@ -77,7 +90,6 @@ pub fn tuple_expression_test() { assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason } -// TODO merge hole pub fn pair_test() { let source = tuple_([binary("Hello"), tuple_([])]) @@ -117,8 +129,8 @@ pub fn row_expression_test() { let #(typed, checker) = infer(source, t.Row([], None)) assert Error(reason) = get_type(typed, checker) - // TODO resolve types in errors too // assert typer.UnexpectedFields([#("foo", t.Binary)]) = reason + // TODO move up let #(typed, checker) = infer(source, t.Row([#("foo", t.Tuple([]))], None)) assert Ok(type_) = get_type(typed, checker) assert t.Row([#("foo", t.Tuple([]))], None) = type_ @@ -167,9 +179,9 @@ pub fn function_test() { let #(typed, checker) = infer(source, t.Binary) assert Error(reason) = get_type(typed, checker) - // TODO resolve errors // assert typer.UnmatchedTypes(t.Binary, t.Function(t.Unbound(_), t.Tuple([]))) = // reason + // TODO move up let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Tuple([]))) assert Ok(type_) = get_type(typed, checker) assert t.Function(t.Tuple([]), t.Tuple([])) = type_ @@ -265,3 +277,159 @@ pub fn hole_expression_test() { assert Ok(type_) = get_type(typed, checker) assert t.Binary = type_ } + +// patterns +pub fn tuple_pattern_test() { + let source = function(p.Tuple(["x"]), variable("x")) + + let #(typed, checker) = infer(source, unbound()) + assert Ok(t.Function(from, _)) = get_type(typed, checker) + assert t.Tuple([t.Unbound(_)]) = from + + let #(typed, checker) = + infer(source, t.Function(t.Tuple([unbound()]), t.Unbound(-2))) + assert Ok(t.Function(from, _)) = get_type(typed, checker) + assert t.Tuple([t.Unbound(_)]) = from + + let #(typed, checker) = + infer(source, t.Function(t.Tuple([t.Binary]), t.Unbound(-2))) + assert Ok(t.Function(from, _)) = get_type(typed, checker) + assert t.Tuple([t.Binary]) = from + + // wrong arity + let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Unbound(-2))) + assert Error(reason) = get_type(typed, checker) + // TODO need to return the function error + assert typer.IncorrectArity(0, 1) = reason + + // wrong bound type + let #(typed, checker) = + infer(source, t.Function(t.Tuple([t.Binary]), t.Tuple([]))) + // Should this be an inside error or not + // assert Error(reason) = get_type(typed, checker) + // // TODO need to return the function error + // assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason +} + +// let +pub fn row_pattern_test() { + let source = function(p.Row([#("foo", "x")]), variable("x")) + // todo +} + +// TODO expanding row type test +// test reusing id +// pub fn recursive_tuple_test() { +// let source = +// let_( +// p.Variable("f"), +// function( +// p.Tuple([]), +// tuple_([binary("x"), call(variable("f"), tuple_([]))]), +// ), +// variable("f"), +// ) +// let #(typed, checker) = infer(source, unbound()) +// assert Ok(t.Function(from, to)) = get_type(typed, checker) +// assert t.Tuple([]) = from +// // assert t.Tuple([t.Binary, t.Unbound(mu)]) = to +// // typer.get_type(typed) +// // |> io.debug +// list.map(checker.substitutions, io.debug) +// // io.debug(mu) +// // io.debug("----") +// let [x, .._] = checker.substitutions +// let #(-1, t.Function(_, t.Tuple(elements))) = x +// io.debug(elements) +// let [_, t.Recursive(mu, inner)] = elements +// io.debug("loow ") +// io.debug(mu) +// io.debug(inner) +// let t.Tuple([_, t.Unbound(x)]) = inner +// io.debug(x) +// } +fn my_infer(untyped, goal) { + do_my_infer(untyped, goal, []) +} + +// Do this as alg J +fn do_my_infer(untyped, goal, env) { + let #(_, untyped) = untyped + io.debug(untyped) + case untyped { + e.Let(p.Variable(f), #(_, e.Function(p.Variable(x), body)), then) -> { + let p = t.Unbound(1) + let r = t.Unbound(2) + let env = [#(f, t.Function(p, r)), #(x, p), ..env] + do_my_infer(body, r, env) + } + e.Tuple([e1, e2]) -> { + // unify goal tuple(tnext 1) + let t1 = t.Unbound(3) + let t2 = t.Unbound(4) + io.debug("goal") + io.debug(goal) + do_my_infer(e1, t1, env) + do_my_infer(e2, t2, env) + } + e.Binary(_) -> { + io.debug("is binary") + io.debug(goal) + #(1, 1) + } + e.Call(e1, e2) -> { + io.debug(goal) + io.debug(e1) + io.debug(e2) + // 0 = 1 -> 2 + // 1 = Tuple([]) Null + // 2 = Tuple(3, 4) + // 3 = Binary + // 4 = 1 -> 2.1 + // 2 = Tuple(Binary, 2) + // rA(Binary, A) + // rA[Nil | Cons (B, A)] + // reverse: rA[Nil | Cons (B, A)] -> rA[Nil | Cons (B, A)] + // map: rA[Nil | Cons (B, A)] -> (B, C) -> rD[Nil | Cons (C, D)] +// map: List(B) -> (B -> C) -> List(C) + todo("in call") + } + e.Variable(label) -> { + let t = list.key_find(env, label) + io.debug(t) + todo + } + } + // #(1, 1) +} + +pub fn my_recursive_tuple_test() { + let source = + let_( + p.Variable("f"), + function( + p.Variable("x"), + tuple_([binary("hello"), call(variable("f"), tuple_([]))]), + ), + variable("f"), + ) + + let #(typed, checker) = my_infer(source, unbound()) + // assert Ok(t.Function(from, to)) = get_type(typed, checker) + // assert t.Tuple([]) = from + // // assert t.Tuple([t.Binary, t.Unbound(mu)]) = to + // // typer.get_type(typed) + // // |> io.debug + // list.map(checker.substitutions, io.debug) + // // io.debug(mu) + // // io.debug("----") + // let [x, .._] = checker.substitutions + // let #(-1, t.Function(_, t.Tuple(elements))) = x + // io.debug(elements) + // let [_, t.Recursive(mu, inner)] = elements + // io.debug("loow ") + // io.debug(mu) + // io.debug(inner) + // let t.Tuple([_, t.Unbound(x)]) = inner + // io.debug(x) +} From 884bcde218a815eec5f1a5c7d2fbb5893cc1be89 Mon Sep 17 00:00:00 2001 From: Peter Date: Wed, 9 Feb 2022 20:49:25 +0100 Subject: [PATCH 03/18] spike alg w --- eyg/src/eyg/inference.gleam | 119 ++++++ eyg/test/eyg/terms_test.gleam | 714 ++++++++++++++++------------------ 2 files changed, 460 insertions(+), 373 deletions(-) create mode 100644 eyg/src/eyg/inference.gleam diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam new file mode 100644 index 000000000..2c8f7e63b --- /dev/null +++ b/eyg/src/eyg/inference.gleam @@ -0,0 +1,119 @@ +import gleam/list +import eyg/ast/expression as e +import eyg/ast/pattern as p +import eyg/typer/monotype as t +import eyg/typer + +pub fn do_unify(t1, t2, substitutions) { + case t1, t2 { + t.Unbound(i), t.Unbound(j) if i == j -> Ok(substitutions) + t.Unbound(i), _ -> + case list.key_find(substitutions, i) { + Ok(t1) -> do_unify(t1, t2, substitutions) + Error(Nil) -> Ok([#(i, t2), ..substitutions]) + } + _, t.Unbound(j) -> + case list.key_find(substitutions, j) { + Ok(t2) -> do_unify(t1, t2, substitutions) + Error(Nil) -> Ok([#(j, t1), ..substitutions]) + } + t.Native(n1), t.Native(n2) if n1 == n2 -> Ok(substitutions) + t.Binary, t.Binary -> Ok(substitutions) + t.Tuple(e1), t.Tuple(e2) -> + case list.zip(e1, e2) { + Ok(pairs) -> list.try_fold(pairs, substitutions, unify_pair) + Error(#(c1, c2)) -> Error(typer.IncorrectArity(c1, c2)) + } + t.Function(from1, to1), t.Function(from2, to2) -> { + try substitutions = do_unify(from1, from2, substitutions) + do_unify(to1, to2, substitutions) + } + _, _ -> Error(typer.UnmatchedTypes(t1, t2)) + } +} + +fn unify(t1, t2, state: State(n)) { + let State(substitutions: s, ..) = state + try s = do_unify(t1, t2, s) + // TODO add errors here + Ok(State(..state, substitutions: s)) +} + +fn unify_pair(pair, substitutions) { + let #(t1, t2) = pair + do_unify(t1, t2, substitutions) +} + +pub fn lookup(env, label) { + todo +} + +pub fn generalise(mono, env) { + todo("generalise") +} + +pub fn instantiate(_, _) { + todo +} + +pub fn resolve(_, _) { + todo +} + +pub type State(n) { + State(// definetly not this + // native_to_string: fn(n) -> String, + next_unbound: Int, substitutions: List(#(Int, t.Monotype(n)))) +} + +fn fresh(state) { + let State(next_unbound: i, ..) = state + #(t.Unbound(i), State(..state, next_unbound: i + 1)) +} + +// CAN'T hold onto typer.Reason circular dependency +// definetly not string +// inconsistencies: List(#(List(Int), String)), +pub fn infer(untyped, expected) { + let state = State(0, []) + let scope = [] + do_infer(untyped, expected, state, scope) +} + +// return just substitutions +fn do_infer(untyped, expected, state, scope) { + let #(_, expression) = untyped + case expression { + e.Binary(_) -> + case unify(expected, t.Binary, state) { + Ok(state) -> #(Ok(expected), state) + Error(reason) -> #(Error(reason), state) + } + // e.Variable(label) -> { + // let schema = lookup(env, label) + // let monotype = instantiate(schema, substitutions) + // unify(expected, monotype, substitutions) + // } + e.Function(p.Variable(label), body) -> { + let #(arg, state) = fresh(state) + let #(return, state) = fresh(state) + case unify(expected, t.Function(arg, return), state) { + Ok(state) -> + do_infer(body, return, state, [#(label, #([], arg)), ..scope]) + Error(reason) -> #(Error(reason), state) + } + } + // e.Call(func, with) -> { + // let s = infer(func, fresh, state) + // } + e.Let(p.Variable(label), value, then) -> { + let #(u, state) = fresh(state) + // TODO haandle self case or variable renaming + let #(_t, state) = + do_infer(value, u, state, [#(label, #([], u)), ..scope]) + // generalise with top level scope + let polytype = generalise(resolve(u, state), scope) + do_infer(then, expected, state, [#(label, polytype), ..scope]) + } + } +} diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index bc964dbfb..9fdb42b52 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -12,33 +12,38 @@ import eyg/ast/expression as e import eyg/typer/monotype as t import eyg/ast/pattern as p import eyg/typer/polytype +import eyg/inference // builder pattern for adding variables in test where this would be helpful -pub fn infer(untyped, type_) { - let native_to_string = fn(_: Nil) { "" } - let variables = [#("equal", typer.equal_fn())] - let checker = typer.init(native_to_string) - let scope = typer.root_scope(variables) - let state = #(checker, scope) - // TODO replace all variables - // - // sdo - typer.infer(untyped, type_, state) +// pub fn infer(untyped, type_) { +// let native_to_string = fn(_: Nil) { "" } +// let variables = [#("equal", typer.equal_fn())] +// let checker = typer.init(native_to_string) +// let scope = typer.root_scope(variables) +// let state = #(checker, scope) +// // TODO replace all variables +// // +// // sdo +// typer.infer(untyped, type_, state) +// } +fn infer(untyped, type_) { + inference.infer(untyped, type_) } fn unbound() { t.Unbound(-1) } -fn get_type(typed, checker: typer.Typer(a)) { - case typer.get_type(typed) { +fn get_type(typed, checker) { + let inference.State(substitutions: substitutions, ..) = checker + case typed { Ok(type_) -> { - let resolved = t.resolve(type_, checker.substitutions) + let resolved = t.resolve(type_, substitutions) Ok(resolved) } Error(typer.UnmatchedTypes(expected, given)) -> { - let expected = t.resolve(expected, checker.substitutions) - let given = t.resolve(given, checker.substitutions) + let expected = t.resolve(expected, substitutions) + let given = t.resolve(given, substitutions) Error(typer.UnmatchedTypes(expected, given)) } Error(reason) -> Error(reason) @@ -64,372 +69,335 @@ pub fn binary_expression_test() { assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason } -pub fn tuple_expression_test() { - let source = tuple_([binary("Hello")]) - let #(typed, checker) = infer(source, unbound()) - assert Ok(type_) = get_type(typed, checker) - assert t.Tuple([t.Binary]) = type_ - - let #(typed, checker) = infer(source, t.Tuple([unbound()])) - assert Ok(type_) = get_type(typed, checker) - assert t.Tuple([t.Binary]) = type_ - - let #(typed, checker) = infer(source, t.Tuple([t.Binary])) - assert Ok(type_) = get_type(typed, checker) - assert t.Tuple([t.Binary]) = type_ - - let #(typed, checker) = infer(source, t.Tuple([])) - assert Error(reason) = get_type(typed, checker) - assert typer.IncorrectArity(0, 1) = reason - - let #(typed, checker) = infer(source, t.Tuple([t.Tuple([])])) - // Type is correct here only internally is there a failure - assert Ok(t.Tuple([t.Tuple([])])) = get_type(typed, checker) - assert Ok(element) = get_expression(typed, [0]) - assert Error(reason) = get_type(element, checker) - assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason -} - -pub fn pair_test() { - let source = tuple_([binary("Hello"), tuple_([])]) - - let tx = t.Unbound(-1) - let ty = t.Unbound(-2) - let #(typed, checker) = infer(source, t.Tuple([tx, ty])) - assert Ok(type_) = get_type(typed, checker) - assert t.Tuple([t.Binary, t.Tuple([])]) = type_ - - // could check tx/ty bound properly - let #(typed, checker) = infer(source, t.Tuple([tx, tx])) - assert Ok(type_) = get_type(typed, checker) - assert t.Tuple([t.Binary, t.Binary]) = type_ - assert Ok(element) = get_expression(typed, [1]) - assert Error(reason) = get_type(element, checker) - assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason -} - -pub fn row_expression_test() { - // TODO order when row is called - let source = row([#("foo", binary("Hello"))]) - - let #(typed, checker) = infer(source, unbound()) - assert Ok(type_) = get_type(typed, checker) - assert t.Row([#("foo", t.Binary)], None) = type_ - - let #(typed, checker) = infer(source, t.Row([#("foo", t.Binary)], None)) - assert Ok(type_) = get_type(typed, checker) - assert t.Row([#("foo", t.Binary)], None) = type_ - - // TODO row with some - let #(typed, checker) = - infer(source, t.Row([#("foo", t.Binary), #("bar", t.Binary)], None)) - assert Error(reason) = get_type(typed, checker) - assert typer.MissingFields([#("bar", t.Binary)]) = reason - - let #(typed, checker) = infer(source, t.Row([], None)) - assert Error(reason) = get_type(typed, checker) - - // assert typer.UnexpectedFields([#("foo", t.Binary)]) = reason - // TODO move up - let #(typed, checker) = infer(source, t.Row([#("foo", t.Tuple([]))], None)) - assert Ok(type_) = get_type(typed, checker) - assert t.Row([#("foo", t.Tuple([]))], None) = type_ - assert Ok(element) = get_expression(typed, [0, 1]) - assert Error(reason) = get_type(element, checker) - assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason - - // T.Row(head, option(more_row)) - // Means no such thing as an empty record. Good because tuple is unit - let #(typed, checker) = infer(source, t.Row([#("foo", t.Binary)], Some(-1))) - assert Ok(type_) = get_type(typed, checker) - // TODO should resolve to none - // assert t.Row([#("foo", t.Binary)], None) = type_ -} - -// TODO tag test -// TODO patterns -pub fn var_expression_test() { - let source = variable("x") - - let #(typed, checker) = infer(source, unbound()) - assert Error(reason) = get_type(typed, checker) - // TODO check we're on the lowest unbound integer - assert typer.UnknownVariable("x") = reason -} - -pub fn function_test() { - let source = function(p.Variable(""), binary("")) - - let #(typed, checker) = infer(source, unbound()) - assert Ok(type_) = get_type(typed, checker) - assert t.Function(t.Unbound(_), t.Binary) = type_ - - let #(typed, checker) = infer(source, t.Function(unbound(), t.Unbound(-2))) - assert Ok(type_) = get_type(typed, checker) - assert t.Function(t.Unbound(_), t.Binary) = type_ - - let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Binary)) - assert Ok(type_) = get_type(typed, checker) - assert t.Function(t.Tuple([]), t.Binary) = type_ - - let #(typed, checker) = infer(source, t.Function(unbound(), unbound())) - assert Ok(type_) = get_type(typed, checker) - assert t.Function(t.Binary, t.Binary) = type_ - - let #(typed, checker) = infer(source, t.Binary) - assert Error(reason) = get_type(typed, checker) - - // assert typer.UnmatchedTypes(t.Binary, t.Function(t.Unbound(_), t.Tuple([]))) = - // reason - // TODO move up - let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Tuple([]))) - assert Ok(type_) = get_type(typed, checker) - assert t.Function(t.Tuple([]), t.Tuple([])) = type_ - assert Ok(body) = get_expression(typed, [1]) - assert Error(reason) = get_type(body, checker) - assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason -} - -pub fn id_function_test() { - let source = function(p.Variable("x"), variable("x")) - - let #(typed, checker) = infer(source, unbound()) - assert Ok(type_) = get_type(typed, checker) - assert t.Function(t.Unbound(i), t.Unbound(j)) = type_ - assert True = i == j - - let #(typed, checker) = infer(source, t.Function(unbound(), t.Binary)) - assert Ok(type_) = get_type(typed, checker) - // TODO check unbound is now binary - assert t.Function(t.Binary, t.Binary) = type_ - - let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Binary)) - assert Ok(type_) = get_type(typed, checker) - assert t.Function(t.Tuple([]), t.Binary) = type_ - assert Ok(body) = get_expression(typed, [1]) - assert Error(reason) = get_type(body, checker) - assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason - // Not this is saying that the variable is wrong some how -} - -// equal bin bin -// equal bin tuple still returns true -pub fn call_function_test() { - let func = function(p.Tuple([]), binary("")) - let source = call(func, tuple_([])) - - let #(typed, checker) = infer(source, unbound()) - assert Ok(type_) = get_type(typed, checker) - assert t.Binary = type_ - - let #(typed, checker) = infer(source, t.Binary) - assert Ok(type_) = get_type(typed, checker) - assert t.Binary = type_ - // Error is internal - // let #(typed, checker) = infer(source, t.Tuple([])) - // assert Error(reason) = get_type(typed, checker) - // assert typer.UnmatchedTypes(t.Tuple([]), t.Tuple([])) = reason -} - -pub fn call_generic_function_test() { - let func = function(p.Variable("x"), variable("x")) - let source = call(func, tuple_([])) - - let #(typed, checker) = infer(source, unbound()) - assert Ok(type_) = get_type(typed, checker) - assert t.Tuple([]) = type_ - - let #(typed, checker) = infer(source, t.Tuple([])) - assert Ok(type_) = get_type(typed, checker) - assert t.Tuple([]) = type_ - - // error in generic pushed to arguments - let #(typed, checker) = infer(source, t.Binary) - assert Ok(type_) = get_type(typed, checker) - assert t.Binary = type_ - assert Ok(body) = get_expression(typed, [1]) - assert Error(reason) = get_type(body, checker) - assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason -} - -pub fn call_not_a_function_test() { - let source = call(binary("no a func"), tuple_([])) - - let #(typed, checker) = infer(source, t.Binary) - assert Ok(type_) = get_type(typed, checker) - assert t.Binary = type_ - assert Ok(body) = get_expression(typed, [0]) - assert Error(reason) = get_type(body, checker) - assert typer.UnmatchedTypes(expected, t.Binary) = reason - // TODO resolve expected - // assert t.Function(t.Tuple([]), t.Binary) = expected -} - -pub fn hole_expression_test() { - let source = hole() - - let #(typed, checker) = infer(source, unbound()) - assert Ok(type_) = get_type(typed, checker) - // TODO check we're on the lowest unbound integer - assert t.Unbound(_) = type_ - - let #(typed, checker) = infer(source, t.Binary) - assert Ok(type_) = get_type(typed, checker) - assert t.Binary = type_ -} - -// patterns -pub fn tuple_pattern_test() { - let source = function(p.Tuple(["x"]), variable("x")) - - let #(typed, checker) = infer(source, unbound()) - assert Ok(t.Function(from, _)) = get_type(typed, checker) - assert t.Tuple([t.Unbound(_)]) = from - - let #(typed, checker) = - infer(source, t.Function(t.Tuple([unbound()]), t.Unbound(-2))) - assert Ok(t.Function(from, _)) = get_type(typed, checker) - assert t.Tuple([t.Unbound(_)]) = from - - let #(typed, checker) = - infer(source, t.Function(t.Tuple([t.Binary]), t.Unbound(-2))) - assert Ok(t.Function(from, _)) = get_type(typed, checker) - assert t.Tuple([t.Binary]) = from - - // wrong arity - let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Unbound(-2))) - assert Error(reason) = get_type(typed, checker) - // TODO need to return the function error - assert typer.IncorrectArity(0, 1) = reason - - // wrong bound type - let #(typed, checker) = - infer(source, t.Function(t.Tuple([t.Binary]), t.Tuple([]))) - // Should this be an inside error or not - // assert Error(reason) = get_type(typed, checker) - // // TODO need to return the function error - // assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason -} - -// let -pub fn row_pattern_test() { - let source = function(p.Row([#("foo", "x")]), variable("x")) - // todo -} - -// TODO expanding row type test -// test reusing id -// pub fn recursive_tuple_test() { -// let source = -// let_( -// p.Variable("f"), -// function( -// p.Tuple([]), -// tuple_([binary("x"), call(variable("f"), tuple_([]))]), -// ), -// variable("f"), -// ) +// pub fn tuple_expression_test() { +// let source = tuple_([binary("Hello")]) // let #(typed, checker) = infer(source, unbound()) -// assert Ok(t.Function(from, to)) = get_type(typed, checker) -// assert t.Tuple([]) = from -// // assert t.Tuple([t.Binary, t.Unbound(mu)]) = to -// // typer.get_type(typed) -// // |> io.debug -// list.map(checker.substitutions, io.debug) -// // io.debug(mu) -// // io.debug("----") -// let [x, .._] = checker.substitutions -// let #(-1, t.Function(_, t.Tuple(elements))) = x -// io.debug(elements) -// let [_, t.Recursive(mu, inner)] = elements -// io.debug("loow ") -// io.debug(mu) -// io.debug(inner) -// let t.Tuple([_, t.Unbound(x)]) = inner -// io.debug(x) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Tuple([t.Binary]) = type_ +// let #(typed, checker) = infer(source, t.Tuple([unbound()])) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Tuple([t.Binary]) = type_ +// let #(typed, checker) = infer(source, t.Tuple([t.Binary])) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Tuple([t.Binary]) = type_ +// let #(typed, checker) = infer(source, t.Tuple([])) +// assert Error(reason) = get_type(typed, checker) +// assert typer.IncorrectArity(0, 1) = reason +// let #(typed, checker) = infer(source, t.Tuple([t.Tuple([])])) +// // Type is correct here only internally is there a failure +// assert Ok(t.Tuple([t.Tuple([])])) = get_type(typed, checker) +// assert Ok(element) = get_expression(typed, [0]) +// assert Error(reason) = get_type(element, checker) +// assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason // } -fn my_infer(untyped, goal) { - do_my_infer(untyped, goal, []) -} - -// Do this as alg J -fn do_my_infer(untyped, goal, env) { - let #(_, untyped) = untyped - io.debug(untyped) - case untyped { - e.Let(p.Variable(f), #(_, e.Function(p.Variable(x), body)), then) -> { - let p = t.Unbound(1) - let r = t.Unbound(2) - let env = [#(f, t.Function(p, r)), #(x, p), ..env] - do_my_infer(body, r, env) - } - e.Tuple([e1, e2]) -> { - // unify goal tuple(tnext 1) - let t1 = t.Unbound(3) - let t2 = t.Unbound(4) - io.debug("goal") - io.debug(goal) - do_my_infer(e1, t1, env) - do_my_infer(e2, t2, env) - } - e.Binary(_) -> { - io.debug("is binary") - io.debug(goal) - #(1, 1) - } - e.Call(e1, e2) -> { - io.debug(goal) - io.debug(e1) - io.debug(e2) - // 0 = 1 -> 2 - // 1 = Tuple([]) Null - // 2 = Tuple(3, 4) - // 3 = Binary - // 4 = 1 -> 2.1 - // 2 = Tuple(Binary, 2) - // rA(Binary, A) - // rA[Nil | Cons (B, A)] - // reverse: rA[Nil | Cons (B, A)] -> rA[Nil | Cons (B, A)] - // map: rA[Nil | Cons (B, A)] -> (B, C) -> rD[Nil | Cons (C, D)] -// map: List(B) -> (B -> C) -> List(C) - todo("in call") - } - e.Variable(label) -> { - let t = list.key_find(env, label) - io.debug(t) - todo - } - } - // #(1, 1) -} - -pub fn my_recursive_tuple_test() { +// pub fn pair_test() { +// let source = tuple_([binary("Hello"), tuple_([])]) +// let tx = t.Unbound(-1) +// let ty = t.Unbound(-2) +// let #(typed, checker) = infer(source, t.Tuple([tx, ty])) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Tuple([t.Binary, t.Tuple([])]) = type_ +// // could check tx/ty bound properly +// let #(typed, checker) = infer(source, t.Tuple([tx, tx])) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Tuple([t.Binary, t.Binary]) = type_ +// assert Ok(element) = get_expression(typed, [1]) +// assert Error(reason) = get_type(element, checker) +// assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason +// } +// pub fn row_expression_test() { +// // TODO order when row is called +// let source = row([#("foo", binary("Hello"))]) +// let #(typed, checker) = infer(source, unbound()) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Row([#("foo", t.Binary)], None) = type_ +// let #(typed, checker) = infer(source, t.Row([#("foo", t.Binary)], None)) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Row([#("foo", t.Binary)], None) = type_ +// // TODO row with some +// let #(typed, checker) = +// infer(source, t.Row([#("foo", t.Binary), #("bar", t.Binary)], None)) +// assert Error(reason) = get_type(typed, checker) +// assert typer.MissingFields([#("bar", t.Binary)]) = reason +// let #(typed, checker) = infer(source, t.Row([], None)) +// assert Error(reason) = get_type(typed, checker) +// // assert typer.UnexpectedFields([#("foo", t.Binary)]) = reason +// // TODO move up +// let #(typed, checker) = infer(source, t.Row([#("foo", t.Tuple([]))], None)) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Row([#("foo", t.Tuple([]))], None) = type_ +// assert Ok(element) = get_expression(typed, [0, 1]) +// assert Error(reason) = get_type(element, checker) +// assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason +// // T.Row(head, option(more_row)) +// // Means no such thing as an empty record. Good because tuple is unit +// let #(typed, checker) = infer(source, t.Row([#("foo", t.Binary)], Some(-1))) +// assert Ok(type_) = get_type(typed, checker) +// // TODO should resolve to none +// // assert t.Row([#("foo", t.Binary)], None) = type_ +// } +// // TODO tag test +// // TODO patterns +// pub fn var_expression_test() { +// let source = variable("x") +// let #(typed, checker) = infer(source, unbound()) +// assert Error(reason) = get_type(typed, checker) +// // TODO check we're on the lowest unbound integer +// assert typer.UnknownVariable("x") = reason +// } +// pub fn function_test() { +// let source = function(p.Variable(""), binary("")) +// let #(typed, checker) = infer(source, unbound()) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Function(t.Unbound(_), t.Binary) = type_ +// let #(typed, checker) = infer(source, t.Function(unbound(), t.Unbound(-2))) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Function(t.Unbound(_), t.Binary) = type_ +// let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Binary)) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Function(t.Tuple([]), t.Binary) = type_ +// let #(typed, checker) = infer(source, t.Function(unbound(), unbound())) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Function(t.Binary, t.Binary) = type_ +// let #(typed, checker) = infer(source, t.Binary) +// assert Error(reason) = get_type(typed, checker) +// // assert typer.UnmatchedTypes(t.Binary, t.Function(t.Unbound(_), t.Tuple([]))) = +// // reason +// // TODO move up +// let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Tuple([]))) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Function(t.Tuple([]), t.Tuple([])) = type_ +// assert Ok(body) = get_expression(typed, [1]) +// assert Error(reason) = get_type(body, checker) +// assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason +// } +// pub fn id_function_test() { +// let source = function(p.Variable("x"), variable("x")) +// let #(typed, checker) = infer(source, unbound()) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Function(t.Unbound(i), t.Unbound(j)) = type_ +// assert True = i == j +// let #(typed, checker) = infer(source, t.Function(unbound(), t.Binary)) +// assert Ok(type_) = get_type(typed, checker) +// // TODO check unbound is now binary +// assert t.Function(t.Binary, t.Binary) = type_ +// let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Binary)) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Function(t.Tuple([]), t.Binary) = type_ +// assert Ok(body) = get_expression(typed, [1]) +// assert Error(reason) = get_type(body, checker) +// assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason +// // Not this is saying that the variable is wrong some how +// } +// // equal bin bin +// // equal bin tuple still returns true +// pub fn call_function_test() { +// let func = function(p.Tuple([]), binary("")) +// let source = call(func, tuple_([])) +// let #(typed, checker) = infer(source, unbound()) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Binary = type_ +// let #(typed, checker) = infer(source, t.Binary) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Binary = type_ +// // Error is internal +// // let #(typed, checker) = infer(source, t.Tuple([])) +// // assert Error(reason) = get_type(typed, checker) +// // assert typer.UnmatchedTypes(t.Tuple([]), t.Tuple([])) = reason +// } +// pub fn call_generic_function_test() { +// let func = function(p.Variable("x"), variable("x")) +// let source = call(func, tuple_([])) +// let #(typed, checker) = infer(source, unbound()) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Tuple([]) = type_ +// let #(typed, checker) = infer(source, t.Tuple([])) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Tuple([]) = type_ +// // error in generic pushed to arguments +// let #(typed, checker) = infer(source, t.Binary) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Binary = type_ +// assert Ok(body) = get_expression(typed, [1]) +// assert Error(reason) = get_type(body, checker) +// assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason +// } +// pub fn call_not_a_function_test() { +// let source = call(binary("no a func"), tuple_([])) +// let #(typed, checker) = infer(source, t.Binary) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Binary = type_ +// assert Ok(body) = get_expression(typed, [0]) +// assert Error(reason) = get_type(body, checker) +// assert typer.UnmatchedTypes(expected, t.Binary) = reason +// // TODO resolve expected +// // assert t.Function(t.Tuple([]), t.Binary) = expected +// } +// pub fn hole_expression_test() { +// let source = hole() +// let #(typed, checker) = infer(source, unbound()) +// assert Ok(type_) = get_type(typed, checker) +// // TODO check we're on the lowest unbound integer +// assert t.Unbound(_) = type_ +// let #(typed, checker) = infer(source, t.Binary) +// assert Ok(type_) = get_type(typed, checker) +// assert t.Binary = type_ +// } +// // patterns +// pub fn tuple_pattern_test() { +// let source = function(p.Tuple(["x"]), variable("x")) +// let #(typed, checker) = infer(source, unbound()) +// assert Ok(t.Function(from, _)) = get_type(typed, checker) +// assert t.Tuple([t.Unbound(_)]) = from +// let #(typed, checker) = +// infer(source, t.Function(t.Tuple([unbound()]), t.Unbound(-2))) +// assert Ok(t.Function(from, _)) = get_type(typed, checker) +// assert t.Tuple([t.Unbound(_)]) = from +// let #(typed, checker) = +// infer(source, t.Function(t.Tuple([t.Binary]), t.Unbound(-2))) +// assert Ok(t.Function(from, _)) = get_type(typed, checker) +// assert t.Tuple([t.Binary]) = from +// // wrong arity +// let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Unbound(-2))) +// assert Error(reason) = get_type(typed, checker) +// // TODO need to return the function error +// assert typer.IncorrectArity(0, 1) = reason +// // wrong bound type +// let #(typed, checker) = +// infer(source, t.Function(t.Tuple([t.Binary]), t.Tuple([]))) +// // Should this be an inside error or not +// // assert Error(reason) = get_type(typed, checker) +// // // TODO need to return the function error +// // assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason +// } +// // let +// pub fn row_pattern_test() { +// let source = function(p.Row([#("foo", "x")]), variable("x")) +// // todo +// } +// // TODO expanding row type test +// // test reusing id +// // pub fn recursive_tuple_test() { +// // let source = +// // let_( +// // p.Variable("f"), +// // function( +// // p.Tuple([]), +// // tuple_([binary("x"), call(variable("f"), tuple_([]))]), +// // ), +// // variable("f"), +// // ) +// // let #(typed, checker) = infer(source, unbound()) +// // assert Ok(t.Function(from, to)) = get_type(typed, checker) +// // assert t.Tuple([]) = from +// // // assert t.Tuple([t.Binary, t.Unbound(mu)]) = to +// // // typer.get_type(typed) +// // // |> io.debug +// // list.map(checker.substitutions, io.debug) +// // // io.debug(mu) +// // // io.debug("----") +// // let [x, .._] = checker.substitutions +// // let #(-1, t.Function(_, t.Tuple(elements))) = x +// // io.debug(elements) +// // let [_, t.Recursive(mu, inner)] = elements +// // io.debug("loow ") +// // io.debug(mu) +// // io.debug(inner) +// // let t.Tuple([_, t.Unbound(x)]) = inner +// // io.debug(x) +// // } +// fn my_infer(untyped, goal) { +// do_my_infer(untyped, goal, []) +// } +// // Do this as alg J +// fn do_my_infer(untyped, goal, env) { +// let #(_, untyped) = untyped +// io.debug(untyped) +// case untyped { +// e.Let(p.Variable(f), #(_, e.Function(p.Variable(x), body)), then) -> { +// let p = t.Unbound(1) +// let r = t.Unbound(2) +// let env = [#(f, t.Function(p, r)), #(x, p), ..env] +// do_my_infer(body, r, env) +// } +// e.Tuple([e1, e2]) -> { +// // unify goal tuple(tnext 1) +// let t1 = t.Unbound(3) +// let t2 = t.Unbound(4) +// io.debug("goal") +// io.debug(goal) +// do_my_infer(e1, t1, env) +// do_my_infer(e2, t2, env) +// } +// e.Binary(_) -> { +// io.debug("is binary") +// io.debug(goal) +// #(1, 1) +// } +// e.Call(e1, e2) -> { +// io.debug(goal) +// io.debug(e1) +// io.debug(e2) +// // 0 = 1 -> 2 +// // 1 = Tuple([]) Null +// // 2 = Tuple(3, 4) +// // 3 = Binary +// // 4 = 1 -> 2.1 +// // 2 = Tuple(Binary, 2) +// // rA(Binary, A) +// // rA[Nil | Cons (B, A)] +// // reverse: rA[Nil | Cons (B, A)] -> rA[Nil | Cons (B, A)] +// // map: rA[Nil | Cons (B, A)] -> (B, C) -> rD[Nil | Cons (C, D)] +// // map: List(B) -> (B -> C) -> List(C) +// todo("in call") +// } +// e.Variable(label) -> { +// let t = list.key_find(env, label) +// io.debug(t) +// todo +// } +// } +// // #(1, 1) +// } +pub fn recursive_loop_test() { let source = let_( p.Variable("f"), function( p.Variable("x"), - tuple_([binary("hello"), call(variable("f"), tuple_([]))]), + let_(p.Variable("tmp"), binary(""), call(variable("f"), variable("x"))), ), variable("f"), ) - - let #(typed, checker) = my_infer(source, unbound()) - // assert Ok(t.Function(from, to)) = get_type(typed, checker) - // assert t.Tuple([]) = from - // // assert t.Tuple([t.Binary, t.Unbound(mu)]) = to - // // typer.get_type(typed) - // // |> io.debug - // list.map(checker.substitutions, io.debug) - // // io.debug(mu) - // // io.debug("----") - // let [x, .._] = checker.substitutions - // let #(-1, t.Function(_, t.Tuple(elements))) = x - // io.debug(elements) - // let [_, t.Recursive(mu, inner)] = elements - // io.debug("loow ") - // io.debug(mu) - // io.debug(inner) - // let t.Tuple([_, t.Unbound(x)]) = inner - // io.debug(x) + let #(typed, checker) = infer(source, unbound()) + assert Ok(t.Binary) = get_type(typed, checker) } +// pub fn my_recursive_tuple_test() { +// let source = +// let_( +// p.Variable("f"), +// function( +// p.Variable("x"), +// tuple_([binary("hello"), call(variable("f"), tuple_([]))]), +// ), +// variable("f"), +// ) +// let #(typed, checker) = my_infer(source, unbound()) +// // assert Ok(t.Function(from, to)) = get_type(typed, checker) +// // assert t.Tuple([]) = from +// // // assert t.Tuple([t.Binary, t.Unbound(mu)]) = to +// // // typer.get_type(typed) +// // // |> io.debug +// // list.map(checker.substitutions, io.debug) +// // // io.debug(mu) +// // // io.debug("----") +// // let [x, .._] = checker.substitutions +// // let #(-1, t.Function(_, t.Tuple(elements))) = x +// // io.debug(elements) +// // let [_, t.Recursive(mu, inner)] = elements +// // io.debug("loow ") +// // io.debug(mu) +// // io.debug(inner) +// // let t.Tuple([_, t.Unbound(x)]) = inner +// // io.debug(x) +// } From 3b78b711e1e9461588ffb57f8868396fa28b519a Mon Sep 17 00:00:00 2001 From: Peter Date: Wed, 9 Feb 2022 23:12:53 +0100 Subject: [PATCH 04/18] more steps --- eyg/src/eyg/inference.gleam | 100 ++++++++++++++++++++++++++++------ eyg/test/eyg/terms_test.gleam | 7 +-- 2 files changed, 85 insertions(+), 22 deletions(-) diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index 2c8f7e63b..f115a6041 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -48,16 +48,72 @@ pub fn lookup(env, label) { todo } -pub fn generalise(mono, env) { - todo("generalise") +pub fn do_free_in_type(t, substitutions, set) { + case t { + t.Unbound(i) -> + case list.key_find(substitutions, i) { + Ok(t) -> do_free_in_type(t, substitutions, set) + Error(Nil) -> push_new(i, set) + } + t.Native(_) | t.Binary -> set + // Tuple + // Row + t.Function(from, to) -> { + let set = do_free_in_type(from, substitutions, set) + do_free_in_type(to, substitutions, set) + } + } } -pub fn instantiate(_, _) { - todo +pub fn free_in_type(t, substitutions) { + do_free_in_type(t, substitutions, []) } -pub fn resolve(_, _) { - todo +fn push_new(item: a, set: List(a)) -> List(a) { + case list.find(set, item) { + Ok(_) -> set + Error(Nil) -> [item, ..set] + } +} + +fn is_not_free_in_env(i, substitutions, env) { + // TOODO smart filter or stateful env + True +} + +pub fn generalise(mono, substitutions, env) { + let type_params = + free_in_type(mono, substitutions) + |> list.filter(fn(i) { is_not_free_in_env(i, substitutions, env) }) + // todo("generalise") + // Hmm have Native(Letter) in the type and list of strings in the parameters + // can't be new numbers + // Dont need to be named can just use initial i's discovered + #(type_params, mono) +} + +pub fn instantiate(poly, _) { + // same as resolve with map of new vars + let #([], mono) = poly + mono +} + +pub fn do_resolve(t, substitutions) { + // This has an occurs in thing + t.resolve(t, substitutions) + // case t { + // t.Unbound(i) -> + // case list.key_find(substitutions, i) { + // Ok(t) -> do_resolve(t, substitutions) + // Error(Nil) -> t + // } + // Native(_) | Binary(_) -> t + // } +} + +pub fn resolve(t, state) { + let State(substitutions: substitutions, ..) = state + do_resolve(t, substitutions) } pub type State(n) { @@ -71,9 +127,6 @@ fn fresh(state) { #(t.Unbound(i), State(..state, next_unbound: i + 1)) } -// CAN'T hold onto typer.Reason circular dependency -// definetly not string -// inconsistencies: List(#(List(Int), String)), pub fn infer(untyped, expected) { let state = State(0, []) let scope = [] @@ -89,11 +142,7 @@ fn do_infer(untyped, expected, state, scope) { Ok(state) -> #(Ok(expected), state) Error(reason) -> #(Error(reason), state) } - // e.Variable(label) -> { - // let schema = lookup(env, label) - // let monotype = instantiate(schema, substitutions) - // unify(expected, monotype, substitutions) - // } + e.Function(p.Variable(label), body) -> { let #(arg, state) = fresh(state) let #(return, state) = fresh(state) @@ -103,17 +152,32 @@ fn do_infer(untyped, expected, state, scope) { Error(reason) -> #(Error(reason), state) } } - // e.Call(func, with) -> { - // let s = infer(func, fresh, state) - // } + e.Call(func, with) -> { + let #(arg, state) = fresh(state) + let #(_t, state) = do_infer(func, t.Function(arg, expected), state, scope) + do_infer(with, arg, state, scope) + } + e.Let(p.Variable(label), value, then) -> { let #(u, state) = fresh(state) // TODO haandle self case or variable renaming let #(_t, state) = do_infer(value, u, state, [#(label, #([], u)), ..scope]) // generalise with top level scope - let polytype = generalise(resolve(u, state), scope) + // Don't need generalize + let polytype = generalise(u, state.substitutions, scope) do_infer(then, expected, state, [#(label, polytype), ..scope]) } + e.Variable(label) -> + case list.key_find(scope, label) { + Ok(polytype) -> { + let monotype = instantiate(polytype, state.substitutions) + case unify(expected, monotype, state) { + Ok(state) -> #(Ok(expected), state) + Error(reason) -> #(Error(reason), state) + } + } + Error(Nil) -> #(Error(typer.UnknownVariable(label)), state) + } } } diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index 9fdb42b52..a1aad1ae6 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -35,15 +35,14 @@ fn unbound() { } fn get_type(typed, checker) { - let inference.State(substitutions: substitutions, ..) = checker case typed { Ok(type_) -> { - let resolved = t.resolve(type_, substitutions) + let resolved = inference.resolve(type_, checker) Ok(resolved) } Error(typer.UnmatchedTypes(expected, given)) -> { - let expected = t.resolve(expected, substitutions) - let given = t.resolve(given, substitutions) + let expected = inference.resolve(expected, checker) + let given = inference.resolve(given, checker) Error(typer.UnmatchedTypes(expected, given)) } Error(reason) -> Error(reason) From 551da09c6b30ae4b9d69e8c2fa6354ff61553b2b Mon Sep 17 00:00:00 2001 From: Peter Date: Thu, 10 Feb 2022 08:37:22 +0100 Subject: [PATCH 05/18] fix generalize --- eyg/src/eyg/inference.gleam | 135 +++++++++++++++++++++++++--------- eyg/test/eyg/terms_test.gleam | 69 +++++++++-------- 2 files changed, 139 insertions(+), 65 deletions(-) diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index f115a6041..3e6ee63a4 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -1,32 +1,35 @@ +import gleam/io import gleam/list +import gleam/pair import eyg/ast/expression as e import eyg/ast/pattern as p import eyg/typer/monotype as t import eyg/typer -pub fn do_unify(t1, t2, substitutions) { +pub fn do_unify(pair, substitutions) { + let #(t1, t2) = pair case t1, t2 { t.Unbound(i), t.Unbound(j) if i == j -> Ok(substitutions) t.Unbound(i), _ -> case list.key_find(substitutions, i) { - Ok(t1) -> do_unify(t1, t2, substitutions) + Ok(t1) -> do_unify(#(t1, t2), substitutions) Error(Nil) -> Ok([#(i, t2), ..substitutions]) } _, t.Unbound(j) -> case list.key_find(substitutions, j) { - Ok(t2) -> do_unify(t1, t2, substitutions) + Ok(t2) -> do_unify(#(t1, t2), substitutions) Error(Nil) -> Ok([#(j, t1), ..substitutions]) } t.Native(n1), t.Native(n2) if n1 == n2 -> Ok(substitutions) t.Binary, t.Binary -> Ok(substitutions) t.Tuple(e1), t.Tuple(e2) -> case list.zip(e1, e2) { - Ok(pairs) -> list.try_fold(pairs, substitutions, unify_pair) + Ok(pairs) -> list.try_fold(pairs, substitutions, do_unify) Error(#(c1, c2)) -> Error(typer.IncorrectArity(c1, c2)) } t.Function(from1, to1), t.Function(from2, to2) -> { - try substitutions = do_unify(from1, from2, substitutions) - do_unify(to1, to2, substitutions) + try substitutions = do_unify(#(from1, from2), substitutions) + do_unify(#(to1, to2), substitutions) } _, _ -> Error(typer.UnmatchedTypes(t1, t2)) } @@ -34,16 +37,11 @@ pub fn do_unify(t1, t2, substitutions) { fn unify(t1, t2, state: State(n)) { let State(substitutions: s, ..) = state - try s = do_unify(t1, t2, s) + try s = do_unify(#(t1, t2), s) // TODO add errors here Ok(State(..state, substitutions: s)) } -fn unify_pair(pair, substitutions) { - let #(t1, t2) = pair - do_unify(t1, t2, substitutions) -} - pub fn lookup(env, label) { todo } @@ -69,33 +67,52 @@ pub fn free_in_type(t, substitutions) { do_free_in_type(t, substitutions, []) } -fn push_new(item: a, set: List(a)) -> List(a) { - case list.find(set, item) { - Ok(_) -> set - Error(Nil) -> [item, ..set] +pub fn do_free_in_polytype(poly, substitutions) { + let #(quantifiers, mono) = poly + difference(free_in_type(mono, substitutions), quantifiers) +} + +pub fn do_free_in_env(env, substitutions, set) { + case env { + [] -> set + [#(_, polytype), ..env] -> { + let set = union(do_free_in_polytype(polytype, substitutions), set) + do_free_in_env(env, substitutions, set) + } } } -fn is_not_free_in_env(i, substitutions, env) { - // TOODO smart filter or stateful env - True +pub fn free_in_env(env, substitutions) { + do_free_in_env(env, substitutions, []) } +// TODO smart filter or stateful env +// |> list.filter(fn(i) { is_not_free_in_env(i, substitutions, env) }) +// Hmm have Native(Letter) in the type and list of strings in the parameters +// can't be new numbers +// Dont need to be named can just use initial i's discovered pub fn generalise(mono, substitutions, env) { let type_params = - free_in_type(mono, substitutions) - |> list.filter(fn(i) { is_not_free_in_env(i, substitutions, env) }) - // todo("generalise") - // Hmm have Native(Letter) in the type and list of strings in the parameters - // can't be new numbers - // Dont need to be named can just use initial i's discovered + difference( + free_in_type(mono, substitutions), + free_in_env(env, substitutions), + ) #(type_params, mono) } -pub fn instantiate(poly, _) { - // same as resolve with map of new vars - let #([], mono) = poly - mono +pub fn instantiate(poly, state) { + let #(forall, mono) = poly + let #(substitutions, state) = + list.map_state( + forall, + state, + fn(i, state) { + let #(tj, state) = fresh(state) + #(#(i, tj), state) + }, + ) + let t = do_resolve(mono, substitutions) + #(t, state) } pub fn do_resolve(t, substitutions) { @@ -142,7 +159,24 @@ fn do_infer(untyped, expected, state, scope) { Ok(state) -> #(Ok(expected), state) Error(reason) -> #(Error(reason), state) } - + e.Tuple(elements) -> { + let #(with_type, state) = + list.map_state( + elements, + state, + fn(e, state) { + let #(u, state) = fresh(state) + #(#(e, u), state) + }, + ) + case unify(expected, t.Tuple(list.map(with_type, pair.second)), state) { + Ok(state) -> #(Ok(expected), state) + Error(reason) -> #(Error(reason), state) + } + list.map_state(with_type, fn(with_type, state) { + let #(element, expected) = + }) + } e.Function(p.Variable(label), body) -> { let #(arg, state) = fresh(state) let #(return, state) = fresh(state) @@ -161,17 +195,15 @@ fn do_infer(untyped, expected, state, scope) { e.Let(p.Variable(label), value, then) -> { let #(u, state) = fresh(state) // TODO haandle self case or variable renaming - let #(_t, state) = - do_infer(value, u, state, [#(label, #([], u)), ..scope]) - // generalise with top level scope - // Don't need generalize + let value_scope = [#(label, #([], u)), ..scope] + let #(_t, state) = do_infer(value, u, state, value_scope) let polytype = generalise(u, state.substitutions, scope) do_infer(then, expected, state, [#(label, polytype), ..scope]) } e.Variable(label) -> case list.key_find(scope, label) { Ok(polytype) -> { - let monotype = instantiate(polytype, state.substitutions) + let #(monotype, state) = instantiate(polytype, state) case unify(expected, monotype, state) { Ok(state) -> #(Ok(expected), state) Error(reason) -> #(Error(reason), state) @@ -181,3 +213,36 @@ fn do_infer(untyped, expected, state, scope) { } } } + +// Set +fn push_new(item: a, set: List(a)) -> List(a) { + case list.find(set, item) { + Ok(_) -> set + Error(Nil) -> [item, ..set] + } +} + +fn difference(items: List(a), excluded: List(a)) -> List(a) { + do_difference(items, excluded, []) +} + +fn do_difference(items, excluded, accumulator) { + case items { + [] -> list.reverse(accumulator) + [next, ..items] -> + case list.find(excluded, next) { + Ok(_) -> do_difference(items, excluded, accumulator) + Error(_) -> push_new(next, accumulator) + } + } +} + +fn union(new: List(a), existing: List(a)) -> List(a) { + case new { + [] -> existing + [next, ..new] -> { + let existing = push_new(next, existing) + union(new, existing) + } + } +} diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index a1aad1ae6..5b891fa4e 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -369,34 +369,43 @@ pub fn recursive_loop_test() { variable("f"), ) let #(typed, checker) = infer(source, unbound()) - assert Ok(t.Binary) = get_type(typed, checker) + assert Ok(t.Function(t.Unbound(i), t.Unbound(j))) = get_type(typed, checker) + assert True = i != j + // TODO x = i and f = i -> j internally but not poly + // assert Ok(body) = get_expression(typed, [1]) + // assert Ok(t.Function(t.Unbound(i), t.Unbound(j))) = get_type(body, checker) + // TODO ---- + // id called polymorphically internally FAil + // id called polymorphically externally Success +} + +// TODO let x = x Test +pub fn my_recursive_tuple_test() { + let source = + let_( + p.Variable("f"), + function( + p.Variable("x"), + tuple_([binary("hello"), call(variable("f"), tuple_([]))]), + ), + variable("f"), + ) + let #(typed, checker) = infer(source, unbound()) + // assert Ok(t.Function(from, to)) = get_type(typed, checker) + // assert t.Tuple([]) = from + // // assert t.Tuple([t.Binary, t.Unbound(mu)]) = to + // // typer.get_type(typed) + // // |> io.debug + // list.map(checker.substitutions, io.debug) + // // io.debug(mu) + // // io.debug("----") + // let [x, .._] = checker.substitutions + // let #(-1, t.Function(_, t.Tuple(elements))) = x + // io.debug(elements) + // let [_, t.Recursive(mu, inner)] = elements + // io.debug("loow ") + // io.debug(mu) + // io.debug(inner) + // let t.Tuple([_, t.Unbound(x)]) = inner + // io.debug(x) } -// pub fn my_recursive_tuple_test() { -// let source = -// let_( -// p.Variable("f"), -// function( -// p.Variable("x"), -// tuple_([binary("hello"), call(variable("f"), tuple_([]))]), -// ), -// variable("f"), -// ) -// let #(typed, checker) = my_infer(source, unbound()) -// // assert Ok(t.Function(from, to)) = get_type(typed, checker) -// // assert t.Tuple([]) = from -// // // assert t.Tuple([t.Binary, t.Unbound(mu)]) = to -// // // typer.get_type(typed) -// // // |> io.debug -// // list.map(checker.substitutions, io.debug) -// // // io.debug(mu) -// // // io.debug("----") -// // let [x, .._] = checker.substitutions -// // let #(-1, t.Function(_, t.Tuple(elements))) = x -// // io.debug(elements) -// // let [_, t.Recursive(mu, inner)] = elements -// // io.debug("loow ") -// // io.debug(mu) -// // io.debug(inner) -// // let t.Tuple([_, t.Unbound(x)]) = inner -// // io.debug(x) -// } From f26ed697867bf7dfa425a4b4e6f92a4933de28d3 Mon Sep 17 00:00:00 2001 From: Peter Date: Thu, 10 Feb 2022 19:47:02 +0100 Subject: [PATCH 06/18] recursive type printing --- eyg/src/eyg/inference.gleam | 229 ++++++++++++++++++++++++++++------ eyg/test/eyg/terms_test.gleam | 16 ++- 2 files changed, 204 insertions(+), 41 deletions(-) diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index 3e6ee63a4..58e5c217a 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -1,4 +1,6 @@ import gleam/io +import gleam/int +import gleam/string import gleam/list import gleam/pair import eyg/ast/expression as e @@ -6,19 +8,28 @@ import eyg/ast/pattern as p import eyg/typer/monotype as t import eyg/typer -pub fn do_unify(pair, substitutions) { +pub fn do_unify( + pair: #(t.Monotype(n), t.Monotype(n)), + substitutions: List(#(Int, #(Bool, t.Monotype(n)))), +) -> Result(List(#(Int, #(Bool, t.Monotype(n)))), typer.Reason(n)) { let #(t1, t2) = pair case t1, t2 { t.Unbound(i), t.Unbound(j) if i == j -> Ok(substitutions) t.Unbound(i), _ -> case list.key_find(substitutions, i) { - Ok(t1) -> do_unify(#(t1, t2), substitutions) - Error(Nil) -> Ok([#(i, t2), ..substitutions]) + Ok(#(_rec, t1)) -> do_unify(#(t1, t2), substitutions) + Error(Nil) -> { + let rec = i == 2 + Ok([#(i, #(rec, t2)), ..substitutions]) + } } _, t.Unbound(j) -> case list.key_find(substitutions, j) { - Ok(t2) -> do_unify(#(t1, t2), substitutions) - Error(Nil) -> Ok([#(j, t1), ..substitutions]) + Ok(#(_rec, t2)) -> do_unify(#(t1, t2), substitutions) + Error(Nil) -> { + let rec = j == 2 + Ok([#(j, #(rec, t1)), ..substitutions]) + } } t.Native(n1), t.Native(n2) if n1 == n2 -> Ok(substitutions) t.Binary, t.Binary -> Ok(substitutions) @@ -46,27 +57,63 @@ pub fn lookup(env, label) { todo } -pub fn do_free_in_type(t, substitutions, set) { - case t { - t.Unbound(i) -> - case list.key_find(substitutions, i) { - Ok(t) -> do_free_in_type(t, substitutions, set) - Error(Nil) -> push_new(i, set) - } - t.Native(_) | t.Binary -> set - // Tuple - // Row - t.Function(from, to) -> { - let set = do_free_in_type(from, substitutions, set) - do_free_in_type(to, substitutions, set) - } - } +pub fn do_free_in_type( + t, + substitutions: List(#(Int, #(Bool, t.Monotype(n)))), + set, +) { + // io.debug(t) + // io.debug("-=-------------------") + // list.map( + // substitutions, + // fn(s) { + // let #(k, #(b, t)) = s + // io.debug(k) + // io.debug(b) + // io.debug(t.to_string(t, fn(_) { "OOO" })) + // }, + // ) + // io.debug(monotype.to_string(t1, fn(_) { "OTHER" })) + // TODO remove + [] + // case t { + // t.Unbound(i) -> + // case list.key_find(substitutions, i) { + // Ok(#(_rec, t)) -> do_free_in_type(t, substitutions, set) + // Error(Nil) -> push_new(i, set) + // } + // t.Native(_) | t.Binary -> set + // t.Tuple(elements) -> + // list.fold( + // elements, + // set, + // fn(e, set) { do_free_in_type(e, substitutions, set) }, + // ) + // // Row + // t.Function(from, to) -> { + // let set = do_free_in_type(from, substitutions, set) + // do_free_in_type(to, substitutions, set) + // } + // } } pub fn free_in_type(t, substitutions) { do_free_in_type(t, substitutions, []) } +fn do_free_in_elements(elements, substitutions, set) { + todo + // case elements { + // [] -> set + // [element, ..rest] -> + // do_free_in_elements( + // rest, + // substitutions, + // do_free_in_type(element, substitutions, set), + // ) + // } +} + pub fn do_free_in_polytype(poly, substitutions) { let #(quantifiers, mono) = poly difference(free_in_type(mono, substitutions), quantifiers) @@ -100,6 +147,7 @@ pub fn generalise(mono, substitutions, env) { #(type_params, mono) } +// Need to handle having recursive type on it's own. i.e. i needs to be in Recurive(i, inner) pub fn instantiate(poly, state) { let #(forall, mono) = poly let #(substitutions, state) = @@ -108,35 +156,118 @@ pub fn instantiate(poly, state) { state, fn(i, state) { let #(tj, state) = fresh(state) - #(#(i, tj), state) + // TODO does this need to handle + #(#(i, #(False, tj)), state) }, ) - let t = do_resolve(mono, substitutions) + let t = do_resolve(mono, substitutions, []) #(t, state) } -pub fn do_resolve(t, substitutions) { - // This has an occurs in thing - t.resolve(t, substitutions) - // case t { - // t.Unbound(i) -> - // case list.key_find(substitutions, i) { - // Ok(t) -> do_resolve(t, substitutions) - // Error(Nil) -> t - // } - // Native(_) | Binary(_) -> t - // } +// TODO tags/unions + +pub fn print(t, substitutions, recuring) { + case t { + t.Unbound(i) -> + case list.find(recuring, i) { + Ok(_) -> int.to_string(i) + Error(Nil) -> + case list.key_find(substitutions, i) { + Error(Nil) -> int.to_string(i) + Ok(#(True, t)) -> + string.join([ + "μ", + int.to_string(i), + ".", + print(t, substitutions, [i, ..recuring]), + ]) + Ok(#(False, t)) -> print(t, substitutions, recuring) + } + } + t.Tuple(elements) -> + string.join([ + "(", + string.join(list.intersperse( + list.map(elements, print(_, substitutions, recuring)), + ", ", + )), + ")", + ]) + t.Binary -> "Binary" + t.Function(from, to) -> + string.join([ + print(from, substitutions, recuring), + " -> ", + print(to, substitutions, recuring), + ]) + } +} + +pub fn do_resolve(type_, substitutions, recuring) { + case type_ { + t.Unbound(i) -> + case list.find(recuring, i) { + Error(Nil) -> + case list.key_find(substitutions, i) { + Ok(#(_rec, t.Unbound(j))) if i == j -> type_ + Error(Nil) -> type_ + Ok(#(False, s)) -> do_resolve(s, substitutions, recuring) + Ok(#(True, s)) -> do_resolve(s, substitutions, [i, ..recuring]) + } + } + // case occurs_in(Unbound(i), substitution) { + // False -> resolve(substitution, substitutions) + // True -> { + // io.debug("====================") + // io.debug(substitution) + // Recursive(i, substitution) + // } + // } + // let False = + // t.Native(name) -> Native(name) + t.Binary -> t.Binary + t.Tuple(elements) -> { + let elements = list.map(elements, do_resolve(_, substitutions, recuring)) + t.Tuple(elements) + } + // Row(fields, rest) -> { + // let resolved_fields = + // list.map( + // fields, + // fn(field) { + // let #(name, type_) = field + // #(name, do_resolve(type_, substitutions)) + // }, + // ) + // case rest { + // None -> Row(resolved_fields, None) + // Some(i) -> { + // type_ + // case do_resolve(Unbound(i), substitutions) { + // Unbound(j) -> Row(resolved_fields, Some(j)) + // Row(inner, rest) -> Row(list.append(resolved_fields, inner), rest) + // } + // } + // } + // } + // TODO check do_resolve in our record based recursive frunctions + t.Function(from, to) -> { + let from = do_resolve(from, substitutions, recuring) + let to = do_resolve(to, substitutions, recuring) + t.Function(from, to) + } + } } pub fn resolve(t, state) { let State(substitutions: substitutions, ..) = state - do_resolve(t, substitutions) + do_resolve(t, substitutions, []) } pub type State(n) { State(// definetly not this // native_to_string: fn(n) -> String, - next_unbound: Int, substitutions: List(#(Int, t.Monotype(n)))) + next_unbound: Int, substitutions: List(#(Int, #(Bool, t.Monotype(n))))) } fn fresh(state) { @@ -151,7 +282,12 @@ pub fn infer(untyped, expected) { } // return just substitutions -fn do_infer(untyped, expected, state, scope) { +fn do_infer( + untyped, + expected, + state, + scope, +) -> #(Result(t.Monotype(n), typer.Reason(n)), State(n)) { let #(_, expression) = untyped case expression { e.Binary(_) -> @@ -169,20 +305,33 @@ fn do_infer(untyped, expected, state, scope) { #(#(e, u), state) }, ) - case unify(expected, t.Tuple(list.map(with_type, pair.second)), state) { + let #(t, state) = case unify( + expected, + t.Tuple(list.map(with_type, pair.second)), + state, + ) { Ok(state) -> #(Ok(expected), state) Error(reason) -> #(Error(reason), state) } - list.map_state(with_type, fn(with_type, state) { - let #(element, expected) = - }) + let #(_, state) = + list.map_state( + with_type, + state, + fn(with_type, state) { + let #(element, expected) = with_type + do_infer(element, expected, state, scope) + }, + ) + #(t, state) } e.Function(p.Variable(label), body) -> { let #(arg, state) = fresh(state) let #(return, state) = fresh(state) case unify(expected, t.Function(arg, return), state) { Ok(state) -> + // let state = do_infer(body, return, state, [#(label, #([], arg)), ..scope]) + // #(Ok(expected), state) Error(reason) -> #(Error(reason), state) } } diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index 5b891fa4e..6d78412d1 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -390,7 +390,21 @@ pub fn my_recursive_tuple_test() { ), variable("f"), ) - let #(typed, checker) = infer(source, unbound()) + let #(Ok(typed), checker) = infer(source, unbound()) + + io.debug("-=-------------------") + // io.debug(typed) + list.map( + checker.substitutions, + fn(s) { + let #(k, #(b, t)) = s + io.debug(k) + io.debug(b) + io.debug(t.to_string(t, fn(_) { "OOO" })) + }, + ) + inference.print(typed, checker.substitutions, []) + |> io.debug // assert Ok(t.Function(from, to)) = get_type(typed, checker) // assert t.Tuple([]) = from // // assert t.Tuple([t.Binary, t.Unbound(mu)]) = to From 16bc5681531bf3d24c25dcb837f1cea49c49fac6 Mon Sep 17 00:00:00 2001 From: Peter Date: Sat, 19 Feb 2022 08:23:56 +0100 Subject: [PATCH 07/18] fix test with recursion as is --- eyg/src/eyg/inference.gleam | 23 ++++++++++++++--------- eyg/test/eyg/terms_test.gleam | 5 +++-- 2 files changed, 17 insertions(+), 11 deletions(-) diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index 58e5c217a..2b9008f8f 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -18,18 +18,12 @@ pub fn do_unify( t.Unbound(i), _ -> case list.key_find(substitutions, i) { Ok(#(_rec, t1)) -> do_unify(#(t1, t2), substitutions) - Error(Nil) -> { - let rec = i == 2 - Ok([#(i, #(rec, t2)), ..substitutions]) - } + Error(Nil) -> Ok(add_substitution(i, t2, substitutions)) } _, t.Unbound(j) -> case list.key_find(substitutions, j) { Ok(#(_rec, t2)) -> do_unify(#(t1, t2), substitutions) - Error(Nil) -> { - let rec = j == 2 - Ok([#(j, #(rec, t1)), ..substitutions]) - } + Error(Nil) -> Ok(add_substitution(j, t1, substitutions)) } t.Native(n1), t.Native(n2) if n1 == n2 -> Ok(substitutions) t.Binary, t.Binary -> Ok(substitutions) @@ -46,6 +40,14 @@ pub fn do_unify( } } +fn add_substitution(i, type_, substitutions) { + // TODO occurs in check + // We assume i doesn't occur in substitutions + // List.contains(free_in_type(type_), i) + let rec = i == 2 + [#(i, #(rec, type_)), ..substitutions] +} + fn unify(t1, t2, state: State(n)) { let State(substitutions: s, ..) = state try s = do_unify(#(t1, t2), s) @@ -165,7 +167,10 @@ pub fn instantiate(poly, state) { } // TODO tags/unions - +// everything should be doable with resolve if we have a Recursive type +// When unifying Does recursion need to be someting that can move between substitutions +// When writing an annotation it would include recursive types +// List(B) = μA.[Null | Cons(B, A)] pub fn print(t, substitutions, recuring) { case t { t.Unbound(i) -> diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index 6d78412d1..b6a362c64 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -403,8 +403,9 @@ pub fn my_recursive_tuple_test() { io.debug(t.to_string(t, fn(_) { "OOO" })) }, ) - inference.print(typed, checker.substitutions, []) - |> io.debug + let "() -> μ2.(Binary, 2)" = + inference.print(typed, checker.substitutions, []) + |> io.debug // assert Ok(t.Function(from, to)) = get_type(typed, checker) // assert t.Tuple([]) = from // // assert t.Tuple([t.Binary, t.Unbound(mu)]) = to From 37f5b84dd6ce7f7c1de6ec5cc8701a0a2d168d02 Mon Sep 17 00:00:00 2001 From: Peter Date: Sat, 19 Feb 2022 08:39:54 +0100 Subject: [PATCH 08/18] switch to recurring type --- eyg/src/eyg/inference.gleam | 44 ++++++++++++++++++----------------- eyg/test/eyg/terms_test.gleam | 17 +++++++------- 2 files changed, 31 insertions(+), 30 deletions(-) diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index 2b9008f8f..940d90653 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -10,19 +10,19 @@ import eyg/typer pub fn do_unify( pair: #(t.Monotype(n), t.Monotype(n)), - substitutions: List(#(Int, #(Bool, t.Monotype(n)))), -) -> Result(List(#(Int, #(Bool, t.Monotype(n)))), typer.Reason(n)) { + substitutions: List(#(Int, t.Monotype(n))), +) -> Result(List(#(Int, t.Monotype(n))), typer.Reason(n)) { let #(t1, t2) = pair case t1, t2 { t.Unbound(i), t.Unbound(j) if i == j -> Ok(substitutions) t.Unbound(i), _ -> case list.key_find(substitutions, i) { - Ok(#(_rec, t1)) -> do_unify(#(t1, t2), substitutions) + Ok(t1) -> do_unify(#(t1, t2), substitutions) Error(Nil) -> Ok(add_substitution(i, t2, substitutions)) } _, t.Unbound(j) -> case list.key_find(substitutions, j) { - Ok(#(_rec, t2)) -> do_unify(#(t1, t2), substitutions) + Ok(t2) -> do_unify(#(t1, t2), substitutions) Error(Nil) -> Ok(add_substitution(j, t1, substitutions)) } t.Native(n1), t.Native(n2) if n1 == n2 -> Ok(substitutions) @@ -44,8 +44,11 @@ fn add_substitution(i, type_, substitutions) { // TODO occurs in check // We assume i doesn't occur in substitutions // List.contains(free_in_type(type_), i) - let rec = i == 2 - [#(i, #(rec, type_)), ..substitutions] + let type_ = case i == 2 { + True -> t.Recursive(i, type_) + False -> type_ + } + [#(i, type_), ..substitutions] } fn unify(t1, t2, state: State(n)) { @@ -59,11 +62,7 @@ pub fn lookup(env, label) { todo } -pub fn do_free_in_type( - t, - substitutions: List(#(Int, #(Bool, t.Monotype(n)))), - set, -) { +pub fn do_free_in_type(t, substitutions: List(#(Int, t.Monotype(n))), set) { // io.debug(t) // io.debug("-=-------------------") // list.map( @@ -149,7 +148,7 @@ pub fn generalise(mono, substitutions, env) { #(type_params, mono) } -// Need to handle having recursive type on it's own. i.e. i needs to be in Recurive(i, inner) +// Need to handle having recursive type on it's own. i.e. i needs to be in Recursive(i, inner) pub fn instantiate(poly, state) { let #(forall, mono) = poly let #(substitutions, state) = @@ -157,9 +156,9 @@ pub fn instantiate(poly, state) { forall, state, fn(i, state) { + // TODO with zip let #(tj, state) = fresh(state) - // TODO does this need to handle - #(#(i, #(False, tj)), state) + #(#(i, tj), state) }, ) let t = do_resolve(mono, substitutions, []) @@ -179,14 +178,14 @@ pub fn print(t, substitutions, recuring) { Error(Nil) -> case list.key_find(substitutions, i) { Error(Nil) -> int.to_string(i) - Ok(#(True, t)) -> + Ok(t.Recursive(i, t)) -> string.join([ "μ", int.to_string(i), ".", print(t, substitutions, [i, ..recuring]), ]) - Ok(#(False, t)) -> print(t, substitutions, recuring) + Ok(t) -> print(t, substitutions, recuring) } } t.Tuple(elements) -> @@ -208,16 +207,19 @@ pub fn print(t, substitutions, recuring) { } } -pub fn do_resolve(type_, substitutions, recuring) { +pub fn do_resolve(type_, substitutions: List(#(Int, t.Monotype(n))), recuring) { case type_ { t.Unbound(i) -> case list.find(recuring, i) { Error(Nil) -> case list.key_find(substitutions, i) { - Ok(#(_rec, t.Unbound(j))) if i == j -> type_ + Ok(t.Unbound(j)) if i == j -> type_ Error(Nil) -> type_ - Ok(#(False, s)) -> do_resolve(s, substitutions, recuring) - Ok(#(True, s)) -> do_resolve(s, substitutions, [i, ..recuring]) + Ok(t.Recursive(j, sub)) -> { + let inner = do_resolve(sub, substitutions, [j, ..recuring]) + t.Recursive(j, inner) + } + Ok(sub) -> do_resolve(sub, substitutions, recuring) } } // case occurs_in(Unbound(i), substitution) { @@ -272,7 +274,7 @@ pub fn resolve(t, state) { pub type State(n) { State(// definetly not this // native_to_string: fn(n) -> String, - next_unbound: Int, substitutions: List(#(Int, #(Bool, t.Monotype(n))))) + next_unbound: Int, substitutions: List(#(Int, t.Monotype(n)))) } fn fresh(state) { diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index b6a362c64..298d435a1 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -394,15 +394,14 @@ pub fn my_recursive_tuple_test() { io.debug("-=-------------------") // io.debug(typed) - list.map( - checker.substitutions, - fn(s) { - let #(k, #(b, t)) = s - io.debug(k) - io.debug(b) - io.debug(t.to_string(t, fn(_) { "OOO" })) - }, - ) + // list.map( + // checker.substitutions, + // fn(s) { + // let #(k, t) = s + // io.debug(k) + // io.debug(t.to_string(t, fn(_) { "OOO" })) + // }, + // ) let "() -> μ2.(Binary, 2)" = inference.print(typed, checker.substitutions, []) |> io.debug From 0b25bb6281785dabe8f5d1eff6c24e6898d9e860 Mon Sep 17 00:00:00 2001 From: Peter Date: Sat, 19 Feb 2022 14:48:33 +0100 Subject: [PATCH 09/18] separate resolve and pring --- eyg/src/eyg/inference.gleam | 56 ++++++++++------------------------- eyg/test/eyg/terms_test.gleam | 2 +- 2 files changed, 17 insertions(+), 41 deletions(-) diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index 940d90653..749812407 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -170,40 +170,25 @@ pub fn instantiate(poly, state) { // When unifying Does recursion need to be someting that can move between substitutions // When writing an annotation it would include recursive types // List(B) = μA.[Null | Cons(B, A)] -pub fn print(t, substitutions, recuring) { +pub fn print(t, state) { + let type_ = resolve(t, state) + to_string(type_) +} + +fn to_string(t) { case t { - t.Unbound(i) -> - case list.find(recuring, i) { - Ok(_) -> int.to_string(i) - Error(Nil) -> - case list.key_find(substitutions, i) { - Error(Nil) -> int.to_string(i) - Ok(t.Recursive(i, t)) -> - string.join([ - "μ", - int.to_string(i), - ".", - print(t, substitutions, [i, ..recuring]), - ]) - Ok(t) -> print(t, substitutions, recuring) - } - } + t.Unbound(i) -> int.to_string(i) + t.Recursive(i, t) -> + string.join(["μ", int.to_string(i), ".", to_string(t)]) t.Tuple(elements) -> string.join([ "(", - string.join(list.intersperse( - list.map(elements, print(_, substitutions, recuring)), - ", ", - )), + string.join(list.intersperse(list.map(elements, to_string), ", ")), ")", ]) t.Binary -> "Binary" t.Function(from, to) -> - string.join([ - print(from, substitutions, recuring), - " -> ", - print(to, substitutions, recuring), - ]) + string.join([to_string(from), " -> ", to_string(to)]) } } @@ -211,27 +196,18 @@ pub fn do_resolve(type_, substitutions: List(#(Int, t.Monotype(n))), recuring) { case type_ { t.Unbound(i) -> case list.find(recuring, i) { + Ok(_) -> type_ Error(Nil) -> case list.key_find(substitutions, i) { Ok(t.Unbound(j)) if i == j -> type_ Error(Nil) -> type_ - Ok(t.Recursive(j, sub)) -> { - let inner = do_resolve(sub, substitutions, [j, ..recuring]) - t.Recursive(j, inner) - } Ok(sub) -> do_resolve(sub, substitutions, recuring) } } - // case occurs_in(Unbound(i), substitution) { - // False -> resolve(substitution, substitutions) - // True -> { - // io.debug("====================") - // io.debug(substitution) - // Recursive(i, substitution) - // } - // } - // let False = - // t.Native(name) -> Native(name) + t.Recursive(i, sub) -> { + let inner = do_resolve(sub, substitutions, [i, ..recuring]) + t.Recursive(i, inner) + } t.Binary -> t.Binary t.Tuple(elements) -> { let elements = list.map(elements, do_resolve(_, substitutions, recuring)) diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index 298d435a1..0c322d69a 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -403,7 +403,7 @@ pub fn my_recursive_tuple_test() { // }, // ) let "() -> μ2.(Binary, 2)" = - inference.print(typed, checker.substitutions, []) + inference.print(typed, checker) |> io.debug // assert Ok(t.Function(from, to)) = get_type(typed, checker) // assert t.Tuple([]) = from From f1250e88a14d7cb6024122d2c77bbe4c0991fea0 Mon Sep 17 00:00:00 2001 From: Peter Date: Sat, 19 Feb 2022 15:11:56 +0100 Subject: [PATCH 10/18] fix free in type --- eyg/src/eyg/inference.gleam | 90 +++++++++++----------------------- eyg/src/gleam/list.gleam | 7 +++ eyg/test/eyg/terms_test.gleam | 91 ++++++++++++++++++----------------- 3 files changed, 83 insertions(+), 105 deletions(-) diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index 749812407..eb5757ec4 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -43,7 +43,7 @@ pub fn do_unify( fn add_substitution(i, type_, substitutions) { // TODO occurs in check // We assume i doesn't occur in substitutions - // List.contains(free_in_type(type_), i) + // list.contains(free_in_type(type_), i) let type_ = case i == 2 { True -> t.Recursive(i, type_) False -> type_ @@ -62,62 +62,32 @@ pub fn lookup(env, label) { todo } -pub fn do_free_in_type(t, substitutions: List(#(Int, t.Monotype(n))), set) { - // io.debug(t) - // io.debug("-=-------------------") - // list.map( - // substitutions, - // fn(s) { - // let #(k, #(b, t)) = s - // io.debug(k) - // io.debug(b) - // io.debug(t.to_string(t, fn(_) { "OOO" })) - // }, - // ) - // io.debug(monotype.to_string(t1, fn(_) { "OTHER" })) - // TODO remove - [] - // case t { - // t.Unbound(i) -> - // case list.key_find(substitutions, i) { - // Ok(#(_rec, t)) -> do_free_in_type(t, substitutions, set) - // Error(Nil) -> push_new(i, set) - // } - // t.Native(_) | t.Binary -> set - // t.Tuple(elements) -> - // list.fold( - // elements, - // set, - // fn(e, set) { do_free_in_type(e, substitutions, set) }, - // ) - // // Row - // t.Function(from, to) -> { - // let set = do_free_in_type(from, substitutions, set) - // do_free_in_type(to, substitutions, set) - // } - // } -} - -pub fn free_in_type(t, substitutions) { - do_free_in_type(t, substitutions, []) +// relies on type having been resolved +fn do_free_in_type(type_, set) { + case type_ { + t.Unbound(i) -> push_new(i, set) + t.Native(_) | t.Binary -> set + t.Tuple(elements) -> list.fold(elements, set, do_free_in_type) + t.Recursive(i, type_) -> { + let inner = do_free_in_type(type_, set) + difference(inner, [i]) + } + // Row + t.Function(from, to) -> { + let set = do_free_in_type(from, set) + do_free_in_type(to, set) + } + } } -fn do_free_in_elements(elements, substitutions, set) { - todo - // case elements { - // [] -> set - // [element, ..rest] -> - // do_free_in_elements( - // rest, - // substitutions, - // do_free_in_type(element, substitutions, set), - // ) - // } +pub fn free_in_type(t) { + do_free_in_type(t, []) } pub fn do_free_in_polytype(poly, substitutions) { let #(quantifiers, mono) = poly - difference(free_in_type(mono, substitutions), quantifiers) + let mono = resolve(mono, substitutions) + difference(free_in_type(mono), quantifiers) } pub fn do_free_in_env(env, substitutions, set) { @@ -140,11 +110,9 @@ pub fn free_in_env(env, substitutions) { // can't be new numbers // Dont need to be named can just use initial i's discovered pub fn generalise(mono, substitutions, env) { + let mono = resolve(mono, substitutions) let type_params = - difference( - free_in_type(mono, substitutions), - free_in_env(env, substitutions), - ) + difference(free_in_type(mono), free_in_env(env, substitutions)) #(type_params, mono) } @@ -265,12 +233,7 @@ pub fn infer(untyped, expected) { } // return just substitutions -fn do_infer( - untyped, - expected, - state, - scope, -) -> #(Result(t.Monotype(n), typer.Reason(n)), State(n)) { +fn do_infer(untyped, expected, state, scope) { let #(_, expression) = untyped case expression { e.Binary(_) -> @@ -307,6 +270,9 @@ fn do_infer( ) #(t, state) } + + // e.Row(fields) -> { + // } e.Function(p.Variable(label), body) -> { let #(arg, state) = fresh(state) let #(return, state) = fresh(state) @@ -329,7 +295,7 @@ fn do_infer( // TODO haandle self case or variable renaming let value_scope = [#(label, #([], u)), ..scope] let #(_t, state) = do_infer(value, u, state, value_scope) - let polytype = generalise(u, state.substitutions, scope) + let polytype = generalise(u, state, scope) do_infer(then, expected, state, [#(label, polytype), ..scope]) } e.Variable(label) -> diff --git a/eyg/src/gleam/list.gleam b/eyg/src/gleam/list.gleam index 970ee68d1..5888fbbef 100644 --- a/eyg/src/gleam/list.gleam +++ b/eyg/src/gleam/list.gleam @@ -10,6 +10,13 @@ pub fn find(list: List(a), search: a) -> Result(a, Nil) { } } +pub fn contains(list: List(a), search: a) -> Bool { + case find(list, search) { + Ok(_) -> True + Error(Nil) -> False + } +} + /// Finds the first element in a given list for which the given function returns /// True. /// diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index 0c322d69a..246fbf046 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -68,42 +68,46 @@ pub fn binary_expression_test() { assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason } -// pub fn tuple_expression_test() { -// let source = tuple_([binary("Hello")]) -// let #(typed, checker) = infer(source, unbound()) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Tuple([t.Binary]) = type_ -// let #(typed, checker) = infer(source, t.Tuple([unbound()])) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Tuple([t.Binary]) = type_ -// let #(typed, checker) = infer(source, t.Tuple([t.Binary])) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Tuple([t.Binary]) = type_ -// let #(typed, checker) = infer(source, t.Tuple([])) -// assert Error(reason) = get_type(typed, checker) -// assert typer.IncorrectArity(0, 1) = reason -// let #(typed, checker) = infer(source, t.Tuple([t.Tuple([])])) -// // Type is correct here only internally is there a failure -// assert Ok(t.Tuple([t.Tuple([])])) = get_type(typed, checker) -// assert Ok(element) = get_expression(typed, [0]) -// assert Error(reason) = get_type(element, checker) -// assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason -// } -// pub fn pair_test() { -// let source = tuple_([binary("Hello"), tuple_([])]) -// let tx = t.Unbound(-1) -// let ty = t.Unbound(-2) -// let #(typed, checker) = infer(source, t.Tuple([tx, ty])) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Tuple([t.Binary, t.Tuple([])]) = type_ -// // could check tx/ty bound properly -// let #(typed, checker) = infer(source, t.Tuple([tx, tx])) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Tuple([t.Binary, t.Binary]) = type_ -// assert Ok(element) = get_expression(typed, [1]) -// assert Error(reason) = get_type(element, checker) -// assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason -// } +pub fn tuple_expression_test() { + let source = tuple_([binary("Hello")]) + let #(typed, checker) = infer(source, unbound()) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([t.Binary]) = type_ + let #(typed, checker) = infer(source, t.Tuple([unbound()])) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([t.Binary]) = type_ + let #(typed, checker) = infer(source, t.Tuple([t.Binary])) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([t.Binary]) = type_ + let #(typed, checker) = infer(source, t.Tuple([])) + assert Error(reason) = get_type(typed, checker) + assert typer.IncorrectArity(0, 1) = reason + let #(typed, checker) = infer(source, t.Tuple([t.Tuple([])])) + // Type is correct here only internally is there a failure + assert Ok(t.Tuple([t.Tuple([])])) = get_type(typed, checker) + // TODO + // assert Ok(element) = get_expression(typed, [0]) + // assert Error(reason) = get_type(element, checker) + // assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason +} + +pub fn pair_test() { + let source = tuple_([binary("Hello"), tuple_([])]) + let tx = t.Unbound(-1) + let ty = t.Unbound(-2) + let #(typed, checker) = infer(source, t.Tuple([tx, ty])) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([t.Binary, t.Tuple([])]) = type_ + // could check tx/ty bound properly + let #(typed, checker) = infer(source, t.Tuple([tx, tx])) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([t.Binary, t.Binary]) = type_ + // TODO + // assert Ok(element) = get_expression(typed, [1]) + // assert Error(reason) = get_type(element, checker) + // assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason +} + // pub fn row_expression_test() { // // TODO order when row is called // let source = row([#("foo", binary("Hello"))]) @@ -137,13 +141,14 @@ pub fn binary_expression_test() { // } // // TODO tag test // // TODO patterns -// pub fn var_expression_test() { -// let source = variable("x") -// let #(typed, checker) = infer(source, unbound()) -// assert Error(reason) = get_type(typed, checker) -// // TODO check we're on the lowest unbound integer -// assert typer.UnknownVariable("x") = reason -// } +pub fn var_expression_test() { + let source = variable("x") + let #(typed, checker) = infer(source, unbound()) + assert Error(reason) = get_type(typed, checker) + // TODO check we're on the lowest unbound integer + assert typer.UnknownVariable("x") = reason +} + // pub fn function_test() { // let source = function(p.Variable(""), binary("")) // let #(typed, checker) = infer(source, unbound()) From f74fbddfad62647c2ed09b8753e92931629a8abd Mon Sep 17 00:00:00 2001 From: Peter Date: Sat, 19 Feb 2022 19:43:47 +0100 Subject: [PATCH 11/18] recursion on resolving --- eyg/src/eyg/inference.gleam | 100 +++++++++++++++++++++++++--------- eyg/test/eyg/terms_test.gleam | 11 ++-- 2 files changed, 79 insertions(+), 32 deletions(-) diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index eb5757ec4..acb6f355f 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -41,13 +41,19 @@ pub fn do_unify( } fn add_substitution(i, type_, substitutions) { - // TODO occurs in check + // These checks arrive too late end up with reursive type only existing in first recursion // We assume i doesn't occur in substitutions - // list.contains(free_in_type(type_), i) - let type_ = case i == 2 { - True -> t.Recursive(i, type_) - False -> type_ - } + // let check = + // list.contains(free_in_type(do_resolve(type_, substitutions, [])), i) + // let type_ = case check { + // True -> { + // io.debug("============") + // io.debug(i) + // io.debug(type_) + // t.Recursive(i, type_) + // } + // False -> type_ + // } [#(i, type_), ..substitutions] } @@ -133,30 +139,50 @@ pub fn instantiate(poly, state) { #(t, state) } -// TODO tags/unions -// everything should be doable with resolve if we have a Recursive type -// When unifying Does recursion need to be someting that can move between substitutions -// When writing an annotation it would include recursive types -// List(B) = μA.[Null | Cons(B, A)] +pub fn do_reccuring_in_type(type_, found) { + todo +} + +pub fn recuring_in_type(type_) { + do_reccuring_in_type(type_, []) +} + pub fn print(t, state) { let type_ = resolve(t, state) - to_string(type_) + let #(rendered, _) = to_string(type_, []) + rendered } -fn to_string(t) { +pub fn to_string(t, used) { + // Having structural types would allow replacing integer variables with letter variables easily in a substitution + // a function to list variable types would allow a simple substitution + // A lot easier to debug if not using used as part of this case t { - t.Unbound(i) -> int.to_string(i) - t.Recursive(i, t) -> - string.join(["μ", int.to_string(i), ".", to_string(t)]) - t.Tuple(elements) -> - string.join([ - "(", - string.join(list.intersperse(list.map(elements, to_string), ", ")), - ")", - ]) - t.Binary -> "Binary" - t.Function(from, to) -> - string.join([to_string(from), " -> ", to_string(to)]) + t.Unbound(i) -> { + let used = push_new(i, used) + assert Ok(index) = index(used, i) + #(int.to_string(index), used) + } + t.Recursive(i, t) -> { + let used = push_new(i, used) + let #(inner, used) = to_string(t, used) + assert Ok(index) = index(used, i) + let rendered = string.join(["μ", int.to_string(index), ".", inner]) + #(rendered, used) + } + t.Tuple(elements) -> { + let #(rendered, used) = list.map_state(elements, used, to_string) + let rendered = + string.join(["(", string.join(list.intersperse(rendered, ", ")), ")"]) + #(rendered, used) + } + t.Binary -> #("Binary", used) + t.Function(from, to) -> { + let #(from, used) = to_string(from, used) + let #(to, used) = to_string(to, used) + let rendered = string.join([from, " -> ", to]) + #(rendered, used) + } } } @@ -169,9 +195,17 @@ pub fn do_resolve(type_, substitutions: List(#(Int, t.Monotype(n))), recuring) { case list.key_find(substitutions, i) { Ok(t.Unbound(j)) if i == j -> type_ Error(Nil) -> type_ - Ok(sub) -> do_resolve(sub, substitutions, recuring) + Ok(sub) -> { + let inner = do_resolve(sub, substitutions, [i, ..recuring]) + let recursive = list.contains(free_in_type(inner), i) + case recursive { + False -> inner + True -> t.Recursive(i, inner) + } + } } } + // This needs to exist as might already have been called by generalize t.Recursive(i, sub) -> { let inner = do_resolve(sub, substitutions, [i, ..recuring]) t.Recursive(i, inner) @@ -270,7 +304,6 @@ fn do_infer(untyped, expected, state, scope) { ) #(t, state) } - // e.Row(fields) -> { // } e.Function(p.Variable(label), body) -> { @@ -344,3 +377,16 @@ fn union(new: List(a), existing: List(a)) -> List(a) { } } } + +fn do_index(list, term, count) { + case list { + [] -> Error(Nil) + [item, .._] if item == term -> Ok(count) + [_, ..list] -> do_index(list, term, count + 1) + } +} + +// set index start from back +fn index(list, term) { + do_index(list.reverse(list), term, 0) +} diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index 246fbf046..156c5177b 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -397,19 +397,20 @@ pub fn my_recursive_tuple_test() { ) let #(Ok(typed), checker) = infer(source, unbound()) - io.debug("-=-------------------") + // io.debug("-=-------------------") // io.debug(typed) // list.map( // checker.substitutions, // fn(s) { // let #(k, t) = s // io.debug(k) - // io.debug(t.to_string(t, fn(_) { "OOO" })) + // // io.debug(t.to_string(t, fn(_) { "OOO" })) + // io.debug(inference.to_string(t, [])) // }, // ) - let "() -> μ2.(Binary, 2)" = - inference.print(typed, checker) - |> io.debug + let "() -> μ0.(Binary, 0)" = inference.print(typed, checker) + // inference.print(t.Unbound(4), checker) + // |> io.debug // assert Ok(t.Function(from, to)) = get_type(typed, checker) // assert t.Tuple([]) = from // // assert t.Tuple([t.Binary, t.Unbound(mu)]) = to From 2a6c007abbe9eaa3490b85f84b3deb5e36ffc8dd Mon Sep 17 00:00:00 2001 From: Peter Date: Sat, 19 Feb 2022 19:51:47 +0100 Subject: [PATCH 12/18] cleanup --- eyg/src/eyg/inference.gleam | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index acb6f355f..0761faa3c 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -64,10 +64,6 @@ fn unify(t1, t2, state: State(n)) { Ok(State(..state, substitutions: s)) } -pub fn lookup(env, label) { - todo -} - // relies on type having been resolved fn do_free_in_type(type_, set) { case type_ { @@ -139,14 +135,6 @@ pub fn instantiate(poly, state) { #(t, state) } -pub fn do_reccuring_in_type(type_, found) { - todo -} - -pub fn recuring_in_type(type_) { - do_reccuring_in_type(type_, []) -} - pub fn print(t, state) { let type_ = resolve(t, state) let #(rendered, _) = to_string(type_, []) @@ -311,9 +299,7 @@ fn do_infer(untyped, expected, state, scope) { let #(return, state) = fresh(state) case unify(expected, t.Function(arg, return), state) { Ok(state) -> - // let state = do_infer(body, return, state, [#(label, #([], arg)), ..scope]) - // #(Ok(expected), state) Error(reason) -> #(Error(reason), state) } } From 4bb7c9f1a3037a48342f4479ee75210fa0330100 Mon Sep 17 00:00:00 2001 From: Peter Date: Sat, 19 Feb 2022 20:05:20 +0100 Subject: [PATCH 13/18] keep tree --- eyg/src/eyg/inference.gleam | 39 +++++++++++++++++++++-------------- eyg/test/eyg/terms_test.gleam | 13 ++++++------ 2 files changed, 31 insertions(+), 21 deletions(-) diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index 0761faa3c..3a3c58fb3 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -258,10 +258,10 @@ pub fn infer(untyped, expected) { fn do_infer(untyped, expected, state, scope) { let #(_, expression) = untyped case expression { - e.Binary(_) -> + e.Binary(value) -> case unify(expected, t.Binary, state) { - Ok(state) -> #(Ok(expected), state) - Error(reason) -> #(Error(reason), state) + Ok(state) -> #(#(Ok(expected), e.Binary(value)), state) + Error(reason) -> #(#(Error(reason), e.Binary(value)), state) } e.Tuple(elements) -> { let #(with_type, state) = @@ -281,7 +281,7 @@ fn do_infer(untyped, expected, state, scope) { Ok(state) -> #(Ok(expected), state) Error(reason) -> #(Error(reason), state) } - let #(_, state) = + let #(elements, state) = list.map_state( with_type, state, @@ -290,43 +290,52 @@ fn do_infer(untyped, expected, state, scope) { do_infer(element, expected, state, scope) }, ) - #(t, state) + #(#(t, e.Tuple(elements)), state) } // e.Row(fields) -> { // } e.Function(p.Variable(label), body) -> { let #(arg, state) = fresh(state) let #(return, state) = fresh(state) - case unify(expected, t.Function(arg, return), state) { - Ok(state) -> - do_infer(body, return, state, [#(label, #([], arg)), ..scope]) + let #(body, state) = + do_infer(body, return, state, [#(label, #([], arg)), ..scope]) + let #(t, state) = case unify(expected, t.Function(arg, return), state) { + Ok(state) -> #(Ok(expected), state) Error(reason) -> #(Error(reason), state) } + #(#(t, e.Function(p.Variable(label), body)), state) } e.Call(func, with) -> { let #(arg, state) = fresh(state) - let #(_t, state) = do_infer(func, t.Function(arg, expected), state, scope) - do_infer(with, arg, state, scope) + let #(func, state) = + do_infer(func, t.Function(arg, expected), state, scope) + let #(with, state) = do_infer(with, arg, state, scope) + #(#(Ok(expected), e.Call(func, with)), state) } e.Let(p.Variable(label), value, then) -> { let #(u, state) = fresh(state) // TODO haandle self case or variable renaming let value_scope = [#(label, #([], u)), ..scope] - let #(_t, state) = do_infer(value, u, state, value_scope) + let #(value, state) = do_infer(value, u, state, value_scope) let polytype = generalise(u, state, scope) - do_infer(then, expected, state, [#(label, polytype), ..scope]) + let #(then, state) = + do_infer(then, expected, state, [#(label, polytype), ..scope]) + #(#(Ok(expected), e.Let(p.Variable(label), value, then)), state) } e.Variable(label) -> case list.key_find(scope, label) { Ok(polytype) -> { let #(monotype, state) = instantiate(polytype, state) case unify(expected, monotype, state) { - Ok(state) -> #(Ok(expected), state) - Error(reason) -> #(Error(reason), state) + Ok(state) -> #(#(Ok(expected), e.Variable(label)), state) + Error(reason) -> #(#(Error(reason), e.Variable(label)), state) } } - Error(Nil) -> #(Error(typer.UnknownVariable(label)), state) + Error(Nil) -> #( + #(Error(typer.UnknownVariable(label)), e.Variable(label)), + state, + ) } } } diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index 156c5177b..76d5388cf 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -35,6 +35,7 @@ fn unbound() { } fn get_type(typed, checker) { + let #(typed, tree) = typed case typed { Ok(type_) -> { let resolved = inference.resolve(type_, checker) @@ -85,10 +86,9 @@ pub fn tuple_expression_test() { let #(typed, checker) = infer(source, t.Tuple([t.Tuple([])])) // Type is correct here only internally is there a failure assert Ok(t.Tuple([t.Tuple([])])) = get_type(typed, checker) - // TODO - // assert Ok(element) = get_expression(typed, [0]) - // assert Error(reason) = get_type(element, checker) - // assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason + assert Ok(element) = get_expression(typed, [0]) + assert Error(reason) = get_type(element, checker) + assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason } pub fn pair_test() { @@ -395,7 +395,7 @@ pub fn my_recursive_tuple_test() { ), variable("f"), ) - let #(Ok(typed), checker) = infer(source, unbound()) + let #(typed, checker) = infer(source, unbound()) // io.debug("-=-------------------") // io.debug(typed) @@ -408,7 +408,8 @@ pub fn my_recursive_tuple_test() { // io.debug(inference.to_string(t, [])) // }, // ) - let "() -> μ0.(Binary, 0)" = inference.print(typed, checker) + let Ok(type_) = get_type(typed, checker) + let "() -> μ0.(Binary, 0)" = inference.print(type_, checker) // inference.print(t.Unbound(4), checker) // |> io.debug // assert Ok(t.Function(from, to)) = get_type(typed, checker) From 5342a24e1023749419ea5902f1fbf0706f1150e7 Mon Sep 17 00:00:00 2001 From: Peter Date: Sat, 19 Feb 2022 20:07:03 +0100 Subject: [PATCH 14/18] a bit more test --- eyg/test/eyg/terms_test.gleam | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index 76d5388cf..d64d33293 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -102,10 +102,9 @@ pub fn pair_test() { let #(typed, checker) = infer(source, t.Tuple([tx, tx])) assert Ok(type_) = get_type(typed, checker) assert t.Tuple([t.Binary, t.Binary]) = type_ - // TODO - // assert Ok(element) = get_expression(typed, [1]) - // assert Error(reason) = get_type(element, checker) - // assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason + assert Ok(element) = get_expression(typed, [1]) + assert Error(reason) = get_type(element, checker) + assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason } // pub fn row_expression_test() { From b2b19e987f7f249a0b66ca86930e8f8e7247a9d7 Mon Sep 17 00:00:00 2001 From: Peter Date: Sun, 20 Feb 2022 10:46:44 +0100 Subject: [PATCH 15/18] test row --- eyg/src/eyg/inference.gleam | 156 ++++++++++++++++++++++++---------- eyg/src/eyg/typer.gleam | 3 +- eyg/src/gleam/list.gleam | 21 +++++ eyg/test/eyg/terms_test.gleam | 65 +++++++------- 4 files changed, 169 insertions(+), 76 deletions(-) diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index 3a3c58fb3..fe4f7b934 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -1,5 +1,6 @@ import gleam/io import gleam/int +import gleam/option.{None, Some} import gleam/string import gleam/list import gleam/pair @@ -10,37 +11,52 @@ import eyg/typer pub fn do_unify( pair: #(t.Monotype(n), t.Monotype(n)), - substitutions: List(#(Int, t.Monotype(n))), -) -> Result(List(#(Int, t.Monotype(n))), typer.Reason(n)) { + state: State(n), +) -> Result(State(n), typer.Reason(n)) { let #(t1, t2) = pair case t1, t2 { - t.Unbound(i), t.Unbound(j) if i == j -> Ok(substitutions) + t.Unbound(i), t.Unbound(j) if i == j -> Ok(state) t.Unbound(i), _ -> - case list.key_find(substitutions, i) { - Ok(t1) -> do_unify(#(t1, t2), substitutions) - Error(Nil) -> Ok(add_substitution(i, t2, substitutions)) + case list.key_find(state.substitutions, i) { + Ok(t1) -> do_unify(#(t1, t2), state) + Error(Nil) -> Ok(add_substitution(i, t2, state)) } _, t.Unbound(j) -> - case list.key_find(substitutions, j) { - Ok(t2) -> do_unify(#(t1, t2), substitutions) - Error(Nil) -> Ok(add_substitution(j, t1, substitutions)) + case list.key_find(state.substitutions, j) { + Ok(t2) -> do_unify(#(t1, t2), state) + Error(Nil) -> Ok(add_substitution(j, t1, state)) } - t.Native(n1), t.Native(n2) if n1 == n2 -> Ok(substitutions) - t.Binary, t.Binary -> Ok(substitutions) + t.Native(n1), t.Native(n2) if n1 == n2 -> Ok(state) + t.Binary, t.Binary -> Ok(state) t.Tuple(e1), t.Tuple(e2) -> case list.zip(e1, e2) { - Ok(pairs) -> list.try_fold(pairs, substitutions, do_unify) + Ok(pairs) -> list.try_fold(pairs, state, do_unify) Error(#(c1, c2)) -> Error(typer.IncorrectArity(c1, c2)) } + t.Row(row1, extra1), t.Row(row2, extra2) -> { + let #(unmatched1, unmatched2, shared) = typer.group_shared(row1, row2) + let #(i, state) = fresh(state) + try state = case unmatched2, extra1 { + [], _ -> Ok(state) + only, Some(i) -> Ok(add_substitution(i, t.Row(only, Some(i)), state)) + only, None -> Error(typer.UnexpectedFields(only)) + } + try state = case unmatched1, extra2 { + [], _ -> Ok(state) + only, Some(i) -> Ok(add_substitution(i, t.Row(only, Some(i)), state)) + only, None -> Error(typer.MissingFields(only)) + } + list.try_fold(shared, state, do_unify) + } t.Function(from1, to1), t.Function(from2, to2) -> { - try substitutions = do_unify(#(from1, from2), substitutions) - do_unify(#(to1, to2), substitutions) + try state = do_unify(#(from1, from2), state) + do_unify(#(to1, to2), state) } _, _ -> Error(typer.UnmatchedTypes(t1, t2)) } } -fn add_substitution(i, type_, substitutions) { +fn add_substitution(i, type_, state: State(n)) -> State(n) { // These checks arrive too late end up with reursive type only existing in first recursion // We assume i doesn't occur in substitutions // let check = @@ -54,14 +70,16 @@ fn add_substitution(i, type_, substitutions) { // } // False -> type_ // } - [#(i, type_), ..substitutions] + let substitutions = [#(i, type_), ..state.substitutions] + State(..state, substitutions: substitutions) } fn unify(t1, t2, state: State(n)) { - let State(substitutions: s, ..) = state - try s = do_unify(#(t1, t2), s) - // TODO add errors here - Ok(State(..state, substitutions: s)) + // let State(substitutions: s, ..) = state + // try s = do_unify(#(t1, t2), s) + // // TODO add errors here + // Ok(State(..state, substitutions: s)) + do_unify(#(t1, t2), state) } // relies on type having been resolved @@ -70,11 +88,27 @@ fn do_free_in_type(type_, set) { t.Unbound(i) -> push_new(i, set) t.Native(_) | t.Binary -> set t.Tuple(elements) -> list.fold(elements, set, do_free_in_type) + t.Row(fields, rest) -> { + let set = + list.fold( + fields, + set, + fn(field, set) { + let #(_name, type_) = field + do_free_in_type(type_, set) + }, + ) + case rest { + None -> set + // Already resolved + Some(i) -> push_new(i, set) + } + } t.Recursive(i, type_) -> { let inner = do_free_in_type(type_, set) difference(inner, [i]) } - // Row + t.Function(from, to) -> { let set = do_free_in_type(from, set) do_free_in_type(to, set) @@ -203,27 +237,27 @@ pub fn do_resolve(type_, substitutions: List(#(Int, t.Monotype(n))), recuring) { let elements = list.map(elements, do_resolve(_, substitutions, recuring)) t.Tuple(elements) } - // Row(fields, rest) -> { - // let resolved_fields = - // list.map( - // fields, - // fn(field) { - // let #(name, type_) = field - // #(name, do_resolve(type_, substitutions)) - // }, - // ) - // case rest { - // None -> Row(resolved_fields, None) - // Some(i) -> { - // type_ - // case do_resolve(Unbound(i), substitutions) { - // Unbound(j) -> Row(resolved_fields, Some(j)) - // Row(inner, rest) -> Row(list.append(resolved_fields, inner), rest) - // } - // } - // } - // } - // TODO check do_resolve in our record based recursive frunctions + t.Row(fields, rest) -> { + let resolved_fields = + list.map( + fields, + fn(field) { + let #(name, type_) = field + #(name, do_resolve(type_, substitutions, recuring)) + }, + ) + case rest { + None -> t.Row(resolved_fields, None) + Some(i) -> { + type_ + case do_resolve(t.Unbound(i), substitutions, recuring) { + t.Unbound(j) -> t.Row(resolved_fields, Some(j)) + t.Row(inner, rest) -> + t.Row(list.append(resolved_fields, inner), rest) + } + } + } + } t.Function(from, to) -> { let from = do_resolve(from, substitutions, recuring) let to = do_resolve(to, substitutions, recuring) @@ -292,8 +326,42 @@ fn do_infer(untyped, expected, state, scope) { ) #(#(t, e.Tuple(elements)), state) } - // e.Row(fields) -> { - // } + e.Row(fields) -> { + // This approach fails because the fresh type is not available later + // let #(fields, state) = list.map_state(fields, state, fn(field, state) { + // let #(name, untyped) = field + // let #(type_, state) = fresh(state) + // let #(typed, state) = do_infer(untyped, type_, state, scope) + // #(#(name, typed), state) + // }) + // let field_types = list.map(fields, fn(field) { + // let #(name, typed) = field + // let #(Ok(type_), _tree) = typed + // #(name, type_) + // }) + // let given = t.Row(field_types, None) + // #(#(Ok(t.Tuple([])), e.Binary("")), state) + let #(pairs, state) = + list.map_state( + fields, + state, + fn(field, state) { + let #(name, untyped) = field + let #(expected, state) = fresh(state) + let row_type = #(name, expected) + let #(typed, state) = do_infer(untyped, expected, state, scope) + let typed_row = #(name, typed) + #(#(row_type, typed_row), state) + }, + ) + let #(row_types, typed_rows) = list.unzip(pairs) + let given = t.Row(row_types, None) + let #(t, state) = case unify(expected, given, state) { + Ok(state) -> #(Ok(expected), state) + Error(reason) -> #(Error(reason), state) + } + #(#(t, e.Row(typed_rows)), state) + } e.Function(p.Variable(label), body) -> { let #(arg, state) = fresh(state) let #(return, state) = fresh(state) diff --git a/eyg/src/eyg/typer.gleam b/eyg/src/eyg/typer.gleam index ac5835443..4e00af1a2 100644 --- a/eyg/src/eyg/typer.gleam +++ b/eyg/src/eyg/typer.gleam @@ -237,7 +237,8 @@ pub fn unify(expected, given, state) { // } } -fn group_shared(left, right) { +// TODO test in list +pub fn group_shared(left, right) { do_group_shared(left, right, [], []) } diff --git a/eyg/src/gleam/list.gleam b/eyg/src/gleam/list.gleam index 5888fbbef..93f0c9f7c 100644 --- a/eyg/src/gleam/list.gleam +++ b/eyg/src/gleam/list.gleam @@ -17,6 +17,27 @@ pub fn contains(list: List(a), search: a) -> Bool { } } +fn do_unzip(input, xs, ys) { + case input { + [] -> #(reverse(xs), reverse(ys)) + [#(x, y), ..rest] -> do_unzip(rest, [x, ..xs], [y, ..ys]) + } +} + +/// Takes a single list of 2-element tuples and returns two lists. +/// +/// ## Examples +/// +/// > unzip([#(1, 2), #(3, 4)]) +/// #([1, 3], [2, 4]) +/// +/// > unzip([]) +/// #([], []) +/// +pub fn unzip(input: List(#(a, b))) -> #(List(a), List(b)) { + do_unzip(input, [], []) +} + /// Finds the first element in a given list for which the given function returns /// True. /// diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index d64d33293..82c144d68 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -107,37 +107,40 @@ pub fn pair_test() { assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason } -// pub fn row_expression_test() { -// // TODO order when row is called -// let source = row([#("foo", binary("Hello"))]) -// let #(typed, checker) = infer(source, unbound()) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Row([#("foo", t.Binary)], None) = type_ -// let #(typed, checker) = infer(source, t.Row([#("foo", t.Binary)], None)) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Row([#("foo", t.Binary)], None) = type_ -// // TODO row with some -// let #(typed, checker) = -// infer(source, t.Row([#("foo", t.Binary), #("bar", t.Binary)], None)) -// assert Error(reason) = get_type(typed, checker) -// assert typer.MissingFields([#("bar", t.Binary)]) = reason -// let #(typed, checker) = infer(source, t.Row([], None)) -// assert Error(reason) = get_type(typed, checker) -// // assert typer.UnexpectedFields([#("foo", t.Binary)]) = reason -// // TODO move up -// let #(typed, checker) = infer(source, t.Row([#("foo", t.Tuple([]))], None)) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Row([#("foo", t.Tuple([]))], None) = type_ -// assert Ok(element) = get_expression(typed, [0, 1]) -// assert Error(reason) = get_type(element, checker) -// assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason -// // T.Row(head, option(more_row)) -// // Means no such thing as an empty record. Good because tuple is unit -// let #(typed, checker) = infer(source, t.Row([#("foo", t.Binary)], Some(-1))) -// assert Ok(type_) = get_type(typed, checker) -// // TODO should resolve to none -// // assert t.Row([#("foo", t.Binary)], None) = type_ -// } +pub fn row_expression_test() { + // TODO order when row is called + let source = row([#("foo", binary("Hello"))]) + let #(typed, checker) = infer(source, unbound()) + assert Ok(type_) = get_type(typed, checker) + assert t.Row([#("foo", t.Binary)], None) = type_ + let #(typed, checker) = infer(source, t.Row([#("foo", t.Binary)], None)) + assert Ok(type_) = get_type(typed, checker) + assert t.Row([#("foo", t.Binary)], None) = type_ + // TODO row with some + let #(typed, checker) = + infer(source, t.Row([#("foo", t.Binary), #("bar", t.Binary)], None)) + assert Error(reason) = get_type(typed, checker) + assert typer.MissingFields([#("bar", t.Binary)]) = reason + let #(typed, checker) = infer(source, t.Row([], None)) + assert Error(reason) = get_type(typed, checker) + // assert typer.UnexpectedFields([#("foo", t.Binary)]) = reason + // TODO move up + let #(typed, checker) = infer(source, t.Row([#("foo", t.Tuple([]))], None)) + // TODO think which one I want most. + // assert Ok(type_) = get_type(typed, checker) + // assert t.Row([#("foo", t.Tuple([]))], None) = type_ + // assert Ok(element) = get_expression(typed, [0, 1]) + // assert Error(reason) = get_type(element, checker) + // assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason + // ----- up to previous todo + // T.Row(head, option(more_row)) + // Means no such thing as an empty record. Good because tuple is unit + let #(typed, checker) = infer(source, t.Row([#("foo", t.Binary)], Some(-1))) + assert Ok(type_) = get_type(typed, checker) + // TODO should resolve to none + // assert t.Row([#("foo", t.Binary)], None) = type_ +} + // // TODO tag test // // TODO patterns pub fn var_expression_test() { From b13f39477c46082a7726429b90ccc4b1965e9ca1 Mon Sep 17 00:00:00 2001 From: Peter Date: Sun, 20 Feb 2022 10:51:32 +0100 Subject: [PATCH 16/18] more tests --- eyg/src/eyg/inference.gleam | 4 +- eyg/test/eyg/terms_test.gleam | 149 ++++++++++++++++++---------------- 2 files changed, 79 insertions(+), 74 deletions(-) diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index fe4f7b934..303a68a1d 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -365,12 +365,12 @@ fn do_infer(untyped, expected, state, scope) { e.Function(p.Variable(label), body) -> { let #(arg, state) = fresh(state) let #(return, state) = fresh(state) - let #(body, state) = - do_infer(body, return, state, [#(label, #([], arg)), ..scope]) let #(t, state) = case unify(expected, t.Function(arg, return), state) { Ok(state) -> #(Ok(expected), state) Error(reason) -> #(Error(reason), state) } + let #(body, state) = + do_infer(body, return, state, [#(label, #([], arg)), ..scope]) #(#(t, e.Function(p.Variable(label), body)), state) } e.Call(func, with) -> { diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index 82c144d68..3af5d940a 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -151,52 +151,55 @@ pub fn var_expression_test() { assert typer.UnknownVariable("x") = reason } -// pub fn function_test() { -// let source = function(p.Variable(""), binary("")) -// let #(typed, checker) = infer(source, unbound()) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Function(t.Unbound(_), t.Binary) = type_ -// let #(typed, checker) = infer(source, t.Function(unbound(), t.Unbound(-2))) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Function(t.Unbound(_), t.Binary) = type_ -// let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Binary)) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Function(t.Tuple([]), t.Binary) = type_ -// let #(typed, checker) = infer(source, t.Function(unbound(), unbound())) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Function(t.Binary, t.Binary) = type_ -// let #(typed, checker) = infer(source, t.Binary) -// assert Error(reason) = get_type(typed, checker) -// // assert typer.UnmatchedTypes(t.Binary, t.Function(t.Unbound(_), t.Tuple([]))) = -// // reason -// // TODO move up -// let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Tuple([]))) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Function(t.Tuple([]), t.Tuple([])) = type_ -// assert Ok(body) = get_expression(typed, [1]) -// assert Error(reason) = get_type(body, checker) -// assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason -// } -// pub fn id_function_test() { -// let source = function(p.Variable("x"), variable("x")) -// let #(typed, checker) = infer(source, unbound()) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Function(t.Unbound(i), t.Unbound(j)) = type_ -// assert True = i == j -// let #(typed, checker) = infer(source, t.Function(unbound(), t.Binary)) -// assert Ok(type_) = get_type(typed, checker) -// // TODO check unbound is now binary -// assert t.Function(t.Binary, t.Binary) = type_ -// let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Binary)) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Function(t.Tuple([]), t.Binary) = type_ -// assert Ok(body) = get_expression(typed, [1]) -// assert Error(reason) = get_type(body, checker) -// assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason -// // Not this is saying that the variable is wrong some how -// } +pub fn function_test() { + let source = function(p.Variable(""), binary("")) + let #(typed, checker) = infer(source, unbound()) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Unbound(_), t.Binary) = type_ + let #(typed, checker) = infer(source, t.Function(unbound(), t.Unbound(-2))) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Unbound(_), t.Binary) = type_ + let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Binary)) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Tuple([]), t.Binary) = type_ + let #(typed, checker) = infer(source, t.Function(unbound(), unbound())) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Binary, t.Binary) = type_ + let #(typed, checker) = infer(source, t.Binary) + assert Error(reason) = get_type(typed, checker) + // assert typer.UnmatchedTypes(t.Binary, t.Function(t.Unbound(_), t.Tuple([]))) = + // reason + // TODO move up + let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Tuple([]))) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Tuple([]), t.Tuple([])) = type_ + assert Ok(body) = get_expression(typed, [1]) + assert Error(reason) = get_type(body, checker) + assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason +} + +pub fn id_function_test() { + let source = function(p.Variable("x"), variable("x")) + let #(typed, checker) = infer(source, unbound()) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Unbound(i), t.Unbound(j)) = type_ + assert True = i == j + let #(typed, checker) = infer(source, t.Function(unbound(), t.Binary)) + assert Ok(type_) = get_type(typed, checker) + // TODO check unbound is now binary + assert t.Function(t.Binary, t.Binary) = type_ + let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Binary)) + assert Ok(type_) = get_type(typed, checker) + assert t.Function(t.Tuple([]), t.Binary) = type_ + assert Ok(body) = get_expression(typed, [1]) + assert Error(reason) = get_type(body, checker) + assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason + // Not this is saying that the variable is wrong some how +} + // // equal bin bin // // equal bin tuple still returns true +// TODO patterns in arguments // pub fn call_function_test() { // let func = function(p.Tuple([]), binary("")) // let source = call(func, tuple_([])) @@ -211,34 +214,36 @@ pub fn var_expression_test() { // // assert Error(reason) = get_type(typed, checker) // // assert typer.UnmatchedTypes(t.Tuple([]), t.Tuple([])) = reason // } -// pub fn call_generic_function_test() { -// let func = function(p.Variable("x"), variable("x")) -// let source = call(func, tuple_([])) -// let #(typed, checker) = infer(source, unbound()) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Tuple([]) = type_ -// let #(typed, checker) = infer(source, t.Tuple([])) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Tuple([]) = type_ -// // error in generic pushed to arguments -// let #(typed, checker) = infer(source, t.Binary) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Binary = type_ -// assert Ok(body) = get_expression(typed, [1]) -// assert Error(reason) = get_type(body, checker) -// assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason -// } -// pub fn call_not_a_function_test() { -// let source = call(binary("no a func"), tuple_([])) -// let #(typed, checker) = infer(source, t.Binary) -// assert Ok(type_) = get_type(typed, checker) -// assert t.Binary = type_ -// assert Ok(body) = get_expression(typed, [0]) -// assert Error(reason) = get_type(body, checker) -// assert typer.UnmatchedTypes(expected, t.Binary) = reason -// // TODO resolve expected -// // assert t.Function(t.Tuple([]), t.Binary) = expected -// } +pub fn call_generic_function_test() { + let func = function(p.Variable("x"), variable("x")) + let source = call(func, tuple_([])) + let #(typed, checker) = infer(source, unbound()) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([]) = type_ + let #(typed, checker) = infer(source, t.Tuple([])) + assert Ok(type_) = get_type(typed, checker) + assert t.Tuple([]) = type_ + // error in generic pushed to arguments + let #(typed, checker) = infer(source, t.Binary) + assert Ok(type_) = get_type(typed, checker) + assert t.Binary = type_ + assert Ok(body) = get_expression(typed, [1]) + assert Error(reason) = get_type(body, checker) + assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason +} + +pub fn call_not_a_function_test() { + let source = call(binary("no a func"), tuple_([])) + let #(typed, checker) = infer(source, t.Binary) + assert Ok(type_) = get_type(typed, checker) + assert t.Binary = type_ + assert Ok(body) = get_expression(typed, [0]) + assert Error(reason) = get_type(body, checker) + assert typer.UnmatchedTypes(expected, t.Binary) = reason + // TODO resolve expected + // assert t.Function(t.Tuple([]), t.Binary) = expected +} + // pub fn hole_expression_test() { // let source = hole() // let #(typed, checker) = infer(source, unbound()) From 04fbd432852ef46c999ba60dfd0ad5b255848f4b Mon Sep 17 00:00:00 2001 From: Peter Date: Sun, 20 Feb 2022 11:12:55 +0100 Subject: [PATCH 17/18] implement tag and union type --- eyg/src/eyg/ast/expression.gleam | 12 ++++-- eyg/src/eyg/inference.gleam | 69 ++++++++++++++++++++++++-------- eyg/src/eyg/typer/monotype.gleam | 2 + eyg/test/eyg/terms_test.gleam | 9 ++++- 4 files changed, 70 insertions(+), 22 deletions(-) diff --git a/eyg/src/eyg/ast/expression.gleam b/eyg/src/eyg/ast/expression.gleam index f5674686f..26c5fe337 100644 --- a/eyg/src/eyg/ast/expression.gleam +++ b/eyg/src/eyg/ast/expression.gleam @@ -57,10 +57,9 @@ pub fn example(config, hole) { } } -fn tagged(name, value) { - function(p.Row([#(name, "then")]), call(variable("then"), value)) -} - +// fn tagged(name, value) { +// function(p.Row([#(name, "then")]), call(variable("then"), value)) +// } pub fn lift_type(_config, hole) { case hole { t.Function(from, _to) -> { @@ -154,6 +153,7 @@ pub type Node(m, g) { Binary(value: String) Tuple(elements: List(Expression(m, g))) Row(fields: List(#(String, Expression(m, g)))) + Tagged(tag: String, value: Expression(m, g)) Variable(label: String) Let(pattern: Pattern, value: Expression(m, g), then: Expression(m, g)) Function(pattern: Pattern, body: Expression(m, g)) @@ -197,6 +197,10 @@ pub fn row(fields) { #(dynamic.from(Nil), Row(fields)) } +pub fn tagged(tag, value) { + #(dynamic.from(Nil), Tagged(tag, value)) +} + pub fn hole() { #(dynamic.from(Nil), Hole) } diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index 303a68a1d..cff9decbf 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -88,27 +88,11 @@ fn do_free_in_type(type_, set) { t.Unbound(i) -> push_new(i, set) t.Native(_) | t.Binary -> set t.Tuple(elements) -> list.fold(elements, set, do_free_in_type) - t.Row(fields, rest) -> { - let set = - list.fold( - fields, - set, - fn(field, set) { - let #(_name, type_) = field - do_free_in_type(type_, set) - }, - ) - case rest { - None -> set - // Already resolved - Some(i) -> push_new(i, set) - } - } + t.Row(rows, rest) | t.Union(rows, rest) -> do_free_in_row(rows, rest, set) t.Recursive(i, type_) -> { let inner = do_free_in_type(type_, set) difference(inner, [i]) } - t.Function(from, to) -> { let set = do_free_in_type(from, set) do_free_in_type(to, set) @@ -116,6 +100,23 @@ fn do_free_in_type(type_, set) { } } +fn do_free_in_row(rows, rest, set) { + let set = + list.fold( + rows, + set, + fn(row, set) { + let #(_name, type_) = row + do_free_in_type(type_, set) + }, + ) + case rest { + None -> set + // Already resolved + Some(i) -> push_new(i, set) + } +} + pub fn free_in_type(t) { do_free_in_type(t, []) } @@ -258,6 +259,28 @@ pub fn do_resolve(type_, substitutions: List(#(Int, t.Monotype(n))), recuring) { } } } + t.Union(variants, rest) -> { + let resolved_variants = + // TODO map_value would help or a resolve_named unify_named etc probably also sensible + list.map( + variants, + fn(variant) { + let #(name, type_) = variant + #(name, do_resolve(type_, substitutions, recuring)) + }, + ) + case rest { + None -> t.Union(resolved_variants, None) + Some(i) -> { + type_ + case do_resolve(t.Unbound(i), substitutions, recuring) { + t.Unbound(j) -> t.Union(resolved_variants, Some(j)) + t.Union(inner, rest) -> + t.Union(list.append(resolved_variants, inner), rest) + } + } + } + } t.Function(from, to) -> { let from = do_resolve(from, substitutions, recuring) let to = do_resolve(to, substitutions, recuring) @@ -362,6 +385,18 @@ fn do_infer(untyped, expected, state, scope) { } #(#(t, e.Row(typed_rows)), state) } + e.Tagged(tag, value) -> { + let #(i, state) = fresh(state) + let #(t.Unbound(j), state) = fresh(state) + let given = t.Union([#(tag, i)], Some(j)) + let #(t, state) = case unify(expected, given, state) { + Ok(state) -> #(Ok(expected), state) + Error(reason) -> #(Error(reason), state) + } + let #(typed, state) = do_infer(value, i, state, scope) + #(#(t, e.Tagged(tag, typed)), state) + } + e.Function(p.Variable(label), body) -> { let #(arg, state) = fresh(state) let #(return, state) = fresh(state) diff --git a/eyg/src/eyg/typer/monotype.gleam b/eyg/src/eyg/typer/monotype.gleam index 7256f013b..f0799cf08 100644 --- a/eyg/src/eyg/typer/monotype.gleam +++ b/eyg/src/eyg/typer/monotype.gleam @@ -8,7 +8,9 @@ pub type Monotype(n) { Native(n) Binary Tuple(elements: List(Monotype(n))) + // TODO rename Record Row(fields: List(#(String, Monotype(n))), extra: Option(Int)) + Union(variants: List(#(String, Monotype(n))), extra: Option(Int)) Function(from: Monotype(n), to: Monotype(n)) Unbound(i: Int) Recursive(i: Int, type_: Monotype(n)) diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index 3af5d940a..ca3b40ea5 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -5,7 +5,7 @@ import eyg import eyg/ast import eyg/ast/editor import eyg/ast/expression.{ - binary, call, function, hole, let_, row, tuple_, variable, + binary, call, function, hole, let_, row, tagged, tuple_, variable, } import eyg/typer import eyg/ast/expression as e @@ -141,6 +141,13 @@ pub fn row_expression_test() { // assert t.Row([#("foo", t.Binary)], None) = type_ } +pub fn tag_test() { + let source = tagged("None", tuple_([])) + let #(typed, checker) = infer(source, unbound()) + assert Ok(type_) = get_type(typed, checker) + assert t.Union([#("None", t.Tuple([]))], Some(_)) = type_ +} + // // TODO tag test // // TODO patterns pub fn var_expression_test() { From 885605a1c54a1ffa4bcf882ec4f7815683c8fd0b Mon Sep 17 00:00:00 2001 From: Peter Date: Sun, 20 Feb 2022 11:27:07 +0100 Subject: [PATCH 18/18] test union more --- eyg/src/eyg/ast/editor.gleam | 3 +++ eyg/src/eyg/inference.gleam | 9 ++++++++- eyg/test/eyg/terms_test.gleam | 33 +++++++++++++++++++++++++++++++-- 3 files changed, 42 insertions(+), 3 deletions(-) diff --git a/eyg/src/eyg/ast/editor.gleam b/eyg/src/eyg/ast/editor.gleam index e37b3e827..ba42e8307 100644 --- a/eyg/src/eyg/ast/editor.gleam +++ b/eyg/src/eyg/ast/editor.gleam @@ -1603,6 +1603,9 @@ pub fn get_element(tree: e.Expression(a, b), position) -> Element(a, b) { let [#(_, child), .._] = list.drop(fields, i) get_element(child, rest) } + // TODO need to get out the union tag + #(_, e.Tagged(_tag, value)), [1, ..rest] -> get_element(value, rest) + #(_, e.Let(pattern, _, _)), [0, ..rest] -> get_pattern(pattern, rest, tree) #(_, e.Let(_, value, _)), [1, ..rest] -> get_element(value, rest) #(_, e.Let(_, _, then)), [2, ..rest] -> get_element(then, rest) diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam index cff9decbf..73996877a 100644 --- a/eyg/src/eyg/inference.gleam +++ b/eyg/src/eyg/inference.gleam @@ -33,7 +33,12 @@ pub fn do_unify( Ok(pairs) -> list.try_fold(pairs, state, do_unify) Error(#(c1, c2)) -> Error(typer.IncorrectArity(c1, c2)) } - t.Row(row1, extra1), t.Row(row2, extra2) -> { + // Is the type only ever Row. I think not it's Record Record and Union Union + // TODO t.Record(r1) + t.Row(row1, extra1), t.Row(row2, extra2) | t.Union(row1, extra1), t.Union( + row2, + extra2, + ) -> { let #(unmatched1, unmatched2, shared) = typer.group_shared(row1, row2) let #(i, state) = fresh(state) try state = case unmatched2, extra1 { @@ -199,6 +204,8 @@ pub fn to_string(t, used) { string.join(["(", string.join(list.intersperse(rendered, ", ")), ")"]) #(rendered, used) } + // TODO used first fn used variable names + t.Union(_, _) -> #("UNION", used) t.Binary -> #("Binary", used) t.Function(from, to) -> { let #(from, used) = to_string(from, used) diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam index ca3b40ea5..5184a57d8 100644 --- a/eyg/test/eyg/terms_test.gleam +++ b/eyg/test/eyg/terms_test.gleam @@ -142,10 +142,39 @@ pub fn row_expression_test() { } pub fn tag_test() { - let source = tagged("None", tuple_([])) + let source = tagged("Some", tuple_([])) + + // Unbound let #(typed, checker) = infer(source, unbound()) assert Ok(type_) = get_type(typed, checker) - assert t.Union([#("None", t.Tuple([]))], Some(_)) = type_ + assert t.Union([#("Some", t.Tuple([]))], Some(_)) = type_ + + // Part of Option + let #(typed, checker) = + infer( + source, + t.Union([#("Some", t.Tuple([])), #("None", t.Tuple([]))], None), + ) + assert Ok(type_) = get_type(typed, checker) + assert t.Union([#("Some", t.Tuple([])), #("None", t.Tuple([]))], None) = type_ + io.debug(inference.print(type_, checker)) + + // Mismatched type + let #(typed, checker) = + infer(source, t.Union([#("Some", t.Binary), #("None", t.Tuple([]))], None)) + assert Ok(type_) = get_type(typed, checker) + // TODO expected option of A or A + assert Ok(element) = get_expression(typed, [1]) + assert Error(reason) = get_type(element, checker) + assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason + // assert t.Union([#("Some", t.Tuple([]))], Some(_)) = type_ + // wrong variant + // union Foo + let #(typed, checker) = infer(source, t.Union([#("Foo", t.Tuple([]))], None)) + assert Error(reason) = get_type(typed, checker) + assert typer.UnexpectedFields(a) = reason + io.debug(a) + // io.debug(b) } // // TODO tag test