Skip to main content
MathOverflow

Return to Answer

remove a stray )
Source Link
Jacques Carette
Jacques Carette
  • 11.8k
  • 4
  • 44
  • 80

This answer is largely a rendition of Sridhar's comment into lambda calculus. A strong monad $T$ has the following introduction and elimination rules in the lambda calculus.

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : T(A)} $$ $$ \frac{\Gamma \vdash e : T(A) \qquad \Gamma, x : A \vdash e' : T(B)} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : T(B)} $$

You may recognize these rules as typing a variant of the do-notation in Haskell.

Strength is needed to interpret the elimination rule, since the context $\Gamma$ is available in both premises of the elimination rule. Taking $\sigma : \Gamma \times T(A) \to T(\Gamma \times A)$, we can calculate:

$$ \begin{array}{lcl} e & : & \Gamma \to T(A) \\\ e' & : & \Gamma \times A \to T(B) \\\ T(e') & : & T(\Gamma \times A) \to T^2(B) \\\ T(e'); \mu & : & T(\Gamma \times A) \to T(B) \\\ \langle id; e\rangle & : & \Gamma \to \Gamma \times T(A)\\\ \langle id; e\rangle; \sigma & : & \Gamma \to T(\Gamma \times A)\\\ \langle id; e\rangle; \sigma; T(e'); \mu & : & \Gamma \to T(B)\\\ \end{array} $$

Without the strength $\sigma$, we could not use the context $\Gamma$ in $e'$. That is, we would get introduction and elimination forms:

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : \Diamond A)} $$$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : \Diamond A} $$ $$ \frac{\Gamma \vdash e : \Diamond A \qquad x : A \vdash e' : \Diamond B} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : \Diamond B} $$

I changed the notation from $T$ to $\Diamond$, since this is actually the possibility modality of S4 modal logic! These modalities arise in applications like functional languages for distributed programming --- e.g., see Murphy et al's 2004 LICS paper "A Symmetric Modal Lambda Calculus for Distributed Computing".

This answer is largely a rendition of Sridhar's comment into lambda calculus. A strong monad $T$ has the following introduction and elimination rules in the lambda calculus.

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : T(A)} $$ $$ \frac{\Gamma \vdash e : T(A) \qquad \Gamma, x : A \vdash e' : T(B)} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : T(B)} $$

You may recognize these rules as typing a variant of the do-notation in Haskell.

Strength is needed to interpret the elimination rule, since the context $\Gamma$ is available in both premises of the elimination rule. Taking $\sigma : \Gamma \times T(A) \to T(\Gamma \times A)$, we can calculate:

$$ \begin{array}{lcl} e & : & \Gamma \to T(A) \\\ e' & : & \Gamma \times A \to T(B) \\\ T(e') & : & T(\Gamma \times A) \to T^2(B) \\\ T(e'); \mu & : & T(\Gamma \times A) \to T(B) \\\ \langle id; e\rangle & : & \Gamma \to \Gamma \times T(A)\\\ \langle id; e\rangle; \sigma & : & \Gamma \to T(\Gamma \times A)\\\ \langle id; e\rangle; \sigma; T(e'); \mu & : & \Gamma \to T(B)\\\ \end{array} $$

Without the strength $\sigma$, we could not use the context $\Gamma$ in $e'$. That is, we would get introduction and elimination forms:

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : \Diamond A)} $$ $$ \frac{\Gamma \vdash e : \Diamond A \qquad x : A \vdash e' : \Diamond B} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : \Diamond B} $$

I changed the notation from $T$ to $\Diamond$, since this is actually the possibility modality of S4 modal logic! These modalities arise in applications like functional languages for distributed programming --- e.g., see Murphy et al's 2004 LICS paper "A Symmetric Modal Lambda Calculus for Distributed Computing".

This answer is largely a rendition of Sridhar's comment into lambda calculus. A strong monad $T$ has the following introduction and elimination rules in the lambda calculus.

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : T(A)} $$ $$ \frac{\Gamma \vdash e : T(A) \qquad \Gamma, x : A \vdash e' : T(B)} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : T(B)} $$

You may recognize these rules as typing a variant of the do-notation in Haskell.

Strength is needed to interpret the elimination rule, since the context $\Gamma$ is available in both premises of the elimination rule. Taking $\sigma : \Gamma \times T(A) \to T(\Gamma \times A)$, we can calculate:

$$ \begin{array}{lcl} e & : & \Gamma \to T(A) \\\ e' & : & \Gamma \times A \to T(B) \\\ T(e') & : & T(\Gamma \times A) \to T^2(B) \\\ T(e'); \mu & : & T(\Gamma \times A) \to T(B) \\\ \langle id; e\rangle & : & \Gamma \to \Gamma \times T(A)\\\ \langle id; e\rangle; \sigma & : & \Gamma \to T(\Gamma \times A)\\\ \langle id; e\rangle; \sigma; T(e'); \mu & : & \Gamma \to T(B)\\\ \end{array} $$

Without the strength $\sigma$, we could not use the context $\Gamma$ in $e'$. That is, we would get introduction and elimination forms:

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : \Diamond A} $$ $$ \frac{\Gamma \vdash e : \Diamond A \qquad x : A \vdash e' : \Diamond B} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : \Diamond B} $$

I changed the notation from $T$ to $\Diamond$, since this is actually the possibility modality of S4 modal logic! These modalities arise in applications like functional languages for distributed programming --- e.g., see Murphy et al's 2004 LICS paper "A Symmetric Modal Lambda Calculus for Distributed Computing".

fixed typo
Source Link
Neel Krishnaswami
Neel Krishnaswami
  • 9.2k
  • 1
  • 30
  • 54

This answer is largely a rendition of Sridhar's comment into lambda calculus. A strong monad $T$ has the following introduction and elimination rules in the lambda calculus.

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : T(A)} $$ $$ \frac{\Gamma \vdash e : T(A) \qquad \Gamma, x : A \vdash e' : T(B)} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : T(B)} $$

You may recognize these rules as typing a variant of the do-notation in Haskell.

Strength is needed to interpret the elimination rule, since the context $\Gamma$ is available in both premises of the elimination rule. Taking $\sigma : \Gamma \times T(A) \to T(\Gamma \times A)$, we can calculate:

$$ \begin{array}{lcl} e & : & \Gamma \to T(A) \\\ e' & : & \Gamma \times A \to T(B) \\\ T(e') & : & T(\Gamma \times A) \to T^2(B) \\\ T(e'); \mu & : & T(\Gamma \times A) \to T(B) \\\ id \times e & : & \Gamma \to \Gamma \times T(A)\\\ (id \times e); \sigma & : & \Gamma \to T(\Gamma \times A)\\\ (id \times e); \sigma; T(e'); \mu & : & \Gamma \to T(B)\\\ \end{array} $$$$ \begin{array}{lcl} e & : & \Gamma \to T(A) \\\ e' & : & \Gamma \times A \to T(B) \\\ T(e') & : & T(\Gamma \times A) \to T^2(B) \\\ T(e'); \mu & : & T(\Gamma \times A) \to T(B) \\\ \langle id; e\rangle & : & \Gamma \to \Gamma \times T(A)\\\ \langle id; e\rangle; \sigma & : & \Gamma \to T(\Gamma \times A)\\\ \langle id; e\rangle; \sigma; T(e'); \mu & : & \Gamma \to T(B)\\\ \end{array} $$

Without the strength $\sigma$, we could not use the context $\Gamma$ in $e'$. That is, we would get introduction and elimination forms:

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : \Diamond A)} $$ $$ \frac{\Gamma \vdash e : \Diamond A \qquad x : A \vdash e' : \Diamond B} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : \Diamond B} $$

I changed the notation from $T$ to $\Diamond$, since this is actually the possibility modality of S4 modal logic! TheyThese modalities arise in applications like functional languages for distributed programming --- e.g., see Murphy et al's 2004 LICS paper "A Symmetric Modal Lambda Calculus for Distributed Computing".

This answer is largely a rendition of Sridhar's comment into lambda calculus. A strong monad $T$ has the following introduction and elimination rules in the lambda calculus.

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : T(A)} $$ $$ \frac{\Gamma \vdash e : T(A) \qquad \Gamma, x : A \vdash e' : T(B)} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : T(B)} $$

You may recognize these rules as typing a variant of the do-notation in Haskell.

Strength is needed to interpret the elimination rule, since the context $\Gamma$ is available in both premises of the elimination rule. Taking $\sigma : \Gamma \times T(A) \to T(\Gamma \times A)$, we can calculate:

$$ \begin{array}{lcl} e & : & \Gamma \to T(A) \\\ e' & : & \Gamma \times A \to T(B) \\\ T(e') & : & T(\Gamma \times A) \to T^2(B) \\\ T(e'); \mu & : & T(\Gamma \times A) \to T(B) \\\ id \times e & : & \Gamma \to \Gamma \times T(A)\\\ (id \times e); \sigma & : & \Gamma \to T(\Gamma \times A)\\\ (id \times e); \sigma; T(e'); \mu & : & \Gamma \to T(B)\\\ \end{array} $$

Without the strength $\sigma$, we could not use the context $\Gamma$ in $e'$. That is, we would get introduction and elimination forms:

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : \Diamond A)} $$ $$ \frac{\Gamma \vdash e : \Diamond A \qquad x : A \vdash e' : \Diamond B} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : \Diamond B} $$

I changed the notation from $T$ to $\Diamond$, since this is actually the possibility modality of S4 modal logic! They arise in applications like functional languages for distributed programming --- e.g., see Murphy et al's 2004 LICS paper "A Symmetric Modal Lambda Calculus for Distributed Computing".

This answer is largely a rendition of Sridhar's comment into lambda calculus. A strong monad $T$ has the following introduction and elimination rules in the lambda calculus.

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : T(A)} $$ $$ \frac{\Gamma \vdash e : T(A) \qquad \Gamma, x : A \vdash e' : T(B)} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : T(B)} $$

You may recognize these rules as typing a variant of the do-notation in Haskell.

Strength is needed to interpret the elimination rule, since the context $\Gamma$ is available in both premises of the elimination rule. Taking $\sigma : \Gamma \times T(A) \to T(\Gamma \times A)$, we can calculate:

$$ \begin{array}{lcl} e & : & \Gamma \to T(A) \\\ e' & : & \Gamma \times A \to T(B) \\\ T(e') & : & T(\Gamma \times A) \to T^2(B) \\\ T(e'); \mu & : & T(\Gamma \times A) \to T(B) \\\ \langle id; e\rangle & : & \Gamma \to \Gamma \times T(A)\\\ \langle id; e\rangle; \sigma & : & \Gamma \to T(\Gamma \times A)\\\ \langle id; e\rangle; \sigma; T(e'); \mu & : & \Gamma \to T(B)\\\ \end{array} $$

Without the strength $\sigma$, we could not use the context $\Gamma$ in $e'$. That is, we would get introduction and elimination forms:

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : \Diamond A)} $$ $$ \frac{\Gamma \vdash e : \Diamond A \qquad x : A \vdash e' : \Diamond B} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : \Diamond B} $$

I changed the notation from $T$ to $\Diamond$, since this is actually the possibility modality of S4 modal logic! These modalities arise in applications like functional languages for distributed programming --- e.g., see Murphy et al's 2004 LICS paper "A Symmetric Modal Lambda Calculus for Distributed Computing".

Source Link
Neel Krishnaswami
Neel Krishnaswami
  • 9.2k
  • 1
  • 30
  • 54

This answer is largely a rendition of Sridhar's comment into lambda calculus. A strong monad $T$ has the following introduction and elimination rules in the lambda calculus.

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : T(A)} $$ $$ \frac{\Gamma \vdash e : T(A) \qquad \Gamma, x : A \vdash e' : T(B)} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : T(B)} $$

You may recognize these rules as typing a variant of the do-notation in Haskell.

Strength is needed to interpret the elimination rule, since the context $\Gamma$ is available in both premises of the elimination rule. Taking $\sigma : \Gamma \times T(A) \to T(\Gamma \times A)$, we can calculate:

$$ \begin{array}{lcl} e & : & \Gamma \to T(A) \\\ e' & : & \Gamma \times A \to T(B) \\\ T(e') & : & T(\Gamma \times A) \to T^2(B) \\\ T(e'); \mu & : & T(\Gamma \times A) \to T(B) \\\ id \times e & : & \Gamma \to \Gamma \times T(A)\\\ (id \times e); \sigma & : & \Gamma \to T(\Gamma \times A)\\\ (id \times e); \sigma; T(e'); \mu & : & \Gamma \to T(B)\\\ \end{array} $$

Without the strength $\sigma$, we could not use the context $\Gamma$ in $e'$. That is, we would get introduction and elimination forms:

$$ \frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : \Diamond A)} $$ $$ \frac{\Gamma \vdash e : \Diamond A \qquad x : A \vdash e' : \Diamond B} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : \Diamond B} $$

I changed the notation from $T$ to $\Diamond$, since this is actually the possibility modality of S4 modal logic! They arise in applications like functional languages for distributed programming --- e.g., see Murphy et al's 2004 LICS paper "A Symmetric Modal Lambda Calculus for Distributed Computing".