Type Systems and Programming Languages 11.9-11.12 takas 2001-05-14

11.9 Sums – sum type 異なる種類のデータを単一に扱う仕組み (variant types) の導入としての binary sum type 例) PhysicalAdrr = {firstlast:String, addr:String}; VirtualAdrr = {name:String, email:String}; というレコード型があったとき Addr = PhisicalAddr + VirtualAddr というものが sum type

11.9 Sums – tag: inl, inr 先の Addr 型の要素は PhysicalAddr, VirtualAddr の要素にタグをつけて生成する 例) pa : PhisicalAddr であるとき inl pa : Addr inl : PhysicalAddr → PhysicalAddr + VirtualAddr inr : VirtualAddr → PhysicalAddr + VirtualAddr

11.9 Sums - case sum type の要素が左右の枝のどちらであるかを判定するために用いる 例) getName : Addr → String getName = λa:Addr. case a of inl x => x.firstlast | inr y => y.name;

11.9 Sums – Uniqueness of Types 問題 T-INL, T-INR で型の唯一性が失われている inl t1 : T1 + T2 において T2 は何でもよいことになる Type checking が単なるボトムアップで済まなくなる 対策 Type checking アルゴリズムを変える (22章) “T2 の取りうるすべてのもの” を単一的に表す (15章) プログラマに T2 を指定してもらう (この章)

11.10 Variants Binary sum を拡張して任意個の型のunionを扱う inl, inr の代わりにラベルを用いて識別する Addr = <physical:PhysicalAddr, virtual:VirtualAddr>; a = <physical=pa> as Addr; # Addr getName = λa:Addr. # Addr → String case a of <physical=x> => x.firstlast | <virtual=y> => y.name;

11.10 Variants - Options 例) OptionalNat = <none:Unit, some:Nat> Table = Nat → OptionalNat; # Nat から Nat への mapping emptyTable = (λn:Nat. <none=unit> as OptionalNat) as Table; # emptyTable : Table extendTable = λt:Table. λm:Nat. λv:Nat. (λn:Nat. if equal n m then <some=v> as OptionalNat; else t n) as Table; # extendTable : Table → Nat → Nat → Table

11.10 Variants - Enumerations 全ラベルが Unit 型になっているもの Weekday = <mon:Unit,tue:Unit,wed:Unit,thu:Unit,fri:Unit>; nextBusinessDay = λw:Weekday. case w of <mon=x> => <tue=unit> as Weekday | <tue=x> => <wed=unit> as Weekday | <wed=x> => <thu=unit> as Weekday | <thu=x> => <fri=unit> as Weekday | <fri=x> => <mon=unit> as Weekday;

11.10 Variants - Single-Field Variants V = <l:T>; T の要素に対する操作を V の要素に直接適用できなくなる 例) Dollar = <dollars:Float>; Euro = <euros:Float>; Float という basic type を区別できるようになる dollars2euros = λd:Dollar. … というように型チェックができるようになる

11.10 Variants – Variants vs Datatype <l1:T1,…,ln:Tn> as T Datatype (OCaml で使われているもの) type T = l1 of T1 | … | ln of Tn;

11.10 Variants – Variants と Datatype の違い (1 of 2) 型とラベル(datatype constructor)の大文字小文字が逆 datatype constructor を使用するとき Type の記述が不要(OCaml) ラベルに対する型を省略可能で Unit になる Type Weekday = Mon | Tue | Wed | Thu | Fri

11.10 Variants – Variants と Datatype の違い (2 of 2) 再帰的表現 type NatList = nil | cons of Nat * NatList Type operator (引数付き datatype) type ’a List = nil | cons of ’a * ’a List

11.11 General Recursion Untyped λ-calculus 同様 fix を用いて再帰を表現する ff = λie:Nat→Bool. # (Nat → Bool) → Nat → Bool λx:Nat. if iszero x then true else if iszero (pred x) then false else if ie (pred (pred x)); iseven = fix ff; # Nat → Bool

11.11 General Recursion fix には関数だけが適用可能なわけではない ff = λieio:{iseven:Nat→Bool, isodd:Nat→Bool} {iseven = λx:Nat. if iszero x then true else ieio.isodd (pred x), isodd = λx:Nat. if iszero x then false else ieio.iseven (pred x)}; # ff : {iseven:Nat→Bool,isodd:Nat→Bool} → {iseven:Nat→Bool,isodd:Nat→Bool} r = fix ff; # r: {iseven:Nat→Bool,isodd:Nat→Bool}

11.12 Lists →, ×と同様の type operator List T (T の要素の有限長のリスト) 空リスト: nil[T] cons: cons[T] t1 t2 (t1:T, t2: List T) テスト: isnil[T] t (t:T)