Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Spike of recursion #35

Open
wants to merge 18 commits into
base: main
Choose a base branch
from
Prev Previous commit
Next Next commit
big recursion spike
  • Loading branch information
CrowdHailer committed Feb 8, 2022
commit 2bd4af631f478c485fc62fa990ebf4ad08508d96
100 changes: 49 additions & 51 deletions eyg/src/eyg/typer.gleam
Original file line number Diff line number Diff line change
@@ -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) {
17 changes: 13 additions & 4 deletions eyg/src/eyg/typer/monotype.gleam
Original file line number Diff line number Diff line change
@@ -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) -> {
6 changes: 6 additions & 0 deletions eyg/src/eyg/typer/polytype.gleam
Original file line number Diff line number Diff line change
@@ -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)
}
}

101 changes: 0 additions & 101 deletions eyg/test/eyg/patterns_test.gleam
Original file line number Diff line number Diff line change
@@ -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([
Loading