Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [polymorphism]

The tag has no usage guidance.

3
votes
1answer
93 views

Universe polymorphism: the inference of universes and their constraints

When making a universe polymorphic definition in Coq, universes and their constraints are automatically inferred. Are they somewhat the most general ones (in a sense similar to the principal type ...
0
votes
1answer
103 views

Language/type system closest to Haskell without general recursion

I've implemented a completely functional DSL, and now I'd like to reason about it. It would be helpful to be able to compare it to existing languages. The type system is parametric polymorphic with ...
4
votes
0answers
116 views

Completeness of realizability semantics for higher-order type theory

In this answer I mention a paper by Geuvers in which he describes a class of models for a type theory $\lambda P_2$ which is a sub-system of the CoC and roughly corresponds to 2nd order predicate ...
4
votes
0answers
60 views

Finite intersection property of polymorphic type families

Let $\Phi$ be a type functor definable in polymorphic lambda calculus: $$ \alpha : * \vdash \Phi(\alpha) : * $$ $$ f : A \to B \vdash \mathsf{Map}^{A,B}_\Phi(f) : \Phi(A) \to \Phi(B)$$ Suppose further ...
11
votes
2answers
261 views

Higher-rank polymorphism over unboxed types

I have a language in which types are unboxed by default, with type inference based on Hindley–Milner. I’d like to add higher-rank polymorphism, mainly for working with existential types. I think I ...
5
votes
1answer
196 views

Commutativity of addition in polymorphic lambda calculus

In the article "Extensional models of polymorphism" by Breazu-Tannen and Coquand, natural numbers are presented using a Church-like encoding: $polyint = \forall t . (t \to t) \to t \to t$ Addition ...
5
votes
1answer
165 views

Nested automatization of type inference of forall elimination

Following a previous question about how to automatize the type inference in a forall elimination of an application, now suppose we want to do the same but for a nested forall, say $(\Lambda X_1.\...
9
votes
1answer
425 views

In System F à la Church, can we automatize type inference for the for-all elimination?

The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$. Now, suppose ...
11
votes
2answers
414 views

Does the System F with pairs have the strong normalisation and subject reduction properties?

It is easy to look in a lot of textbooks the proofs of subject reduction and strong normalisation for System F, also, sometimes there are definitions of System F with pairs, where (t,r) is a term, not ...
7
votes
0answers
388 views

Type inference with subtype constraints and polymorphism using Trifonov and Smith's constraint maps

Trifonov and Smith's Subtyping Constrained Types (1996) introduces constraint maps to represent consistent closed constraint sets (such maps providing sets of lower and upper bounds to each variable ...