Proofing Products / Tuples ...

ProofofProducts.swift

precedencegroup Apply {
  higherThan: ComparisonPrecedence
  associativity: right
}

precedencegroup Compose {
  higherThan: Apply
}

infix operator ⚬ : Compose
infix operator <*> : Apply

// --------------------------------------------------------------------------------
// MARK: - Arrow
// --------------------------------------------------------------------------------

struct Arrow<F, T> {

  let c: (F) -> T

  func apply(_ f: F) -> T {
    return c(f)
  }

  init(_ c: @escaping (F) -> T){
    self.c = c
  }
}


func <*> <A1, A2>(_ arr: Arrow<A1, A2>, _ a1: A1) -> A2 {
  return arr.apply(a1)
}

func ⚬ <A1, A2, A3>(_ a1: Arrow<A1, A2>, _ a2: Arrow<A2, A3>) -> Arrow<A1, A3> {
  return Arrow { a2 <*> a1 <*> $0 }
}

// --------------------------------------------------------------------------------
// MARK: - Product
// --------------------------------------------------------------------------------

protocol Product {
  associatedtype Fst
  associatedtype Snd
  var fst: Fst { get }
  var snd: Snd { get }
}

struct Tuple<A: Equatable, B: Equatable>: Product, Equatable {
  let fst: A
  let snd: B

  public static func ==(lhs: Tuple<A,B>, rhs: Tuple<A,B>) -> Bool {
    return lhs.fst == rhs.fst && lhs.snd == rhs.snd
  }
}

// --------------------------------------------------------------------------------
// MARK: - Product
// --------------------------------------------------------------------------------

func fork<A>(_ a: A) -> Tuple<A, A> {
  return Tuple<A, A>(fst: a, snd: a)
}

func fst<A: Product>(_ t: A) -> A.Fst {
  return t.fst
}

func snd<A: Product>(_ t: A) -> A.Snd {
  return t.snd
}

func id<A>(_ t: A) -> A {
  return t
}

// --------------------------------------------------------------------------------
// MARK: - Proof
// --------------------------------------------------------------------------------

struct Proof<A, B, C, X> where
A: Equatable, B: Equatable, C: Equatable, X: Product {

  let a1: Arrow<C, X>
  let a2: Arrow<X, A>
  let a3: Arrow<X, B>
  let a4: Arrow<C, A>
  let a5: Arrow<C, B>

  init(_ a1: @escaping (C) -> X,
       _ a2: @escaping (X) -> A,
       _ a3: @escaping (X) -> B,
       _ a4: @escaping (C) -> A,
       _ a5: @escaping (C) -> B) {
    self.a1 = Arrow(a1)
    self.a2 = Arrow(a2)
    self.a3 = Arrow(a3)
    self.a4 = Arrow(a4)
    self.a5 = Arrow(a5)
  }

  func perform(with c: C) -> Bool {
    guard a1 ⚬ a2 <*> c == a4 <*> c,
          a1 ⚬ a3 <*> c == a5 <*> c
      else { return false }
    return true
  }
}


let proof: Proof<String, String, String, Tuple<String, String>> = Proof(fork, fst, snd, id, id)
proof.perform(with: "a")


typealias T2S = Tuple<String, String>
let proof2: Proof<T2S, T2S, T2S, T2S> = Proof(id, id, id, id, id)
proof2.perform(with: Tuple(fst:"a", snd: "b"))

let proof3: Proof<String, String, T2S, T2S> = Proof(id, fst, snd, fst, snd)
proof3.perform(with: Tuple(fst:"a", snd: "b"))