358 have the variable convention already built in. |
358 have the variable convention already built in. |
359 |
359 |
360 \begin{figure} |
360 \begin{figure} |
361 \begin{boxedminipage}{\linewidth} |
361 \begin{boxedminipage}{\linewidth} |
362 \begin{center} |
362 \begin{center} |
363 \begin{tabular}{r@ {\hspace{2mm}}cl} |
363 \begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l} |
364 \multicolumn{3}{@ {}l}{Type Kinds}\\ |
364 \multicolumn{3}{@ {}l}{Type Kinds}\\ |
365 @{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\medskip\\ |
365 @{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\ |
366 \multicolumn{3}{@ {}l}{Coercion Kinds}\\ |
366 \multicolumn{3}{@ {}l}{Coercion Kinds}\\ |
367 @{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\medskip\\ |
367 @{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\ |
368 \multicolumn{3}{@ {}l}{Types}\\ |
368 \multicolumn{3}{@ {}l}{Types}\\ |
369 @{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"} |
369 @{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"} |
370 @{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\medskip\\ |
370 @{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\ |
371 \multicolumn{3}{@ {}l}{Coercion Types}\\ |
371 \multicolumn{3}{@ {}l}{Coercion Types}\\ |
372 @{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"} |
372 @{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"} |
373 @{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> |"}\\ |
373 @{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> "}\\ |
374 & & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> |"}\\ |
374 & @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\ |
375 & & @{text "left \<gamma> | right \<gamma> | \<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 |"}\\ |
375 & @{text "|"} & @{text "\<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\ |
376 & & @{text "rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\medskip\\ |
|
377 \multicolumn{3}{@ {}l}{Terms}\\ |
376 \multicolumn{3}{@ {}l}{Terms}\\ |
378 @{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma> |"}\\ |
377 @{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma>"}\\ |
379 & & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2 |"}\\ |
378 & @{text "|"} & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\ |
380 & & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\medskip\\ |
379 & @{text "|"} & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\ |
381 \multicolumn{3}{@ {}l}{Patterns}\\ |
380 \multicolumn{3}{@ {}l}{Patterns}\\ |
382 @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\medskip\\ |
381 @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\smallskip\\ |
383 \multicolumn{3}{@ {}l}{Constants}\\ |
382 \multicolumn{3}{@ {}l}{Constants}\\ |
384 @{text C} & & coercion constants\\ |
383 & @{text C} & coercion constants\\ |
385 @{text T} & & value type constructors\\ |
384 & @{text T} & value type constructors\\ |
386 @{text "S\<^isub>n"} & & n-ary type functions\\ |
385 & @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\ |
387 @{text K} & & data constructors\medskip\\ |
386 & @{text K} & data constructors\smallskip\\ |
388 \multicolumn{3}{@ {}l}{Variables}\\ |
387 \multicolumn{3}{@ {}l}{Variables}\\ |
389 @{text a} & & type variables\\ |
388 & @{text a} & type variables\\ |
390 @{text c} & & coercion variables\\ |
389 & @{text c} & coercion variables\\ |
391 @{text x} & & term variables\\ |
390 & @{text x} & term variables\\ |
392 \end{tabular} |
391 \end{tabular} |
393 \end{center} |
392 \end{center} |
394 \end{boxedminipage} |
393 \end{boxedminipage} |
395 \caption{The term-language of System @{text "F\<^isub>C"}, also often referred to as \emph{Core-Haskell} |
394 \caption{The term-language of System @{text "F\<^isub>C"} |
396 \cite{CoreHaskell}. In this version of Core-Haskell we made a modification by |
395 \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this |
397 separating completely the grammars for type kinds and coercion types.\label{corehas}} |
396 version of the term-language we made a modification by separating the |
|
397 grammars for type and coercion kinds, as well as types and coercion |
|
398 types. For this paper the interesting term-constructor is @{text "\<CASE>"} |
|
399 involving the binding of multiple type-, coercion- and term-variables from |
|
400 patterns.\label{corehas}} |
398 \end{figure} |
401 \end{figure} |
399 *} |
402 *} |
400 |
403 |
401 section {* A Short Review of the Nominal Logic Work *} |
404 section {* A Short Review of the Nominal Logic Work *} |
402 |
405 |