The troublesome reflection rule (TYPES 2015 slides) http://math.andrej.com/2015/05/19/the-troublesome-reflection-rule-types-2015-slides/ を読んでる。 以前に言及 https://plus.google.com/+MasahiroSakai/posts/5JvfPGJj8BU した Brazilian type checking の話の続きか。 流石に Brazil という名前はやめて Andromeda という名前にしたのね。