Affe

# Channels
#
# We use channels as a basic example of the various concepts available in Affe

# Prelude
# Let's assume the existence of strings
type string : un

# Channels are affine.
# This means that a channel can be used at most once.
# It can't be aliased and used by two different functions,
# but it can be "dropped", which means it can stay unused
#
# Affe supports three kinds:
# - `un` : Unrestricted, can be used arbitrarely
# - `aff` : Affine, can be used at most once
# - `lin` : Must be used exactly once
type channel : aff

# We can open a channel at a particular addresse/file/..
val open : string -> channel

# We can close a channel explicitely
val close : channel -> unit

# We can send and receive data from a channel
# Since the channel can not be aliased, this takes the handle
# on the channel, and then return it again
val send : int -> channel -> channel
val receive : channel -> int * channel

# Basic programs on channels

# Open a channel, wait for a message, send it back
let echo_once s =
  let ch = open s in
  let (msg, ch) = receive ch in
  let ch = send msg ch in
  let () = close ch in # This `close` is optional, since channels are affines.
  # let x = send msg ch in # This would fail
  ()

# A common function on channels
let with_channel s f =
  let ch = open s in
  let ch = f ch in
  close ch
  
# The type of `with_channel` is
#    ∀^a. string -> (channel -{^a}> channel) -> unit
# The annotation on the arrow indicate the linearity.
# It's time to study arrows more closely.


# Interlude on arrows
# 
# Let us consider a function that applies a closure on a range of integer

let iter_integers =
  let rec aux f i j =
  match i = j with {
  | True -> ()
  | False ->
    let () = f i in
    aux f (i+1) j
  }
  in
  aux

# This function takes a closure of type `int -{^k}> unit`
# Where `^a` is a *kind* variable that must respect the constraints `^k < unₙ`
#
# Indeed, the closure is called multiple time. if it captured anything linear,
# it could use it multiple time!

# We can try to send multiple integers by uncommenting the following code:

# let send_integers s =
#   let ch = open s in
#   let k msg = let _unused = send msg ch in () in
#   iter_integers k 0 10

# We get an error indicating than the function `k` is `affine`, as it captures
# the channel `ch` which is affine, and thus can not be passed to `iter_integers`