타입 검사 핵심 함수

• synthesize(expr, context): 표현식의 타입을 추론하고 업데이트된 컨텍스트를 반환합니다.

• check(expr, type, context): 표현식이 예상 타입과 호환되는지 검사하고 업데이트된 컨텍스트를 반환합니다.

• 이 두 함수는 서로 재귀적으로 호출되며 타입 해소의 핵심 역할을 수행합니다.

언어 구성 요소 및 타입 정의

• Expression 모듈: LiteralInt, LiteralString, Variable, Annotation, Lambda, Application 등 다양한 구문 요소를 정의합니다.

• Type 모듈: Int, String, Variable, Existential, Lambda, Quantification 등 해당 구문 요소에 대응하는 타입들을 정의합니다.

컨텍스트(Context) 관리

• 컨텍스트는 변수, 함수, 타입 변수 등 심볼과 그 타입을 저장하는 리스트 기반의 자료구조입니다.

• Context::Element: TypedVariable, UnsolvedExistential, SolvedExistential, Marker 등 컨텍스트 내 요소를 정의합니다.

• 주요 컨텍스트 메서드: lookup, push, split, replace, apply 등이 구현됩니다.

핵심 타입 규칙 구현 과정

• 리터럴, 변수, 주석: synthesize 및 check 함수를 통해 기본적인 타입 추론 및 검증을 처리합니다. type_well_formed?로 타입 유효성을 검사합니다.

• 람다 및 존재 타입: 람다 합성 시 fresh_name으로 존재 타입을 생성하며, 이는 아직 결정되지 않은 타입의 플레이스홀더입니다. 존재 타입은 타입 검사 과정에서 해결됩니다.

• 서브타이핑 및 인스턴스화: subtype 함수로 타입 호환성을 정의하고, `Context

apply로 해결된 존재 변수를 타입에 적용합니다. occurs?로 순환 타입을 방지하며, instantiate_right와 instantiate_left`로 존재 타입을 구체적인 타입으로 해결합니다.

• 범용 타입(Quantification): Type::Quantification을 통해 forall a. A -> A와 같은 고차 다형성을 지원하며, 관련 함수들을 업데이트합니다. substitute 함수로 타입 변수를 대체합니다.

• 함수 적용(Application): synthesize_application 함수를 통해 함수 호출의 타입을 추론하며, Quantification, Existential, Lambda 타입에 대한 적용 규칙을 처리합니다.

• 컨텍스트 마커: 컨텍스트 분할을 용이하게 하는 Marker 요소를 도입하여 복잡한 타입 규칙 관리를 돕습니다.

이러한 구현을 통해 infer 함수로 완전한 타입 추론 시스템을 구축합니다.