Identity Inclusion in Relational Type Theory


Manage episode 282601615 series 2823367
Player FM과 저희 커뮤니티의 Aaron Stump 콘텐츠는 모두 원 저작자에게 속하며 Player FM이 아닌 작가가 저작권을 갖습니다. 오디오는 해당 서버에서 직접 스트리밍 됩니다. 구독 버튼을 눌러 Player FM에서 업데이트 현황을 확인하세요. 혹은 다른 팟캐스트 앱에서 URL을 불러오세요.

Where relational semantics for parametric polymorphism often includes a lemma called Identity Extension (discussed in Episode 10, on the paper "Types, Abstraction, and Parametric Polymorphism"), RelTT instead has a refinement of this called Identity Inclusion. Instead of saying that the interpretation of every closed type is the identity relation (Identity Extension), the Identity Inclusion lemma identifies certain types whose relational meaning is included in the identity relation, and certain types which include the identity relation. So there are two subset relations, going in opposite directions. The two classes of types are first, the ones where all quantifiers occur only positively, and second, where they occur only negatively. Using Identity Inclusion, we can derive transitivity for forall-positive types, which is needed to derive induction following the natural generalization of the scheme in Wadler's paper (last episode).

94 에피소드