GADT，功能性，参数性：选择两个
GADTs, Functoriality, Parametricity: Pick Two
摘要：
GADT可以表示为他们的教会编码la Atkey，或作为固定点la Johann和Polonsky。虽然表示为Church编码的GADT不需要支持满足函子定律的映射函数，但GADT的不动点表示必须支持这样的映射函数，即使是定义良好的。因此，GADT的两种表示通常不需要相同。这一观察结果迫使人们选择支持GADT的语言中的数据类型表示方式。在本文中，我们表明，选择是否表示数据类型作为他们的教会编码或定点确定是否支持GADT语言可以有参数模型。因此，这种选择对于我们如何使用这些高级数据类型进行编程和推理具有重要的影响。
英文摘要：
GADTs can be represented either as their Church encodings a la Atkey, or as fixpoints a la Johann and Polonsky. While a GADT represented as its Church encoding need not support a map function satisfying the functor laws, the fixpoint representation of a GADT must support such a map function even to be well-defined. The two representations of a GADT thus need not be the same in general. This observation forces a choice of representation of data types in languages supporting GADTs. In this paper we show that choosing whether to represent data types as their Church encodings or as fixpoints determines whether or not a language supporting GADTs can have parametric models. This choice thus has important consequences for how we can program with, and reason about, these advanced data types.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
