Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorMike Shulman
   • CommentTimeSep 6th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexCreated [[polymorphism]].

   Created polymorphism.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeFeb 16th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexadded this reference: > * [[Robert Atkey]], [[Neil Ghani]] and Patricia Johann, _A Relationally Parametric Model of Dependent Type Theory_, In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014). 2014. ([web](http://bentnib.org/dtt-parametricity.html))

   added this reference:

   • Robert Atkey, Neil Ghani and Patricia Johann, A Relationally Parametric Model of Dependent Type Theory, In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014). 2014. (web)

3. • CommentRowNumber3.
   • CommentAuthorNoam_Zeilberger
   • CommentTimeSep 25th 2018
   • PermaLink
   Author: Noam_Zeilberger
   Format: MarkdownItexadded the Milner 1978 reference <a href="https://ncatlab.org/nlab/revision/diff/polymorphism/10">diff</a>, <a href="https://ncatlab.org/nlab/revision/polymorphism/10">v10</a>, <a href="https://ncatlab.org/nlab/show/polymorphism">current</a>

   added the Milner 1978 reference

   diff, v10, current

4. • CommentRowNumber4.
   • CommentAuthorDavidRoberts
   • CommentTimeDec 17th 2018
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexAdded disambiguation link to [[poly-morphism]]. <a href="https://ncatlab.org/nlab/revision/diff/polymorphism/11">diff</a>, <a href="https://ncatlab.org/nlab/revision/polymorphism/11">v11</a>, <a href="https://ncatlab.org/nlab/show/polymorphism">current</a>

   Added disambiguation link to poly-morphism.

   diff, v11, current

5. • CommentRowNumber5.
   • CommentAuthorCorbin
   • CommentTimeOct 2nd 2021
   • PermaLink
   Author: Corbin
   Format: MarkdownItexAdd a basic paragraph about the classic "Theorems for free!" paper. I am redlinking [[free theorem]] in anticipation of a more categorical approach which could consider these as examples of [[free object]]s. [[System F]] is redlinked elsewhere. Yet another article I should probably stub. <a href="https://ncatlab.org/nlab/revision/diff/polymorphism/14">diff</a>, <a href="https://ncatlab.org/nlab/revision/polymorphism/14">v14</a>, <a href="https://ncatlab.org/nlab/show/polymorphism">current</a>

   Add a basic paragraph about the classic “Theorems for free!” paper.

   I am redlinking free theorem in anticipation of a more categorical approach which could consider these as examples of free objects.

   System F is redlinked elsewhere. Yet another article I should probably stub.

   diff, v14, current

6. • CommentRowNumber6.
   • CommentAuthorCorbin
   • CommentTimeOct 2nd 2021
   • PermaLink
   Author: Corbin
   Format: MarkdownItexFix LaTeX and add a link to the citation. <a href="https://ncatlab.org/nlab/revision/diff/polymorphism/14">diff</a>, <a href="https://ncatlab.org/nlab/revision/polymorphism/14">v14</a>, <a href="https://ncatlab.org/nlab/show/polymorphism">current</a>

   Fix LaTeX and add a link to the citation.

   diff, v14, current

7. • CommentRowNumber7.
   • CommentAuthornLab edit announcer
   • CommentTimeApr 30th 2024
   • PermaLink
   Author: nLab edit announcer
   Format: MarkdownItexAlso adding the [Narya](https://github.com/mikeshulman/narya) proof assistant to this article, to which [[parametricity]] redirects to. Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/polymorphism/16">diff</a>, <a href="https://ncatlab.org/nlab/revision/polymorphism/16">v16</a>, <a href="https://ncatlab.org/nlab/show/polymorphism">current</a>

   Also adding the Narya proof assistant to this article, to which parametricity redirects to.

   Anonymouse

   diff, v16, current

8. • CommentRowNumber8.
   • CommentAuthornLab edit announcer
   • CommentTime7 days ago
   • PermaLink
   Author: nLab edit announcer
   Format: MarkdownItexParametric polymorphism is also called parametricity in more recent type theory literature, such as in * [[Thorsten Altenkirch]], [[Yorgo Chamoun]], [[Ambrus Kaposi]], [[Michael Shulman]], *Internal parametricity, without an interval*, Proceedings of the ACM on Programming Languages (POPL) **8** (2024) 2340-2369 &lbrack;[arXiv:2307.06448](https://arxiv.org/abs/2307.06448), [doi:10.1145/3632920](https://doi.org/10.1145/3632920)&rbrack; Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/polymorphism/17">diff</a>, <a href="https://ncatlab.org/nlab/revision/polymorphism/17">v17</a>, <a href="https://ncatlab.org/nlab/show/polymorphism">current</a>

   Parametric polymorphism is also called parametricity in more recent type theory literature, such as in

   • Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman, Internal parametricity, without an interval, Proceedings of the ACM on Programming Languages (POPL) 8 (2024) 2340-2369 [arXiv:2307.06448, doi:10.1145/3632920]

   Anonymouse

   diff, v17, current

9. • CommentRowNumber9.
   • CommentAuthornLab edit announcer
   • CommentTime7 days ago
   • PermaLink
   Author: nLab edit announcer
   Format: MarkdownItexAdding reference * [[Jean-Philippe Bernardy]], [[Patrik Jansson]], and [[Ross Paterson]]. 2010. *Parametricity and dependent types.* In Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, Paul Hudak and Stephanie Weirich (Eds.). ACM, 345–356. &lbrack;[doi:10.1145/1863543.1863592](https://doi.org/10.1145/1863543.1863592)&rbrack; Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/polymorphism/17">diff</a>, <a href="https://ncatlab.org/nlab/revision/polymorphism/17">v17</a>, <a href="https://ncatlab.org/nlab/show/polymorphism">current</a>

   Adding reference

   • Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. 2010. Parametricity and dependent types. In Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, Paul Hudak and Stephanie Weirich (Eds.). ACM, 345–356. [doi:10.1145/1863543.1863592]

   Anonymouse

   diff, v17, current

10. • CommentRowNumber10.
    • CommentAuthornLab edit announcer
    • CommentTime7 days ago
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdding reference * [[Astra Kolomatskaia]], [[Michael Shulman]], *Displayed Type Theory and Semi-Simplicial Types* &lbrack;[arXiv:2311.18781](https://arxiv.org/abs/2311.18781)&rbrack; Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/polymorphism/17">diff</a>, <a href="https://ncatlab.org/nlab/revision/polymorphism/17">v17</a>, <a href="https://ncatlab.org/nlab/show/polymorphism">current</a>

    Adding reference

    • Astra Kolomatskaia, Michael Shulman, Displayed Type Theory and Semi-Simplicial Types [arXiv:2311.18781]

    Anonymouse

    diff, v17, current

11. • CommentRowNumber11.
    • CommentAuthornLab edit announcer
    • CommentTime7 days ago
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdding redirects for [[external parametricity]], [[internal parametricity]], [[modal parametricity]], and [[modal internal parametricity]]. Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/polymorphism/17">diff</a>, <a href="https://ncatlab.org/nlab/revision/polymorphism/17">v17</a>, <a href="https://ncatlab.org/nlab/show/polymorphism">current</a>

    Adding redirects for external parametricity, internal parametricity, modal parametricity, and modal internal parametricity.

    Anonymouse

    diff, v17, current

12. • CommentRowNumber12.
    • CommentAuthornLab edit announcer
    • CommentTime7 days ago
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdding thesis * Guilhem Moulin. **Internalizing parametricity.** PhD thesis, Chalmers University, 2016. &lbrack;[pdf](https://publications.lib.chalmers.se/records/fulltext/235758/235758.pdf)&rbrack; Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/polymorphism/17">diff</a>, <a href="https://ncatlab.org/nlab/revision/polymorphism/17">v17</a>, <a href="https://ncatlab.org/nlab/show/polymorphism">current</a>

    Adding thesis

    • Guilhem Moulin. Internalizing parametricity. PhD thesis, Chalmers University, 2016. [pdf]

    Anonymouse

    diff, v17, current

13. • CommentRowNumber13.
    • CommentAuthornLab edit announcer
    • CommentTime7 days ago
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdding reference * [[Jean-Philippe Bernardy]], [[Thierry Coquand]], and [[Guilhem Moulin]]. 2015. **A Presheaf Model of Parametric Type Theory.** In The 31st Conference on the Mathematical Foundations of Programming Semantics, MFPS 2015, Nijmegen, The Netherlands, June 22-25, 2015 (Electronic Notes in Theoretical Computer Science, Vol. 319), Dan R. Ghica (Ed.). Elsevier, 67–82. &lbrack;[doi:10.1016/j.entcs.2015.12.006](https://doi.org/10.1016/j.entcs.2015.12.006)&rbrack; Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/polymorphism/17">diff</a>, <a href="https://ncatlab.org/nlab/revision/polymorphism/17">v17</a>, <a href="https://ncatlab.org/nlab/show/polymorphism">current</a>

    Adding reference

    • Jean-Philippe Bernardy, Thierry Coquand, and Guilhem Moulin. 2015. A Presheaf Model of Parametric Type Theory. In The 31st Conference on the Mathematical Foundations of Programming Semantics, MFPS 2015, Nijmegen, The Netherlands, June 22-25, 2015 (Electronic Notes in Theoretical Computer Science, Vol. 319), Dan R. Ghica (Ed.). Elsevier, 67–82. [doi:10.1016/j.entcs.2015.12.006]

    Anonymouse

    diff, v17, current

14. • CommentRowNumber14.
    • CommentAuthornLab edit announcer
    • CommentTime7 days ago
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdding reference * {#BM12} [[Jean-Philippe Bernardy]] and [[Guilhem Moulin]]. 2012. *A Computational Interpretation of Parametricity.( In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. IEEE Computer Society, 135–144. &lbrack;[doi:10.1109/LICS.2012.25](https://doi.org/10.1109/LICS.2012.25)&rbrack; Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/polymorphism/17">diff</a>, <a href="https://ncatlab.org/nlab/revision/polymorphism/17">v17</a>, <a href="https://ncatlab.org/nlab/show/polymorphism">current</a>

    Adding reference

    • {#BM12} Jean-Philippe Bernardy and Guilhem Moulin. 2012. *A Computational Interpretation of Parametricity.( In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. IEEE Computer Society, 135–144. [doi:10.1109/LICS.2012.25]

    Anonymouse

    diff, v17, current