[TYPES] System FC: inference rule (EqCo) and grammar for $\kappa$

[Simon Peyton-Jones]

Adam

The FC paper makes an elaborate pun between types and coercions.   This is economical on notation, but it does my head in every time.  Moreover, we treated the type
	(t1~t2) => t3
as syntactic sugar for
	forall (_ : t1~t2). t3
and that in turn leads directly to the confusion that you identify (I believe correctly).

Rather than untangle that paper, have a look at our subsequent effort, "Generative type abstraction and type-level computation", to be presented at POPL later this month:
	http://www.cis.upenn.edu/~sweirich/newtypes.pdf

There you'll see that (a) types and coercions are described separately, and (b) the type (t1~t2) => t3 is shorthand for a three-place type constructor (~e) t1 t2 t3.   Despite some additional complexity from "roles" (introduced in this new paper), the result is a lot easier to grok, I think.  You'll find a brief comparison with the old system in Section 6.2.

best wishes

Simon

|  -----Original Message-----
|  From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-
|  bounces at lists.seas.upenn.edu] On Behalf Of Adam Megacz
|  Sent: 05 January 2011 08:01
|  To: types-list at lists.seas.upenn.edu
|  Subject: [TYPES] System FC: inference rule (EqCo) and grammar for $\kappa$
|  
|  [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
|  
|  
|  Hello, I have a question about System FC, as described in the paper
|  "System F with Type Equality Coercions" (Sulzmann, Chakravarty, Jones,
|  Donnelly).
|  
|  Figure 3 describes the judgment $\vdash_k$, which is a ternary relation
|  between a context, a kind, and a sort.  Specifically, if we see a
|  judgment:
|  
|     $$ X \vdash_k Y : Z $$
|  
|  we know that X is from the syntactic class of contexts (nonterminal
|  \Gamma of Figure 1), Y is from the syntactic class of kinds (nonterminal
|  \kappa of Figure 1), and Z is from the syntactic class of sorts
|  (nonterminal \delta of Figure 1).
|  
|  The first hypothesis of rule (EqCo) is
|  
|     $$ \Gamma \vdash_k \gamma_1 : CO $$
|  
|  so we know that in rule (EqCo) $\gamma_1$ comes from the syntactic class
|  of kinds.  However, the conclusion of rule (EqCo) is:
|  
|     $$ \Gamma \vdash_k \gamma_1 \sim \gamma_2 : CO $$
|  
|  We know that $\gamma_1 \sim \gamma_2$ is a kind, but in the $\kappa$
|  nonterminal in the grammar (Figure 1) the alternative for the $\sim$
|  operator indicates that its arguments -- in particular $\gamma_1$ --
|  must come from the syntactic class of types.  This is in conflict with
|  the previous paragraph.
|  
|  I suspect that the authors intended to have a fourth alternative for
|  nonterminal $\kappa$, meaning that Figure 1 should be amended to:
|  
|    $$ \kappa,\iota
|          \rightarrow
|          \star                           |
|          \kappa_1 \righatrrow \kappa_2   |
|          \sigma_1 \sim        \sigma_2   |
|          \kappa_1 \sim        \kappa_2
|    $$
|  
|  Is my suspicion correct?  If so, I believe the $\sim$ operator is
|  actually triply-overloaded.
|  
|  I have a similar question about $\gamma$ in the conclusion of (CompC).
|  
|  Thanks,
|  
|    - a
|  
|