Recent searches
Search options
Administered by:
これよさそう。Dunfield 先生による bidirectional typing の全てじゃん
> Bidirectional Typing
https://arxiv.org/abs/1908.05839
arXiv.orgBidirectional TypingBidirectional typing combines two modes of typing: type checking, which
checks that a program satisfies a known type, and type synthesis, which
determines a type from the program. Using checking enables bidirectional typing
to support features for which inference is undecidable; using synthesis enables
bidirectional typing to avoid the large annotation burden of explicitly typed
languages. In addition, bidirectional typing improves error locality. We
highlight the design principles that underlie bidirectional type systems,
survey the development of bidirectional typing from the prehistoric period
before Pierce and Turner's local type inference to the present day, and provide
guidance for future investigations.
Bidirectional type checking の記事書こうかなと思ってたけど、これ読めで全て事足りる気がしたので、もうよくね
足りないところがあるとしたら、typing rule を step-by-step で構築する方法は全て書いてあるが、そこから algorithmic typing に持っていくところが書いてないのかな
まあでもそれは https://arxiv.org/abs/1306.6032 読めで終わるんだよなあ。なので、やっぱ閉廷ですよ
arXiv.orgComplete and Easy Bidirectional Typechecking for Higher-Rank PolymorphismBidirectional typechecking, in which terms either synthesize a type or are
checked against a known type, has become popular for its scalability (unlike
Damas-Milner type inference, bidirectional typing remains decidable even for
very expressive type systems), its error reporting, and its relative ease of
implementation. Following design principles from proof theory, bidirectional
typing can be applied to many type constructs. The principles underlying a
bidirectional approach to polymorphism, however, are less obvious. We give a
declarative, bidirectional account of higher-rank polymorphism, grounded in
proof theory; this calculus enjoys many properties such as eta-reduction and
predictability of annotations. We give an algorithm for implementing the
declarative system; our algorithm is remarkably simple and well-behaved,
despite being both sound and complete.
まあ subsumption 周りの design choice はまとめる価値があるかもな