Type-Level Assertions (or, almost-dependent types)

Type-Level Assertions.swift

/*
 * We've defined "traits" by which we can type an integer that are characteristic of its value.
 * These traits can even be subtraits of other traits (like both positive and negative being nonzero).
 *
 * We can use these traits in the type signatures of functions to indicate what trait will be returned
 * as a function of the passed-in traits. 
 *
 * Even cooler, we can specify properties of the traits such that we can runtime-verify the correctness
 * of these labels (in case a function was improperly annotated, for example).
 */

import Foundation

@objc protocol IntegerTrait {
    static var name: String { get }    // for pretty debug messages
    static func verify(x: Int) -> Bool // for runtime verfications (assertion-like)
}

// Generic type (all other traits derive from this trait)
protocol Anything : IntegerTrait { }
@objc class Unknown : Anything {
    static let name = "Unknown"
    static func verify(x: Int) -> Bool { return true }
}

// Main types (composition of multiple subtypes)
protocol AnyNonPositive : Anything { }
@objc class NonPositive : AnyNonPositive {
    static let name = "NonPositive"
    static func verify(x: Int) -> Bool { return Zero.verify(x) || Negative.verify(x) }
}

protocol AnyNonNegative : Anything { }
@objc class NonNegative : AnyNonNegative {
    static let name = "NonNegative"
    static func verify(x: Int) -> Bool { return Zero.verify(x) || Positive.verify(x) }
}

protocol AnyNonZero : Anything { }
@objc class NonZero : AnyNonZero {
    static let name = "NonZero"
    static func verify(x: Int) -> Bool { return Positive.verify(x) || Negative.verify(x) }
}

// Subtypes (subsets of a base type)
protocol AnyPositive : AnyNonNegative, AnyNonZero { } // positives are both nonnegative and nonzero
@objc class Positive : AnyPositive {
    static let name = "Positive"
    static func verify(x: Int) -> Bool { return x > 0 }
}

protocol AnyNegative : AnyNonPositive, AnyNonZero { } // negatives are both nonpositive and nonzero
@objc class Negative : AnyNegative {
    static let name = "Negative"
    static func verify(x: Int) -> Bool { return x < 0 }
}

protocol AnyZero : AnyNonPositive, AnyNonNegative { } // zero is both nonpositive and nonnegative
@objc class Zero : AnyZero {
    static let name = "Zero"
    static func verify(x: Int) -> Bool { return x == 0 }
}

struct Integer<Trait : IntegerTrait> : IntegerLiteralConvertible, Printable {
    private var backing: Int
    
    init(_ value: Int) {
        self.backing = value
        verify()
    }
    
    init(integerLiteral value: Int) {
        self.init(value)
    }
    
    func map<T: IntegerTrait>(transform: Int -> Int) -> Integer<T> {
        return Integer<T>(transform(backing))
    }
    
    func flatMap<T: IntegerTrait>(transform: Int -> Integer<T>) -> Integer<T> {
        return transform(backing)
    }
    
    func verify() {
        assert(Trait.verify(self.backing), "Trait \"\(Trait.name)\" not satisfied by \(self).")
    }
    
    var description: String {
        get {
            return backing.description
        }
    }
}

// An example of a trait-annotated function

// Note that the first line specifies that it accepts any sort of input
// and returns only non-negative output

func abs<T: AnyPostive>(x: Integer<T>)  -> Integer<Positive>    { return _abs(x) }
func abs<T: AnyNegative>(x: Integer<T>) -> Integer<Positive>    { return _abs(x) }
func abs<T: AnyNonNegative>(x: Integer<T>) -> Integer<NonNegative>    { return _abs(x) }
func abs<T: AnyNonPositive>(x: Integer<T>) -> Integer<NonNegative>    { return _abs(x) }
func abs<T: AnyZero>(x: Integer<T>) -> Integer<Zero>    { return _abs(x) }
func abs<T: AnyNonZero>(x: Integer<T>) -> Integer<Positive>    { return _abs(x) }
func _abs<T, V>(x: Integer<T>) -> Integer<V> { return x.map { x in
    return abs(x)
}}

// We specify all different combinations of input/ouptut traits and
// all these functions call the "real" function, _negate, which contains
// the actual negation logic.

// All these other "functions" are really just specifying the traits annotations
// of the underlying function

prefix func -<T: AnyPositive>   (x: Integer<T>) -> Integer<Negative>    { return _negate(x) }
prefix func -<T: AnyNegative>   (x: Integer<T>) -> Integer<Positive>    { return _negate(x) }
prefix func -<T: AnyNonPositive>(x: Integer<T>) -> Integer<NonNegative> { return _negate(x) }
prefix func -<T: AnyNonNegative>(x: Integer<T>) -> Integer<NonPositive> { return _negate(x) }
prefix func -<T: AnyZero>       (x: Integer<T>) -> Integer<Zero>        { return _negate(x) }
prefix func -<T: AnyNonZero>    (x: Integer<T>) -> Integer<NonZero>     { return _negate(x) }
prefix func -<T: Anything>      (x: Integer<T>) -> Integer<Unknown>     { return _negate(x) }
func _negate<T,V>(x: Integer<T>) -> Integer<V> { return x.map { x in
    return abs(x)
}}

// Note that no code must be added to assert that we are returning the right type.
// Simply constructing the type inserts debug-mode assertions into the code.

// Recall that 0! = 1 and that x! will always be positive if x is positive.
// Thus, we write a factorial function that takes non-negative arguments
// and returns a positive integer.

func factorial<T: AnyNonNegative>(x: Integer<T>) -> Integer<Positive> { return _factorial(x) }
func _factorial<T,V>(x: Integer<T>) -> Integer<V> { return x.map { x in
    var y = 1
    for i in 1...x { y *= i }
    return y
}}

// Note that we use the map function on Integer so that we simply need to work with "Int"
// types instead of "Integer" types within the implementation of these functions. We effectively
// unwrap our Integer x and turn it into an Int. Then, when we return an Int, map automatically
// converts it back into the correct type of Integer and does the appropriate assertion to make sure
// that the traits are correct.

func successor<T: AnyNegative>   (x: Integer<T>) -> Integer<NonPositive>{ return _successor(x) }
func successor<T: AnyNonNegative>(x: Integer<T>) -> Integer<Positive>   { return _successor(x) }
func successor<T: Anything>      (x: Integer<T>) -> Integer<Unknown>    { return _successor(x) }
func _successor<T,V>(x: Integer<T>) -> Integer<V> { return x.map { x in
    return x.successor()
}}

// Note that the protocol name must type the argument trait  and the class name must type
// the return trait, that is, the argument traits must be "Any_____" and the return traits
// must not include the "Any".

// Note that we can specify a catch-all case with Anything -> Unknown.

func predecessor<T: AnyPositive>   (x: Integer<T>) -> Integer<NonNegative>{ return _predecessor(x) }
func predecessor<T: AnyNonPositive>(x: Integer<T>) -> Integer<Negative>   { return _predecessor(x) }
func predecessor<T: Anything>      (x: Integer<T>) -> Integer<Unknown>    { return _predecessor(x) }
func _predecessor<T,V>(x: Integer<T>) -> Integer<V> { return x.map { x in
    return x.predecessor()
}}

// Below is an example of a two-argument function:

func +<T: AnyNonNegative, U: AnyPositive>   (lhs: Integer<T>, rhs: Integer<U>) -> Integer<Positive>    { return _add(lhs, rhs) }
func +<T: AnyPositive,    U: AnyNonNegative>(lhs: Integer<T>, rhs: Integer<U>) -> Integer<Positive>    { return _add(lhs, rhs) }
func +<T: AnyNonNegative, U: AnyNonNegative>(lhs: Integer<T>, rhs: Integer<U>) -> Integer<NonNegative> { return _add(lhs, rhs) }
func +<T: AnyNegative,    U: AnyNonPositive>(lhs: Integer<T>, rhs: Integer<U>) -> Integer<Negative>    { return _add(lhs, rhs) }
func +<T: AnyNonPositive, U: AnyNegative>   (lhs: Integer<T>, rhs: Integer<U>) -> Integer<Negative>    { return _add(lhs, rhs) }
func +<T: AnyNonPositive, U: AnyNonPositive>(lhs: Integer<T>, rhs: Integer<U>) -> Integer<NonPositive> { return _add(lhs, rhs) }
func +<T: AnyPositive,    U: AnyZero>       (lhs: Integer<T>, rhs: Integer<U>) -> Integer<Positive>    { return _add(lhs, rhs) }
func +<T: AnyNegative,    U: AnyZero>       (lhs: Integer<T>, rhs: Integer<U>) -> Integer<Negative>    { return _add(lhs, rhs) }
func +<T: AnyZero,        U: AnyPositive>   (lhs: Integer<T>, rhs: Integer<U>) -> Integer<Positive>    { return _add(lhs, rhs) }
func +<T: AnyZero,        U: AnyNegative>   (lhs: Integer<T>, rhs: Integer<U>) -> Integer<Negative>    { return _add(lhs, rhs) }
func +<T: AnyZero,        U: AnyZero>       (lhs: Integer<T>, rhs: Integer<U>) -> Integer<Zero>        { return _add(lhs, rhs) }
func +<T: AnyZero,        U: AnyNonZero>    (lhs: Integer<T>, rhs: Integer<U>) -> Integer<NonZero>     { return _add(lhs, rhs) }
func +<T: AnyNonZero,     U: AnyZero>       (lhs: Integer<T>, rhs: Integer<U>) -> Integer<NonZero>     { return _add(lhs, rhs) }
func +<T: Anything,       U: Anything>      (lhs: Integer<T>, rhs: Integer<U>) -> Integer<Unknown>     { return _add(lhs, rhs) }
func _add<T,U,V>(lhs: Integer<T>, rhs: Integer<U>) -> Integer<V> { return lhs.flatMap { lhs in rhs.map { rhs in
    return lhs + rhs
}}}

// Note that we use flatMap followed by map when unwrapping our Integers since we have two arguments.
// In general, you will use n - 1 flatMaps followed by 1 map to unwrap n arguments. If you're curious
// why, feel free to ask me (@jadengeller) on Twitter.

func *<T: AnyZero,        U: Anything>      (lhs: Integer<T>, rhs: Integer<U>) -> Integer<Zero>        { return _multiply(lhs, rhs) }
func *<T: Anything,       U: AnyZero>       (lhs: Integer<T>, rhs: Integer<U>) -> Integer<Zero>        { return _multiply(lhs, rhs) }
func *<T: AnyNonZero,     U: AnyNonZero>    (lhs: Integer<T>, rhs: Integer<U>) -> Integer<NonZero>     { return _multiply(lhs, rhs) }
func *<T: AnyPositive,    U: AnyPositive>   (lhs: Integer<T>, rhs: Integer<U>) -> Integer<Positive>    { return _multiply(lhs, rhs) }
func *<T: AnyNegative,    U: AnyNegative>   (lhs: Integer<T>, rhs: Integer<U>) -> Integer<Positive>    { return _multiply(lhs, rhs) }
func *<T: AnyNonPositive, U: AnyNonPositive>(lhs: Integer<T>, rhs: Integer<U>) -> Integer<NonNegative> { return _multiply(lhs, rhs) }
func *<T: AnyNonNegative, U: AnyNonNegative>(lhs: Integer<T>, rhs: Integer<U>) -> Integer<NonNegative> { return _multiply(lhs, rhs) }
func *<T: AnyNonNegative, U: AnyNonPositive>(lhs: Integer<T>, rhs: Integer<U>) -> Integer<NonPositive> { return _multiply(lhs, rhs) }
func *<T: AnyNonPositive, U: AnyNonNegative>(lhs: Integer<T>, rhs: Integer<U>) -> Integer<NonPositive> { return _multiply(lhs, rhs) }
func *<T: Anything,       U: Anything>      (lhs: Integer<T>, rhs: Integer<U>) -> Integer<Anything>    { return _multiply(lhs, rhs) }
func _multiply<T,U,V>(lhs: Integer<T>, rhs: Integer<U>) -> Integer<V> { return lhs.flatMap { lhs in rhs.map { rhs in
    return lhs * rhs
}}}

// The following subtraction function doesn't include any type annotations. We leave adding them as
// an exercise for the reader.

// Note that it should be theoretically possible for the compiler to infer the types of these arguments
// since we are just composing other already-annotated functions, but it doesn't seem possible in Swift.
// If you can figure out a way, I'd love to know!---but I'm pretty sure you just can't.

func _subtract<T,U,V>(lhs: Integer<T>, rhs: Integer<U>) -> Integer<V> { return lhs.flatMap { lhs in rhs.map { rhs in
    return lhs - rhs
}}}

// Now for an example of using these types.

let a: Integer<Positive> = 2
let b: Integer<NonNegative> = 0

// Note that, on program execution, the types of our Integers will be verified against their values
// automatically (even here on declaration), so we won't accidentlly misannotate a value.

let result = factorial(predecessor(a + b))

// We have a compile-time guarentee that result will be positive.
// a + b resolves to a function with traits: Positive, NonNegative -> Positive
// predecessor resolves to a function with traits: Positive -> NonNegative
// factorial has traits: NonNegative -> Positive

// Try changing a's type to NonNegative as well. Our code will no longer
// compile since we can't guarentee that the predecessor of a + b will
// be a non-negative number, and factorial is only defined for non-negative
// numbers. Neat!

// We provide a coerce function if you want to verify that an integer
// is of some given type.

func coerce<T: IntegerTrait, V: IntegerTrait>(x: Integer<T>) -> Integer<V>? {
    return V.verify(x.backing) ? Integer<V>(x.backing) : nil
}

let unknown = Integer<Unknown>(5)
if let x = coerce(unknown) as Integer<NonNegative>? {
    println("The factorial of \(x) is \(factorial(x)).") // -> The factorial of 5 is 120.
}
else {
    println("The factorail of a negative number \(unknown) is undefined.")
}

// Pretty neat, huh! We just specify what we want it to be, and--if possible-- we get it!
// These sorts of checks allow us to tame run-time uncertainty right at compile-time.

// We also have a function unsafeCoerce that does not return an optional, but will crash
// if the coercion is unsuccessful. Kinda defeats the purpose, but it might be useful somewhere.

func unsafeCoerce<T: IntegerTrait, V: IntegerTrait>(x: Integer<T>) -> Integer<V> {
    return Integer<V>(x.backing)
}

let n: Integer<Positive> = 5
let m: Integer<Negative> = unsafeCoerce(n) // CRASH!!!