Weekend plans never work out for me. My priority is my family, so of course there really isn't much time for programming. The few times I can do some programming on the weekends are Friday and Saturday evening while Emily is working. Sometimes I'm busy reading a book, though I guess I did a little bit with a riverpod like framework for Koka. Not much though. Just trying to understand Riverpod's internals right now. Anyways, I got an email from Daan today about him releasing a new version of Koka today with fbip / fip keyword support. It sounds like he wants to do a Koka release with VSCode support in August, so we are going to talk next week about what should go into that release I think.

Thoughts below about Demand CFA for Algebraic Effects.

I'm thinking about how to adjust demand-CFA for algebraic effects:

The bind function should know about all the names of imported effect functions. If we are calling an effect then we have to figure out what calls the innermost lambda, (since there is no binding site).

Okay lets take a step back to the basics. Lets start with the lambda calculus augmented with algebraic effect operators.

TODO: If, Patterns

$$\begin{align*} l &\in \textbf{Literal} \\ x &\in \textbf{Var} & e &\in \textbf{Exp} \\ \ell &\in \textbf{Label} & t &\in \textbf{Term} \\ \\ e &\Coloneqq t^l \\ t &\Coloneqq App\; e\; e \mid Lam\; x\; e \mid x \\ \end{align*}$$

$$\begin{align*} v &\in \textbf{Value} \\ \rho &\in \textbf{Env} \\ c &\in \textbf{Call Context}\\ \\ v &\Coloneqq (Lam, \rho) \mid l \\ \rho &\Coloneqq\; \perp\; \mid \{ x \mapsto v \} \\ c &\Coloneqq\; \langle \rangle \mid \ell :: c \end{align*}$$

$$\renewcommand\Epsilon{\mathcal{E}} \newcommand\flowToRel{(\hat{C},\hat{\Epsilon})\models_\text{fseval}} \newcommand\callsRel{(\hat{C},\hat{\Epsilon})\models_\text{fscall}} \newcommand\lam{\lambda x.e} \newcommand\term[1]{t_#1^{\ell_#1}} \begin{align*} &[REF]\; & &\flowToRel x^\ell & \textit{iff}\; & (\lam)^{\ell_b} = \text{bind}_{fs}(x,x^\ell) \land \callsRel (\lam,(\lam)^{\ell_b}) \land \\ & & & & &\forall (\term{0} \term{1})^{\ell_2} \in \hat{\Epsilon}(e), \flowToRel \term{1} \land \hat{C}(\ell_1) \subseteq \hat{C}(\ell) \\ &[LAM]\; & &\flowToRel (\lam)^\ell & \textit{iff}\; & {\lam} \subseteq \hat{C}(\ell) \\ &[APP]\; & &\flowToRel (\term{0} \term{1})^\ell & \textit{iff}\; & \flowToRel \term{0} \land \\ & & & & &\forall\lambda x.\term{2} \in \hat{C}(\ell_0), \flowToRel \term{2} \land \hat{C}(\ell_2) \subseteq \hat{C}(\ell) \\ \end{align*}$$