7

I think we just need to get some things straight here: In the expression $\lambda a : \mathsf{type} . \lambda x : a . x$ the variable $a$ is bound (by the outer $\lambda$). The expressions $\lambda a : \mathsf{type} . \lambda x : a . x$ and $\lambda b : \mathsf{type} . \lambda x : b . x$ are $\alpha$-equal. The expression $\lambda a : \mathsf{type} . \...


7

The Dunfield & Krishnaswami paper's introduction refers to Practical type inference for arbitrary-rank types As can be seen, it scales well to advanced type systems; moreover, it is easy to implement, and yields relatively high-quality error messages (Peyton Jones et al. 2007) In System F-ish approach there is also a "subtyping" relation. See ...


6

Character and String are conceptually very, very different. Google for "inheritance vs. composition" - you seem to think that Character and String should be connected via inheritance, but in reality a String is composed of 0, 1 or more Characters. And to throw a spanner in the works: Strings are often large, and String operations must be very efficient. ...


6

The missing part is the "identity extension lemma", which is mentioned in Reynolds' original paper but not in Wadler's. For $F : \text{Type} \to \text{Type}$, this says that if the relational interpretation of $F$ is instantiated with a type $A$ and the identity relation on $A$, we get the identity relation on $F\,A$. For System F, identity ...


5

$$\newcommand{\expr}{\mathsf{expr}} \newcommand{\int}{\mathbf{Int}} \newcommand{\List}{\mathbf{List}} \newcommand{\let}{\mathbf{let}} \newcommand{\id}{\mathsf{id}} \newcommand{\in}{\mathbf{in}} \newcommand{\map}{\mathsf{map}} \newcommand{\string}{\mathbf{String}} $$ It's not really possible to answer this without being a little more precise about the status ...


5

An informal, but better way of explaining parametric polymorphism is that the term has a uniform definiton/semantics for all types. A simple example is the identity function: $$λ x. x$$ This is one term that can be reasonably given the type $ℕ → ℕ$, $\mathsf{Bool} → \mathsf{Bool}$, etc. Therefore, we also consider it reasonable for it to give it the type $∀...


5

I imagine what the comment writer is referring to is this... Consider type inference in Haskell. At some point, we may be asked to solve the unification problem f a = Maybe Int. This is very easy to solve (f = Maybe, a = Int), but only because we have restricted the allowable solutions. The solution to f may only be built out of (partial) applications of ...


5

I'm sure that this isn't the only advantage, but I think the primary advantage is simplicity. This is even identified in the original paper introducing the value restriction: previous solutions all existed, but the complexity of annotations made them undesirable. The majority of value that people want to give polymorphic types are functions, which are ...


4

Subtyping is conceptually very different from inheritance. Subtyping refers to shared interfaces; $\tau$ is a subtype of $\tau'$, i.e. $\tau <: \tau'$, then all expressions of type $\tau$ could be used when one of type $\tau'$ is expected. Inheritance refers to the reuse of implementation; if class A inherits class B then A reuses the implementation of B....


4

Strachey's paper defines only two main classes of polymorphism. Subtyping is certainly not parametric polymorphism, so either subtyping is a form of the remaining class or Strachey's terms are not as comprehensive as he thought. Strachey distinguished between parametric polymorphism, where there is no information about the actual type and any type can be ...


4

Keep in mind that, in PL lingo, the term "polymorphism" is used for different notions. In OOP, polymorphism usually means subtype polymorphism. If we have a function foo(x: A) we can call foo with any object having a subtype of A. In this way, the function is defined only once but can operate on "many types" -- which justifies the usage of the word "...


4

They're definitely different things, which is easier to see with a clearer definition of ad-hoc polymorphism. Quoting from Wikipedia: ...ad hoc polymorphism is a kind of polymorphism in which polymorphic functions can be applied to arguments of different types... So in the definition you've quoted, they're using "on" to mean "passed as arguments", rather ...


4

The other answers are good, I just wanted to make it explicit that currying for dependent types is $$ \textstyle \prod (x : A) . \prod (y : B(x)) . C(x, y) \ \cong \ \prod (p : \sum (x : A) . B(x)) . C(\pi_1(p), \pi_2(p)) $$ which is more suggestive in Agda-style notation: $$ (x : A) \to (y : B(x)) \to C(x,y) \ \cong\ (p : (x : A) \times B(x)) \to C(\pi_1(...


4

As a general recipe, to figure out how to encode a type A, write down ∀Z . (A → Z) → Z and massage it to something that does not involve A, using basic isomorphisms, such as currying and uncurrying. For example, if we plug in A := X + Y we get: ∀ Z . (X + Y → Z) → Z ≅ ∀ Z . (X → Z) × (Y → Z) → Z ≅ ∀ Z . (X → Z) → (Y → Z) → Z You can also ...


3

The notation is explained in your course material, e.g. here starting on slide 47. In the notation $$T = \forall \alpha_1, \dots, \alpha_n.\tau$$ $\alpha_i$ are type variables, the $\tau$ is a monomorphic type, and $T$ is a universally quantified, polymorphic type. While free type variables may occur in $\tau$, the quantified variables $\alpha_i$ do not ...


3

You can see an instance of the claimed property in the two definitions of add3. In the ADT style, add3 is defined as: let { Counter, counter } = counterADT in let add3 = λ (c : Counter). counter.inc (counter.inc (counter.inc c)) in counter.get (add3 counter.new); As you see, in order to call about inc, one must already have opened the existential package. ...


3

You seem to have been confounded by many related and similar but crucially different concepts! Let me attempt to explain them one at a time. Parametric polymorphism is the ability to write types that quantify universally over type variables using the $\forall$ quantifier. It is similar to template polymorphism in C++, or generics in Java. For example, the ...


3

So, first, a question. Are you using dynamic or static dispatch? i.e. if Circle and Shape provide implementations of the same method, and you cast a Circle to a Shape, which one gets called? If you're using static dispatch, one way to do it is, instead of making a Circle by taking a shape and adding fields, you make Circle its own type, with a special Super ...


3

To check the application of a function like g : (forall a. a -> a) -> Int to f, we need to check that f : forall a. a -> a. Instead of matching quantifiers (which would be quite brittle), we introduce a fresh, rigid (i.e., non-unifiable) variable, say a1, and we need to check that f : a1 -> a1, and now we can carry on as usual, instantiating f ...


2

I finally figured it out. The key is using sub-typing rules. ctx[]|- t:S ctx[]|S<:T ---------------------------t-sub ctx[]|-t:T By applying this rule after T-APP rules, you can eliminate all "A==B" equations by using eq(A,A) -> . eq(A-->B,A-->B) -> eq(A,A),eq(B,B). ........ One ...


2

Let's say that there's a [$k$-ary] relation $R$ and [$m$-ary] function $f$ such that $m>k$. Is $f$ a polymorphism of $R$? Maybe, maybe not: it depends on the function and the relation. A given $k$-ary relation may have polymorphisms of arity arity less than, equal to, and/or greater than $k$. In fact, every relation has polymorphisms of all arities....


2

A useful intuition is the one you described: the code of a parametric-polymorphic function f can not access type T and choose to behave in different ways according to what T is. Essentially, for f the values of type T are opaque: f can interact with those values only in very restricted ways. For instance, f can "move them around": f : <T,U> (T,U) -&...


2

Contrary to what you wrote, in many languages with parametric polymorphism, the type usually is not provided as an argument to the function. At least, it's not like the other arguments. You can't write something like "if T == int ..." because T is not a variable that can you can access in this way. (How can you ensure this separation between arguments vs ...


2

Short Answer: In λX₁. λX₂. ... λXₙ. t it doesn't matter if t is not a function, but if so, it may not be an interesting example for introduction. Long Answer: First of all, technically speaking, the type system defined in Figure 23-1 does NOT have any base types such as Bool or Nat. A type of t in λX. t is either a type variable X, a function type T → T, ...


2

Structural type systems don't necessarily have anything to do with records. For instance, you could have a system where: data Bool = False | True data Two = Zero | One are actually the same type, because they are both types with two nullary constructors. It also doesn't necessarily tell you much about records, because even though types are determined by ...


2

I think the easiest thing is to refer you to the famous Theorems for free! paper, which explains the intuition behind the use of the Reynolds parametricity theorem. Intuitively, in System $\mathrm F$ a function $\alpha$ of type $\forall X. F\ X \rightarrow G\ X$, is so polymorphic, that $X$ can be instantiated by a morphism $f$ rather than just types. When ...


2

I am not sure I understand your question, but I believe the answer is "yes". When describing monomorphic languages, an expression such as let id x = x : τ (where τ is understood as a type meta-variable) does not mean that you can write τ in the program text. Rather, it means an arbitrary expression of that shape, where the meta-variable is replaced by ...


2

The uncurrying process will lead to existential types. Since the adjoint of $(X\to)$ is $(X\times\vphantom{Y})$ and the adjoint of $(\forall X.)$ is $(\exists X.)$, it is appearently inevitable. Also, it will lead to types depending on terms (where simple types only depends on types themselves, and polymorphism allows terms to depend on types). So generally ...


1

I can only think of some uncurrying of 1 and 3. $\forall X. (X \times int) \rightarrow X$ It looks like we can not uncurry this one, unless we transform it first into the isomorphic type 1. $int \rightarrow \forall X. (X \times int) \rightarrow X$ Alternatively, if we can apply an isomorphism, (3) can be rewritten as $$ \forall X. int \rightarrow (X \times ...


1

I will attempt an answer, though, the discussion in comments with @yuval-filmus seems to be going in the right way. Let's recap: The book discusses ADTs against objects in their strictest sense. ADTs are entirely public about their unique representation. Belonging in the ADT means satisfying said representation, and so binary methods can rightfully assume ...


Only top voted, non community-wiki answers of a minimum length are eligible