Kappa.scala

// Those pesky lambda expressions don't stand a chance :)
// (and certainly no more higher-order functions!)
// Behold,
trait /*The glorious*/ KappaCalculus {
  
  // rules of the game
  type Type[A]
  
  type Unit
  implicit def unitIsType: Type[Unit]
  
  type **[A, B]
  implicit def pairIsType[A : Type, B : Type]: Type[A ** B]
  
  type ->[A, B]
  
  def id[A : Type]: A -> A
  
  def bang[A : Type]: A -> Unit
  
  def comp[A : Type, B : Type, C : Type](bc: B -> C, ab: A -> B): A -> C
  
  def lift[T1 : Type, T2 : Type](e: Unit -> T1) : T2 -> (T1 ** T2)
  
  // Only kappa expressions allowed.
  def kappa[T1 : Type, T2 : Type, T3 : Type](x : (Unit -> T1) => (T2 -> T3)): (T1 ** T2) -> T3

  // play the game!
  
  def drop[T : Type] : (T ** Unit) -> Unit = 
    kappa[T, Unit, Unit](x => id[Unit])
    
  def copy[T : Type] : (T ** Unit) -> (T ** T) =
    kappa(x => comp(lift(x), x))
  
  def swap [T1 : Type, T2 : Type]: (T1 ** (T2 ** Unit)) -> (T2 ** T1) =
    kappa[T1, T2 ** Unit, T2 ** T1] { (x : Unit -> T1) =>
      kappa[T2, Unit, T2 ** T1] { (y : Unit -> T2) =>
        comp(lift(y), x)
      }
    }
  
  // might want to add
  // cancelR : T ** Unit -> T
  // cancelL : Unit ** T -> T
  // and tuple reassociation functions
  
  // see
  // http://www.megacz.com/berkeley/garrows/megacz-pop-talk.pdf
  // https://en.wikipedia.org/wiki/Kappa_calculus
  // https://en.wikipedia.org/wiki/Monoidal_category (this would fit in well)
  // for more info
  
  // coincidentally
  // https://en.wikipedia.org/wiki/Kappa_(folklore)
}

// What is Kappa's relation to Arrows?
// Can we add more structures like coproducts?
// https://ncatlab.org/nlab/show/rig+category
// Algebraic data types?