Module: Jade::Frontend::TypeChecking::Inference::Lambda

Extended by:
Helpers, Lambda
Included in:
Lambda
Defined in:
lib/jade/frontend/type_checking/inference/lambda.rb

Instance Method Summary collapse

Methods included from Helpers

check, generalize, instantiate, type_from_symbol, unify

Instance Method Details

#infer(node, registry, state, expected) ⇒ Object 



9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
 
# File 'lib/jade/frontend/type_checking/inference/lambda.rb', line 9

def infer(node, registry, state, expected)
  node => AST::Lambda(body:, params:)

  params_types = params.map { state.fresh }

  pre_state = state
    .unify_result(
      Result.init(Type.function(params_types, state.fresh)),
      expected.type,
      &type_error(state, node)
    )
    .first

  params_state = params
    .zip(params_types)
    .reduce(pre_state) do |acc, (p, t)|
      case p
      in AST::Pattern::Binding(name:)
        pre_state.env.substitution.apply(t)
          .then do |concrete_t|
            acc.bind(name, Scheme.mono(concrete_t))
              .then { it.with(env: it.env.pin_type(p.id, concrete_t)) }
          end

      in AST::Pattern::Wildcard
        acc

      else
        pre_state.env.substitution.apply(t)
          .then { Pattern.infer(p, registry, acc, Expected.check(it)) }
          .first
      end
    end

  body_state, body_result = check(
    body,
    registry,
    params_state,
    Expected.infer(params_state.fresh),
  )

  exhaustiveness_state = params
    .zip(params_types)
    .reduce(body_state) do |acc, (p, t)|
      case p
      in AST::Pattern::Binding | AST::Pattern::Wildcard
        acc
      else
        concrete_t = body_state.env.substitution.apply(t)
        PatternAnalysis::Exhaustiveness
          .assert([p], p.range, acc.env, registry, concrete_t)
          .then { acc.add_errors(it) }
      end
    end

  Type
    .function(params_types, body_result.type)
    .then { Result.init(it, body_result.constraints) }
    .apply(exhaustiveness_state.env.substitution)
    .then { exhaustiveness_state.unify_result(it, expected.type, &type_error(exhaustiveness_state, node)) }
end