StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>It's not exactly a bug, but it is a long story...</p> <h2>The Story</h2> <p>In 7.0 there used to be a coercion constructor called <code>right</code> which worked like this:</p> <pre><code>g : f a ~ f b --------------- right g : a ~ b </code></pre> <p>That is, if <code>g</code> is a coercion between <code>f a</code> and <code>f b</code>, then <code>right g</code> is a coercion between <code>a</code> and <code>b</code>. This is only sound if <code>f</code> is guaranteed to be injective: otherwise we might legitimately have, say, <code>f Int ~ f Char</code> and then we would be able to conclude <code>Int ~ Char</code>, which would be Bad.</p> <p>But of course, type synonyms and type families are not necessarily injective; for example:</p> <pre><code>type T a = Int type family F a :: * type instance F Int = Bool type instance F Char = Bool </code></pre> <p>So how is this guarantee possible? Well, this is precisely the reason why partial applications of type synonyms and type families are not allowed. Partial applications of type synonyms and type families may not be injective, but saturated applications (even ones which result in a higher kind) always are.</p> <p>Of course, the restriction on partial applications is annoying. So in 7.2, in an attempt to move in the direction of allowing partial application (and because it simplifies the theory and implementation of the coercion language), the <code>right</code> constructor was replaced by a constructor <code>nth</code>, with the accompanying rule</p> <pre><code>g : T a1 .. an ~ T b1 .. bn --------------------------- nth i g : ai ~ bi </code></pre> <p>That is, <code>nth</code> only applies to a coercion <code>g</code> which is between two types which are <em>known to be saturated applications of a type constructor <code>T</code></em>. In theory, this allows for partial applications of type synonyms and families, because we cannot decompose equalities until we know that they are between applications of a (necessarily injective) type constructor. In particular, <code>nth</code> does not apply to a coercion <code>f a ~ f b</code> because <code>f</code> is a type variable, not a type constructor.</p> <p>It was thought at the time of the change that no one would really notice, but obviously this was wrong!</p> <p>Interestingly, the Olegian trick outlined in the <a href="http://permalink.gmane.org/gmane.comp.lang.haskell.cafe/93269">haskell-cafe message from Daniel Schüssler</a> shows that the implementation of type families was not changed accordingly! The problem is that a definition like</p> <pre><code>type family Arg fa type instance Arg (f a) = a </code></pre> <p>should not be allowed if <code>f</code> could be non-injective; in that case the definition does not even make sense.</p> <h2>Next Steps</h2> <p>I think the right thing to do is to reinstate <code>right</code> (or something equivalent), since people clearly want it! Hopefully this will be done soon.</p> <p>In the meantime, it would still be really cool to allow partially applied type synonyms and families. It seems the Right Way (tm) to do that would be to track injectivity in the kind system: that is, each arrow kind would be annotated with its injectivity. This way when encountering an equality <code>f a ~ f b</code> we could look at the kind of <code>f</code> to determine whether it is safe to decompose it into the equality <code>a ~ b</code>. Not coincidentally, I am currently trying to work out the design of such a system. =)</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload