Permalink
Browse files

use \sigma instead of raw unicode character in math mode, as it

does not render in the PDF otherwise.
  • Loading branch information...
1 parent 7691d7f commit 1352994346ee78a0d4140c65e61822aca12229c2 @iainmcgin iainmcgin committed Feb 19, 2013
Showing with 1 addition and 1 deletion.
  1. +1 −1 05-types.md
View
@@ -172,7 +172,7 @@ parameters $a_1 , \ldots , a_n$.
Say the type parameters have lower bounds $L_1 , \ldots , L_n$ and
upper bounds $U_1 , \ldots , U_n$. The parameterized type is
well-formed if each actual type parameter
-_conforms to its bounds_, i.e. $σ L_i <: T_i <: σ U_i$ where $σ$ is the
+_conforms to its bounds_, i.e. $\sigma L_i <: T_i <: \sigma U_i$ where $\sigma$ is the
substitution $[ a_1 := T_1 , \ldots , a_n := T_n ]$.
(@param-types) Given the partial type definitions:

4 comments on commit 1352994

I may not be very strong at math stuff, so probably no surprise that I stumbled upon these lines for a couple of day already, still not able to properly understand. Let’s say that we have a type T, which happens to be parameterized by types T_1 up to T_n, and T is a type constructor taking exactly n type parameters a_1 up to a_n. Then, a lower bound L_i would be the type, for which the actual used type parameter must be the same type or its supertype, and an upper bound U_i would be the type, for which the actual used type parameter must be the same type or its subtype. Now let’s say that for every i from 1 to n, the following must be true for the parameterized type to be well-formed: L_i <: T_i <: U_i. Also since a_i is kind of a variable, the same would apply for L_i <: a_i <: U_i, after filling a_i with the used type, like a substitution. So, the question now: shouldn’t the σ be in the middle? Or is this about something different, my only guess being that the type constructor would not really be correct if the lower bound was a supertype of the upper bound? Thanks for help!

Contributor

Blaisorblade replied Aug 5, 2014

(Some mailing list might be a better place for this).

I may not be very strong at math stuff, so probably no surprise that I stumbled upon these lines for a couple of day already, still not able to properly understand. Let’s say that we have a type T, which happens to be parameterized by types T_1 up to T_n, and T is a type constructor taking exactly n type parameters a_1 up to a_n. Then, a lower bound L_i would be the type, for which the actual used type parameter must be the same type or its supertype, and an upper bound U_i would be the type, for which the actual used type parameter must be the same type or its subtype. Now let’s say that for every i from 1 to n, the following must be true for the parameterized type to be well-formed: L_i <: T_i <: U_i.

All of that is correct :-)

Also since a_i is kind of a variable, the same would apply for L_i <: a_i <: U_i, after filling a_i with the used type, like a substitution. So, the question now: shouldn’t the σ be in the middle?

No... but this paragraph is not talking about defining, say, List[T], but about using it, say List[Int]. In this case, T_1 = Int, because the T_i are the actual arguments, not the formal parameters. So in T_i the substitution was already done, if you want. However, you still need it for the bounds.

To see bounds, we need to look at something bigger, say TreeMap[I, String], assuming the definition:

class TreeSet[A <: Comparable[A], B] { … }
class I extends Comparable[I] { … }

In TreeMap[I, String], we have T_1 = I, and T_2 = String, but U_1 = Comparable[A], which still contains A! So we need the substitution σ to replace that A by T_1, that is I.

Hope this helps!

Contributor

Blaisorblade replied Aug 5, 2014

Arguably, the spec text could maybe be clarified a bit. It's not bad, it's just more spec-y than tutorial-y.

Oh, now I get it! Thanks, it makes sense now.
And yes, it could be more clarified throughout more places than just this one, the math-y style is not always obvious.

Please sign in to comment.