type RulePart =
  | Expr of string
  | Text of string
  | Op of string * RulePart * RulePart
  | Color of string * RulePart
  | Frac of RulePart * RulePart
  | Space of RulePart
  member AsLatex : unit -> string
  static member ( + ) : l:RulePart * r:RulePart -> RulePart

Full name: Index.RulePart
union case RulePart.Expr: string -> RulePart
Multiple items
val string : value:'T -> string

Full name: Microsoft.FSharp.Core.Operators.string

--------------------
type string = System.String

Full name: Microsoft.FSharp.Core.string
union case RulePart.Text: string -> RulePart
union case RulePart.Op: string * RulePart * RulePart -> RulePart
union case RulePart.Color: string * RulePart -> RulePart
union case RulePart.Frac: RulePart * RulePart -> RulePart
union case RulePart.Space: RulePart -> RulePart
val x : RulePart
member RulePart.AsLatex : unit -> string

Full name: Index.RulePart.AsLatex
val format : (RulePart -> string)
val s : string
val r : RulePart
val t : RulePart
val b : RulePart
val c : string
val op : string
val l : RulePart
val l : string
val r : string
val e : RulePart

Full name: Index.e
val e1 : RulePart

Full name: Index.e1
val e2 : RulePart

Full name: Index.e2
val t : RulePart

Full name: Index.t
val t1 : RulePart

Full name: Index.t1
val t2 : RulePart

Full name: Index.t2
val tn : RulePart

Full name: Index.tn
val v : RulePart

Full name: Index.v
val v1 : RulePart

Full name: Index.v1
val v2 : RulePart

Full name: Index.v2
val vn : RulePart

Full name: Index.vn
val x : RulePart

Full name: Index.x
val s : RulePart

Full name: Index.s
val s1 : RulePart

Full name: Index.s1
val s2 : RulePart

Full name: Index.s2
val r : RulePart

Full name: Index.r
val Gamma : RulePart

Full name: Index.Gamma
val clr1 : e:RulePart -> RulePart

Full name: Index.clr1
val e : RulePart
val clr2 : e:RulePart -> RulePart

Full name: Index.clr2
val white : e:RulePart -> RulePart

Full name: Index.white
val v : RulePart
val g : RulePart
val a : RulePart
val kvd : s:string -> RulePart

Full name: Index.kvd
val ident : s:string -> RulePart

Full name: Index.ident
Multiple items
val ref : _arg1:RulePart -> RulePart

Full name: Index.ref

--------------------
type 'T ref = Ref<'T>

Full name: Microsoft.FSharp.Core.ref<_>
val failwith : message:string -> 'T

Full name: Microsoft.FSharp.Core.Operators.failwith
val effs : l:RulePart list -> RulePart

Full name: Index.effs
val l : RulePart list
Multiple items
module List

from Microsoft.FSharp.Collections

--------------------
type List<'T> =
  | ( [] )
  | ( :: ) of Head: 'T * Tail: 'T list
  interface IEnumerable
  interface IEnumerable<'T>
  member Head : 'T
  member IsEmpty : bool
  member Item : index:int -> 'T with get
  member Length : int
  member Tail : 'T list
  static member Cons : head:'T * tail:'T list -> 'T list
  static member Empty : 'T list

Full name: Microsoft.FSharp.Collections.List<_>
val reduce : reduction:('T -> 'T -> 'T) -> list:'T list -> 'T

Full name: Microsoft.FSharp.Collections.List.reduce
val rref : _arg1:RulePart -> RulePart

Full name: Index.rref
val wref : l:RulePart -> r:RulePart -> RulePart

Full name: Index.wref
val fn : x:RulePart -> f:RulePart -> t:RulePart -> RulePart

Full name: Index.fn
val f : RulePart
val abs : v:RulePart -> e:RulePart -> RulePart

Full name: Index.abs
val sem : e:RulePart -> RulePart

Full name: Index.sem
val getNews : unit -> 'a

Full name: index.getNews
val news : 'a * string
val query : Linq.QueryBuilder

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.query
val let_jdg : RulePart

Full name: Index.let_jdg
val let_drv : RulePart

Full name: Index.let_drv
val ef_gam : RulePart

Full name: Index.ef_gam
val ef_simple : RulePart

Full name: Index.ef_simple
val ef_full : RulePart

Full name: Index.ef_full
val abs_write : RulePart

Full name: Index.abs_write
val abs_access : RulePart

Full name: Index.abs_access
val abs_eff : RulePart

Full name: Index.abs_eff
val abs_coeff : RulePart

Full name: Index.abs_coeff
val sem_plain : RulePart

Full name: Index.sem_plain
val sem_coeff : RulePart

Full name: Index.sem_coeff

Coeffects: Theory of context-aware programming languages

   

Tomas Petricek, University of Cambridge
http://tomasp.net | tomas@tomasp.net | @tomaspetricek

\[\definecolor{cw}{RGB}{255,255,255} \definecolor{mc}{RGB}{0,32,172} \definecolor{cc}{RGB}{172,0,32}\]

Programming languages and context


Computing in rich environments

Execution environments are rich
but gradually more diverse

Programming context-aware
applications is hard!


Programming in rich contexts

1: 
2: 
3: 

let getNews() =
  let news = query(extern(DB), "News")
  filterByLocation(news, extern(GPS))

This is becoming important problem!

  • What resources are available?
  • What features does a device support?
  • Is the source secure and trustworthy?

Coeffects provide unified abstraction.

Checking program properties with types

Typing judgements specify program type

\[\Gamma \vdash ~{\color{mc} \text{let}}~v_1=e_1~{\color{mc} \text{in}}~e_2:\tau_2\]

Typing rules define checking procedure

\[\dfrac{ \Gamma \vdash e_1:\tau_1~~~~\Gamma, v_1:\tau_1 \vdash e_2:\tau_2 }{ \Gamma \vdash ~{\color{mc} \text{let}}~v_1=e_1~{\color{mc} \text{in}}~e_2:\tau_2 }\]

Checking effects and coeffects


Checking memory accesses with effects

Language with mutable references on the heap:

\[\Gamma=v_1:\text{ref}_{\sigma_1}\text{int}, v_2:\text{ref}_{\sigma_2}\text{int}\]

Simple type system does not tell us much:

\[\Gamma \vdash ~{\color{mc} \text{let}}~x=~! v_1~{\color{mc} \text{in}}~v_2\leftarrow x:~\text{unit}~\]

Effect systems check memory locations!

\[\Gamma \vdash ~{\color{mc} \text{let}}~x=~! v_1~{\color{mc} \text{in}}~v_2\leftarrow x:~\text{unit}~{\color{cc} ~\&~ \{~\text{read}~\sigma_1, ~\text{write}~\sigma_2\}}\]

Effect systems

What program does
(to the environment)

\[\Gamma \vdash e:\tau{\color{cc} ~\&~ \sigma}\]

  • Memory access
  • Input, output
  • Non-determinism

Coeffect systems

What program needs
(from the environment)

\[\Gamma{\color{mc} @~ r} \vdash e:\tau\]

  • Variable access
  • Resources and data
  • History, neighbours

The fun part: Typing rules

What happens when we create a function value?


\[\Gamma \vdash ~{\color{mc} \text{fun}}~x\Rightarrow v\leftarrow 42:~ ?\]

\[\Gamma \vdash ~{\color{mc} \text{fun}}~x\Rightarrow ~{\color{mc} \text{extern}}~~\text{gps}~:~ ?\]

Effectful and coeffectful functions

Effect systems delay all effects

\[\dfrac{ \Gamma, v:\tau_1 \vdash e:\tau_2{\color{cc} ~\&~ \sigma} }{ \Gamma \vdash ~{\color{mc} \text{fun}}~v\Rightarrow e:\tau_1\xrightarrow{{\color{cc} \sigma}}\tau_2 }\]

Coeffect systems split context requirements

\[\dfrac{ \Gamma, v:\tau_1{\color{cc} @~ \sigma_1\cup\sigma_2} \vdash e:\tau_2 }{ \Gamma{\color{cc} @~ \sigma_1} \vdash ~{\color{mc} \text{fun}}~v\Rightarrow e:\tau_1\xrightarrow{{\color{cc} \sigma_2}}\tau_2 }\]

Why coeffect systems matter?

Programming language theory

  • Unify systems explored before
  • Variable usage, data-flow and resources
  • Interesting and differnet shape
  • Semantics using comonad structure

Programming language practice

  • Foundations for context-aware languages

Categorical approach to semantics


Categorical approach to semantics

What is the meaning of an expression \(e\)?

\[v_1:\tau_1, \ldots, v_n:\tau_n \vdash e : \tau\]

Function between sets or morphism between objects:

\[\tau_1\times\ldots\times\tau_n \rightarrow \tau\]

Maps product of input variables to the output

Semantics of context-aware langauges

Coeffects sdd some additional structure:

\[[\![v_1:\tau_1, \ldots, v_n:\tau_n \vdash e:\tau]\!]\]

Wrap input in a comonad \({\color{cc} C}\):

\[{\color{cc} C}(\tau_1\times\ldots\times\tau_n) \rightarrow \tau\]

Semantics of context-aware langauges

Coeffects sdd some additional structure:

\[[\![v_1:\tau_1, \ldots, v_n:\tau_n{\color{cc} @~ r} \vdash e:\tau]\!]\]

Wrap input in an indexed comonad \({\color{cc} C^r}\):

\[{\color{cc} C^r}(\tau_1\times\ldots\times\tau_n) \rightarrow \tau\]

Comonadic semantics of coeffects

\[{\color{cc} C}(\tau_1\times\ldots\times\tau_n) \rightarrow \tau\]

  • Context provides additional resources
    \(~~~{\color{cc} C}\alpha = \alpha \times \Psi\)

  • Context may be missing (dead variables)
    \(~~~{\color{cc} C}\alpha = \alpha_\bot\)

  • Context provides historical values
    \(~~~{\color{cc} C}\alpha = \alpha_1 \times \ldots \times \alpha_n ~~(n \geq 1)\)

Comonadic semantics of coeffects

\[{\color{cc} C^r}(\tau_1\times\ldots\times\tau_n) \rightarrow \tau\]

  • Context provides additional resources
    \(~~~{\color{cc} C^r}\alpha = \alpha \times \psi^{\color{cc} r}\)

  • Context may be missing (dead variables)
    \(~~~{\color{cc} C^1}\alpha = \alpha~~~~{\color{cc} C^0}\alpha = \bot\)

  • Context provides historical values
    \(~~~{\color{cc} C^n}\alpha = \alpha_{\color{cc} 1} \times \ldots \times \alpha_{\color{cc} n}\)

Summary

Programming language theory problems

  • Features in small calculus
  • Type system properties
  • Programming language semantics

Context-aware programming langauges

  • Unifying languages with context
  • Interesting theory structure