Arantium Maestum

プログラミング、囲碁、読書の話題

型理論

Algorithm W実装のためにPrincipal Type Schemes for Functional Programsを読む(後編)

前回はSubstitution関連で少し寄り道したが、今回こそはPrincipal Type Schemes for Functional Programsの中核である type inference Robinson's unification algorithm algorithm W の話。 type inference For assumptions A, expressions e and type-sche…

Algorithm W実装のためにPrincipal Type Schemes for Functional Programsを読む(中編)

前回「type inference、Robinson's unification, algorithm Wを見ていく」と書いたが、その前にsubstitutionについてつらつらと考えてみたい。 S is a substitution of types for type variables, often written [τ_1/α_1,...,τ_n/α_n] or [τ_i/α_i] とある…

Algorithm W実装のためにPrincipal Type Schemes for Functional Programsを読む(前編)

型推論のためのAlgorithm Wを実装するため、DamasとMilnerのPrincipal Type Schemes for Functional Programsを読んでいる。 重要そうな概念としては expression type/type-scheme substitution instance/generic instance assumption assertion closure typ…

論文メモ: Towards a Theory of Type Structureを読もうとして挫折した話

プログラミング言語理論に関係する論文を結構読み散らかしているのだが、あまりしっかりアウトプットする機会もないので読み込みも甘いし記憶も曖昧になる。 というわけで面白そうなやつは、内容・背景・感想などをブログにメモとして残していこうと考えた。…