ML核心语言的意外机制的同式多型类型检验

一、前言ML语言的意外机制颇具特色。它是这样的一种方法,用以得到“动态捕获意外情形”的方便,而又不冒破坏类型规程的危险,并且,仍然容许同式多型惹起意外(exception-raising)表达式。本文讨论ML语言意外机制的同式多型类型检验将各有关的类型推理法则表达成自然推理系统中法则的形式。