Subtyping: Overview and Implementation

• subtypingの概要と実装を説明する

3. Subtyping

3.1 Overview

ex. Int と Float 包含関係があるが型は違うのでエラー

• オブジェクト指向はSubtypingをsubclassで表す
• 論文ではレコード型として表現

3.2 Implementation of FunSub

• 型付きλ計算にレコード型と明示型付けを導入した FunSub 言語を考える

> (fn x :: (Int -> Int) => 2)
ok: (Int -> Int)
> (fn x:: (Int -> Int) => true)
fail

(fn x :: ({ a: Int, b: Int } -> { a: Int }) => x)
{ a = 2, b = 2, c = true } :: { a: Int, b: Int, c: Bool }

型

data Ty
	= IntTy
	| BoolTy
	| ArrowTy Ty Ty
	| RcdTy [(String, Ty)]
deriving (Show, Eq)

3. 3 Rules

• Subsumption: 型 $\alpha$ の項 $t$ が存在し, $\alpha$ が $\tau$ のサブタイプなら $t$ は $\tau$ 型

$$\frac{\Gamma ⊢t:\alpha \alpha <:\tau }{\Gamma ⊢t:\tau }$$

• supertypeは複数ある, 多重継承として紹介

Refl: 自身もサブタイプ

$$\frac{}{\iota <:\iota }$$

Trans: 推移

$$\frac{{\tau }_a<:{\tau }_b{\tau }_b<:{\tau }_c}{{\tau }_a<:{\tau }_c}$$

3.4 Records

• Record型のサブタイプを決めるには2通りある

• RecordWidthSub: width-wiseな方法, 余ったフィールドは無視される.

$$\frac{\Gamma ⊢T_i^{i\in i\cdots n+k}}{\left\{a_i:T_i^{i\in i\cdots n+k}\right\}<:\left\{a_i:{T_i}^{i\in i\cdots n}\right\}}$$

ex. { a: Int } <: { a: Int, b: Bool }

• RecordDepthSub: depth-wiseな方法, フィールドは一致していなければ行けない

isSubtype (RcdTy xs) (RcdTy ys) = all sub ys
	where sub (lbl, ty) = case lookup lbl xs of
		Just ty2 -> isSubtype ty2 ty
		Nothing -> False

3.5 Functions

FunctionSub: 関数抽象の型付け, $\alpha$: 引数の型, $\tau$ 返り値の型

$$\frac{{\alpha }^{\prime }<:\alpha \tau <:{\tau }^{\prime }}{\alpha \to \tau <:{\alpha }^{\prime }\to {\tau }^{\prime }}$$

関数の型になると依存関係が逆転する: variance の概念
関数型は 反変.

isSubtype (ArrowTy a b) (ArrowTy x y) =
	isSubtype x a && isSubtype b y

FunctionApp: 関数適用の型付け

$$\frac{\Gamma ⊢f:\tau \to \beta \alpha <:\tau \Gamma ⊢:\alpha }{\Gamma ⊢fv:\beta }$$

typecheck env (FApp fn arg) =
	case typecheck env fn of
		Left err -> Left err
		Right (ArrowTy t1 t2) ->
			case typecheck env arg of
				Left err -> Left err
				Right argType ->
					if isSubtype argType t1
						then Right t2
						else Left $ "arg is not subtype"
		Right t -> Left $ "typemismatch: -> vs {t}"

System F の部分型付け派生として $F_{<:}$ があるらしい.

• 型推論のアルゴリズム Algorithm W は単一の型しか対応していないので部分型に対応していないらしい.

参考文献

• https://jin.crypt.sg/files/subtyping.pdf