Skip to content

Instantly share code, notes, and snippets.

@JadenGeller
Last active March 9, 2018 03:06
Show Gist options
  • Save JadenGeller/f39130616846f9bf9879 to your computer and use it in GitHub Desktop.
Save JadenGeller/f39130616846f9bf9879 to your computer and use it in GitHub Desktop.
Type-Level Assertions (or, almost-dependent types)
/*
* 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!!!
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment