<p>You asked why</p>

<blockquote>
  <p><code>[[forall a. [forall b. a -&gt; b]]]</code> has a weight of 1</p>
</blockquote>

<p>It doesn't. It has a <em>polymorphic</em> weight of 1. The polymorphic weight strips the binder before it looks at the weight. For the $\rho$ you chose:</p>

<p>$[\![\forall \overline{\alpha} . \rho]\!] = wt(\rho) = 1 \neq 2 = wt(\forall \overline{\alpha} . \rho)$</p>

CC BY-SA 3.0
2015-05-09T01:57:29.730Z
2015-05-09T01:57:29.730Z
jbapple
<p>I am reading through through a paper called <a href="http://research.microsoft.com/pubs/132621/hmf.pdf" rel="nofollow noreferrer">HMF: Simple Type Inference for First-Class Polymorphism</a> by Daan Leijen of Microsoft Research.</p>

<p>In the paper it describes how to calculate the polymorphic weight of an expression:</p>

<p><img src="https://i.sstatic.net/GnTbm.png" alt="extract from pdf"></p>

<p>I am having trouble understanding why the above example <code>[[forall a. [forall b. a -&gt; b]]]</code> has a weight of 1 rather than two. there are two type abstractions where both type variable are not free in their bodies, should these not be added together?</p>

<type-theory><lambda-calculus><type-inference>
Why is the polymorphic weight 1
t123
# Why is the polymorphic weight 1

(Asked by: username_0 on 2015-05-08)

I am reading through through a paper called [HMF: Simple Type Inference for First-Class Polymorphism](http://research.microsoft.com/pubs/132621/hmf.pdf) by Daan Leijen of Microsoft Research.

In the paper it describes how to calculate the polymorphic weight of an expression:

![extract from pdf](https://i.sstatic.net/GnTbm.png)

I am having trouble understanding why the above example `[[forall a. [forall b. a -> b]]]` has a weight of 1 rather than two. there are two type abstractions where both type variable are not free in their bodies, should these not be added together?

**Tags:** type-theory, lambda-calculus, type-inference


---

## 1 answers

### Answer by username_1 on 2015-05-09. Score: 2 | Accepted answer

You asked why

> `[[forall a. [forall b. a -> b]]]` has a weight of 1

It doesn't. It has a *polymorphic* weight of 1. The polymorphic weight strips the binder before it looks at the weight. For the $\rho$ you chose:

$[\![\forall \overline{\alpha} . \rho]\!] = wt(\rho) = 1 \neq 2 = wt(\forall \overline{\alpha} . \rho)$


---

