Katkat
Back

Implement type AST and infer generics

OpenAISoftware Engineer · Technical Screen
HardSoftware EngineerTechnical ScreenCoding & Algorithms

Last updated

This problem tests your ability to design a recursive data structure for an abstract syntax tree and implement a unification-based type inference engine for a simple functional language.

Problem Statement

Design a mini-type system for expressions containing variables, function abstractions (lambdas), and application. Your task is to implement a TypeInferencer class that represents these expressions as an AST and performs Hindley-Milner style type inference.

AST Definition

The language supports:

  • Variables: Var(name)
  • Abstractions: Abs(param_name, body_expr)
  • Applications: App(function_expr, argument_expr)

Requirements

Implement the function infer(expr) which returns the most general type of the given expression, or raises an UnificationError if a conflict occurs (e.g., trying to use a variable as both a function and an integer). Use type variables (e.g., T0, T1) for unknown types and arrows (T_in -> T_out) for function types.

Signature

class TypeInferencer:
    def infer(self, expr) -> str:
        # Returns string representation, e.g., "(T0 -> T0)"
        pass

Examples

  1. Identity function: Abs("x", Var("x")) should return "(T0 -> T0)".
  2. Self-application: Abs("x", App(Var("x"), Var("x"))) should raise an UnificationError as it is not typable in this system.

Constraints

  • Expressions are finite trees.
  • You must handle nested scoping.
  • You may assume basic variable names are unique if shadowed, or handle renaming to avoid collisions.

Hints

Hint 1

Represent types as a tree structure where a type is either a base type variable or a function type consisting of two sub-types.

Hint 2

Use a union-find data structure or a substitution map to keep track of type equivalencies discovered during recursive tree traversal.

Hint 3

During the inference of an application node, enforce that the type of the function must unify with a mapping from the argument type to a fresh return type variable.

Follow-up questions

  • How would you modify your system to support polymorphic let-bindings (let x = e1 in e2)?
  • What are the performance implications of the current unification algorithm, and can you bound the complexity?
  • How would you extend this system to support basic primitive types like integers and booleans?