Contents.swift

// A translation http://kcsrk.info/ocaml/types/2016/06/30/behavioural-types/
// of a translation https://hal.archives-ouvertes.fr/hal-01216310

enum Violation : ErrorProtocol {
  case Linearity
}

/* sealed */
protocol Operation { associatedtype T }
//{
  enum Read<R> : Operation { typealias T = R }
  enum Write<W> : Operation { typealias T = W }
  enum Stop : Operation { typealias T = Stop }
//}

final class Ref<A, B : Operation> {
  let contents : A
  var live : Bool

  init(_ x : A) {
    self.contents = x
    self.live = true
  }

  static func read(_ target : Ref<A, Read<B>>) -> (A, Ref<A, B>) {
    try! target.precondition()
    return (target.contents, target.refresh())
  }

  static func write(_ target : Ref<A, Write<B>>, _ update : A) -> Ref<A, B> {
    try! target.precondition()
    return Ref(update)
  }

  static func branch<C : Operation where C.T == B.T>(_ left : Ref<A, B>, _ : (Ref<A, C>) -> B) -> Ref<A, C> {
    try! left.precondition()
    return left.refresh()
  }

  private func precondition() throws {
    guard !self.live else {
      throw Violation.Linearity
    }
    self.live = false
  }

  private func refresh<C : Operation>() -> Ref<A, C> {
    return Ref<A, C>(self.contents)
  }
}

let ref : Ref<Int, Write<Read<Stop>>> = Ref(10)

/* sealed */
protocol Peano {}
//{
  enum Zero<A : Operation> : Operation, Peano { typealias T = A; case C(Ref<Int, Write<A>>) }
  enum Succ<A : Operation> : Operation, Peano { typealias T = A; case C(Ref<Int, Write<Read<A>>>) }
//}

//func foo<A : Operation, B : Operation>(_ r : Ref<Int, Zero<Write<A>>>, _ n : Int) -> Ref<Int, Write<B>> {
//  if n == 0 {
//    print("done")
//    return Ref<Int, Write<B>>.write(Ref.branch(r, { (x : Ref<Int, Write<Write<B>>>) in Zero.C(x) }), 0)
//  } else {
//    let r2 = Ref<Int, Read<B>>.write(Ref.branch(r, { (x : Ref<Int, Write<Read<B>>>) in Succ.C(x) }), 20)
//    let (v, r3) = Ref.read(r2)
//    return foo(r3, n - 1)
//  }
//}
//func foo<A : Operation, B : Operation>(_ r : Ref<Int, Succ<Ref<Int, Write<Read<A>>>>>, _ n : Int) -> Ref<Int, Write<B>> {
//  if n == 0 {
//    print("done")
//    return Ref.write(Ref.branch(r, { x in Zero.C(x) }), 0)
//  } else {
//    let r2 = Ref.write(Ref.branch(r, { x in Succ.C(x) }), 20)
//    let (v, r3) = Ref.read(r2)
//    return foo(r3, n - 1)
//  }
//}
//foo(Ref(10), 32)