Navigation Menu

Skip to content

Commit

Permalink
use \sigma instead of raw unicode character in math mode, as it
Browse files Browse the repository at this point in the history 
does not render in the PDF otherwise.
  • Loading branch information
@iainmcgin
iainmcgin committed Feb 19, 2013
1 parent 7691d7f commit 1352994
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion 05-types.md
View file
Expand Up @@ -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:
Expand Down

4 comments on commit 1352994

@datayja
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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!

@Blaisorblade
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(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!

@Blaisorblade
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@datayja
Copy link

@datayja datayja commented on 1352994 Aug 5, 2014

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.