Embed Notice

部分型付け \overline{T \to U \mathrel{<\vcentcolon} (S \to T) \to S \to U} を型強制 \llbracket\overline{T \to U \mathrel{<\vcentcolon} (S \to T) \to S \to U}\rrbracket = \lambda f : (T \to U) \mathbin. \lambda g : (S \to T) \mathbin. \lambda x : S \mathbin. f(gx) によって翻訳することを考えた