User:Mrhaandi/sandbox

This is the user sandbox of Mrhaandi. A user sandbox is a subpage of the user's user page. It serves as a testing spot and page development space for the user and is not an encyclopedia article. Create or edit your own sandbox here.

Other sandboxes: Main sandbox | Template sandbox

Finished writing a draft article? Are you ready to request review of it by an experienced editor for possible inclusion in Wikipedia? Submit your draft for review!

The following table gives an overview over type theoretic concepts that are used in specialized type systems. The names $M,N,O$ range over terms and the names $\sigma ,\tau$ range over types. The notation $\tau [\alpha :=\sigma ]$ (resp. $\tau [x:=N]$ ) describes the type which results from replacing all occurrences of the type variable $\alpha$ (resp. term variable $x$ ) in $\tau$ by the type $\sigma$ (resp. term $N$ ).

Type notion	Notation	Meaning
Product	$\sigma \times \tau$	If $M$ has type $\sigma \times \tau$ , then $M=(N,O)$ is a pair such that $N$ has type $\sigma$ and $O$ has type $\tau$ .
Sum	$\sigma +\tau$	If $M$ has type $\sigma +\tau$ , then either $M=\iota _{1}(N)$ is the first injection such that $N$ has type $\sigma$ , or $M=\iota _{2}(N)$ is the second injection such that $N$ has type $\tau$ .
Function	$\sigma \to \tau$	If $M$ has type $\sigma \to \tau$ and $N$ has type $\sigma$ , then the application $M(N)$ has type $\tau$ .
Intersection	$\sigma \cap \tau$	If $M$ has type $\sigma \cap \tau$ , then $M$ has type $\sigma$ and $M$ has type $\tau$ .
Union	$\sigma \cup \tau$	If $M$ has type $\sigma \cup \tau$ , then $M$ has type $\sigma$ or $M$ has type $\tau$ .
Record	$\langle x:\tau \rangle$	If $M$ has type $\langle x:\tau \rangle$ , then $M$ has a member $x$ that has type $\tau$ .
Parametric	$\forall \alpha .\tau$	If $M$ has type $\forall \alpha .\tau$ , then $M$ has type $\tau [\alpha :=\sigma ]$ for any type $\sigma$ .
Existential	$\exists \alpha .\tau$	If $M$ has type $\exists \alpha .\tau$ , then $M$ has type $\tau [\alpha :=\sigma ]$ for some type $\sigma$ .
Dependent product	$(x:\sigma )\times \tau$	If $M$ has type $(x:\sigma )\times \tau$ , then $M=(N,O)$ is a pair such that $N$ has type $\sigma$ and $O$ has type $\tau [x:=N]$ .
Dependent function	$(x:\sigma )\to \tau$	If $M$ has type $(x:\sigma )\to \tau$ and $N$ has type $\sigma$ , then the application $M(N)$ has type $\tau [x:=N]$ .
Dependent intersection^[1]	$(x:\sigma )\cap \tau$	If $M$ has type $(x:\sigma )\cap \tau$ , then $M$ has type $\sigma$ and $M$ has type $\tau [x:=M]$ .

^ Kopylov, Alexei (2003). "Dependent intersection: A new way of defining records in type theory". 18th IEEE Symposium on Logic in Computer Science. LICS 2003. IEEE Computer Society. pp. 86–95. CiteSeerX 10.1.1.89.4223. doi:10.1109/LICS.2003.1210048.

[1] Kopylov, Alexei (2003). "Dependent intersection: A new way of defining records in type theory". 18th IEEE Symposium on Logic in Computer Science. LICS 2003. IEEE Computer Society. pp. 86–95. CiteSeerX 10.1.1.89.4223. doi:10.1109/LICS.2003.1210048.

[1]