A **really** partial exploration of Curry-Howard correspondence in Swift

Swift-CHC-1

/// source: http://www.objc.io/books/

import Foundation

final public class Box<T> {
    public let unbox: T
    public init (_ value: T) { /// by adding '_' we can ignore the value name when we create a Box object (ex. this way we can just write something like let three = Box(3)
        self.unbox = value
    }
}

/// Enums are often calles "sum types", possibly because they are types that "collect" other types: a particular instance of an Enum will be of a certain type among the types considered by the Enum
enum Add<T, U>{
    case InLeft(Box<T>)
    case InRight(Box<U>)
}

/// Zero enum, without any type: added to any other Add type, it won't change it
enum Zero { }

/// example
typealias Add_Int_Zero = Add<Int, Zero> /// works like 'Int'

/// Int_Zero is isomorphic to Int
func convertTo_Add_Int_Zero(value: Int) -> Add_Int_Zero {
    return .InLeft(Box(value))
}
func mustReturnTrue() -> Bool {
    let five_Int: Int = 5
    let five_Add_Int_Zero = convertTo_Add_Int_Zero(five_Int)
    switch five_Add_Int_Zero {
    case .InLeft(let boxedValue):
        return boxedValue.unbox == five_Int /// this will be called, and it will return true
    default:
        return false
    }
}

/// how about multiplicating types? we use Structs
struct Times<T,U> {
    let first: T
    let second: U
}

/// One type: net "neutral" type for Times
typealias One = ()

/// we can verify the following:
/// Times<One, T> is isomorphic to T
/// Times<Zero, T> is isomorphic to Zero
/// Times<T, U> is isomorphic to Times<U, T> /// this is obvious

/// to verify the previous statements, let's explore these concepts further 

/// source: http://www.fewbutripe.com/swift/math/2015/01/06/proof-in-functions.html

/// consider the following function
func f1<A>(x: A) -> A {
    return x
}
/// the 'return x' statement is the only possible statement for this function (that is, in this case, the identity function), because we don't know anything about the type 'A', but this function must work for any type, and the identity function is the only possible function that can make it A-ok
/// for example, this functions must work and, in the identity implementation, will work for the following type
enum Empty {}
/// this type has no initializer and no value, so we CAN'T use it, we can't create any instance of it

/// ok, let's now consider the following function
func f2<A,B>(x: A, y: B) -> A {
    return x
}
/// again, in this case the only possible implementation is 'return x' but this is not the identity function

/// consider now this:
func f3<A,B>(x: A, g: A -> B) -> B {
    return g(x)
}
/// again, this is the only possible implementation, but seems actually ok in this case
/// it's the same for the following
func f4<A,B,C>(g: A -> B, h: B -> C) -> A -> C {
    return { a in h(g(a))}
}

/// consider the following generic Enum
enum Or<A,B> {
    case Left(@autoclosure () -> A)
    case Right(@autoclosure () -> B)
}
/// the '@autoclosure' statements are needed because swift needs to determine the memory layout of Enums, and with @autoclosures we say swift that we want to pass unevaluated ("lazy" as they're usually called) values
/// this 'Or' type holds both types A and B, more or less like a '(A, B)' tuple
/// here's an example of using this new type
func f5<A,B>(x: A) -> Or<A,B> {
    return Or.Left(x)
}
/// here's a more complex example
func f6<A,B,C>(x: Or<A,B>, g: A -> C, h: B -> C) -> C {
    switch x {
    case .Left(let l):
        return g(l())
    case .Right(let r):
        return h(r())
    }
}
/// 'l' and 'r' are actually closures, so we need to add the parentheses: the problem is basically the fact that Swift, unlike for example Scala, doesn't differentiate between 'val' and 'def' values, that is, values that are passed already evaluated, and valued passed as they are, without evaluation

/// up to this point, we were able to implement generic functions without knowing anything about the generic types, but there are some functions that we absolutely CAN'T implement, like the following
/*
func f<A,B>(x: A) -> B {
    ???
}
func f<A,B,C>(g: A -> C, h: B -> C) -> C {
    ???
}
*/
/// how can we differentiate functions that can be implemented from functions that can't?

/// welcome to the world of PROPOSITIONAL LOGIC

/// some definitions:

/// not: ¬
/// ¬P is false is P is true, and is false otherwise

/// implication: ⇒
/// P ⇒ Q is false if P is true and Q is false, and is true othewise (in the 3 other cases)

/// double implication: ⇔
/// P ⇔ Q is true is P and Q are both true or false, and is false otherwise (it's the opposite of XOR)

/// ∧∨ (AND, OR)
/// we can actually see the connection to what we wrote before
/// f1: P ⇒ P (tautology)
/// f2: P ∧ Q ⇒ P
/// f4: (P ⇒ Q ∧ Q ⇒ R) ⇒ (P ⇒ R)

/// basically: for every implementable function there is a corresponding logical theorem that's provably true; of course the converse is also true

/// a non-implementable function will corresponde in a false logical proposition
/// func f<A,B>(x: A) -> B corresponds to P ⇒ Q, which is clearly false (if any proposition is true, then any other proposition is true? that's of course absurd)

/// we can use this information to prove DeMorgan's law, that is:
/// ¬(P ∨ Q) ⇔ ¬P ∧ ¬Q

/// to prove the law in Swift, we need to model every logical tool we defined
/// the concept of "false" in a type system is usually modeled with a type that holds no value, for example:
enum Nothing {}

/// the negation of type A would be a function with type 'A -> Nothing', but such function cannot exist, so we will make a new type 'Not':
struct Not<A> {
    let not: A -> Nothing
}

/// we can model ∨ with the type 'Or', and we can model ∧ with the following type:
struct And<A,B> {
    let left: A
    let right: B
    init(_ left: A, _ right: B) {
        self.left = left
        self.right = right
    }
}

/// to prove the DeMorgan's law we need to write an implementable function with the same signature as the one of DeMorgan's law (actually, two functions, for the two implications):

/// ¬(P ∨ Q) ⇒ ¬P ∧ ¬Q
func deMorgan1<A,B>(f: Not<Or<A,B>>) -> And<Not<A>,Not<B>> {
    return And<Not<A>,Not<B>>(
        Not<A> { a in f.not(.Left(a))},
        Not<B> { b in f.not(.Right(b))}
    )
}

/// ¬P ∧ ¬Q ⇒ ¬(P ∨ Q)
func deMorgan2<A,B>(f: And<Not<A>,Not<B>> ) -> Not<Or<A,B>> {
    return Not<Or<A,B>> { (x : Or<A,B>) in
        switch x {
        case .Left(let a):
            return f.left.not(a())
        case .Right(let b):
            return f.right.not(b())
        }
    }
}

/// this correspondence between elements of computer science and mathematical logic is known as the Curry-Howard correspondence

/// some more examples

/// let's prove the theorem P ⇒ ¬(¬P)
func proof1<A>(x: A) -> Not<Not<A>> {
    return Not<Not<A>> { (n: Not<A>) -> Nothing in n.not(x) }
}

/// and then ¬(¬P) ⇒ P
/// actually, we can't implement this in Swift, because type theory is modeled in intuitionistic logic, in which ¬(¬P) ⇒ P is NOT true, because intuitionistic logic is constructive: we can only prove a thing by building its truth through other true propositions, and not by negating its negation

/// let's consider a curry function
func curry1<A,B,C>(f: (A, B) -> C) -> A -> B -> C {
    return { a in { b in f(a, b) } }
}
/// how is it modeled in intuitionistic logic?
/// ((A ∧ B) ⇒ C) ⇒ (A ⇒ (B ⇒ C))
/// in other words: if the fact that it's raining and there's strong wind implies the fact that I'm going to wear a waterproof jacket, then if it's raining, the fact that there's strong wind will imply that I'll wear a waterproof jacket

/// let's try to create an instance of type Not<A>
/// remember the defition of Not<A>
/*
struct Not<A> {
    let not: A -> Nothing
}
*/
/// to instantiate this we need a function of type A -> Nothing
let unit: Not<Nothing> = Not<Nothing> { x in x }
/// we basically create a Not<Nothing> instance, in which the function will simply be the identity function

/// now, since Nothing means 'false', we can say that Not<Nothing> means 'True'
typealias True = Not<Nothing>
typealias False = Nothing

/// let's prove that Times<One, T> is isomorphic to T
/// it means, in the new notation, that And<True, P> equals P, that is:
/// - if And<True, P> is True, then P is True
/// - if And<True, P> is False, then P is False, that is if Not<And<True,P>> is True, than Not<P> is True
func isomorphic1<P>(f: And<True,P>) -> P {
    return f.right
}
func isomorphic2<P>(f: Not<And<True,P>>) -> Not<P> {
    return Not<P> { p in f.not(And(unit, p)) }
}

/// let's prove that Times<Zero, T> is isomorphic to Zero
/// it means, in the new notation, that And<False, P> equals False, that is:
/// - P implies Not<And<False, P>>
/// - Not<P> implies Not<And<False, P>>
func isomorphic3<P>(f: P) -> Not<And<False, P>> {
    return Not<And<False, P>> { n in n.left }
}

func isomorphic4<P>(f: Not<P>) -> Not<And<False, P>> {
    return Not<And<False, P>> { n in n.left }
}

/// let's prove that Times<Zero, T> is NOT isomorphic to T, by absurd
/// it means, in the new notation, that And<False, P> equals P, that is:
/// - P implies And<False, P>
/// - Not<P> implies Not<And<False, P>>
/*
func isomorphic5<P>(f: P) -> And<False, P> {
    return And<False, P>(???, f) /// this can't be done!
}

func isomorphic6<P>(f: Not<P>) -> Not<And<False, P>> { /// this is identical
    return Not<And<False, P>> { n in n.left }
}
*/
///