타입이 교차하고 효과가 처리될 때

우리는 대수적 효과 (algebraic effects) 및 핸들러 (handlers)를 갖춘 $\lambda$-calculus를 위한 새로운 교차 타입 시스템 (intersection type system)을 소개합니다. 본질적으로 행동적 (behavioral) 성격을 띠는 이 시스템은 교차 타입 시스템의 고전적 특성, 특히 주축소 (subject reduction) 및 확장 (expansion) 성질을 누립니다. 따라서 이 시스템은 평가 과정이 종료되는 항 (terms)의 집합을 특징짓는 동시에, 도달 가능성 문제 (reachability problem)를 타입 추론 (type inference)으로 환원할 수 있게 합니다. 핸들러를 갖춘 계산법(calculus)에 대해 이러한 특징을 가진 최초의 시스템인 이 새로운 시스템은 단순 타입 (simple types) 시스템을 유도합니다. 이 시스템은 종료를 보장하지는 않지만, Dal Lago와 Ghyselen의 HEPCF와 같은 유사한 타입 시스템들과 달리 타입 건전성 (type sound)을 가지며 결정 가능한 HOMC 문제를 허용합니다.