Relational parametricity was first introduced by Reynolds for System F. Although System F provides a strong model for the type systems at the core of modern functional programming languages, it lacks features of daily programming practice such as complex data types. In order to reason parametrically about such objects, Reynolds' seminal ideas need to be generalized to extensions of System F. Here, we explore such a generalization for the extension of System F by Generalized Algebraic Data Types (GADTs) as found in Haskell. Although GADTs generalize Algebraic Data Types (ADTs) -- i.e., simple recursive types such as lists, trees, etc. -- we show that naively extending the parametric treatment of these recursive types is not enough to tackle GADTs. We propose a tentative workaround for this issue, borrowing ideas from the categorical semantics of GADTs known as (functorial) completion. We discuss some applications, as well as some limitations, of this solution.

翻译：关系参数性最初由Reynolds为系统F引入。尽管系统F为现代函数式编程语言核心的类型系统提供了强大模型，但其缺乏日常编程实践中的复杂数据类型等特性。为了对此类对象进行参数化推理，需要将Reynolds的开创性思想推广至系统F的扩展形式。本文针对Haskell中采用的广义代数数据类型（GADTs）扩展系统F，探索了此类推广方案。虽然GADTs泛化了代数数据类型（ADTs）——即列表、树等简单递归类型——但我们证明简单扩展这些递归类型的参数化处理方法不足以应对GADTs。通过借鉴GADTs范畴语义中被称为（函子）完备化的理论，我们针对该问题提出了初步解决方案，并讨论了该方案的应用场景与局限性。