Skip to content

Instantly share code, notes, and snippets.

@Kuniwak
Last active September 9, 2018 06:13
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save Kuniwak/dd17c1b87a27ce678ea3ff49d73f6be4 to your computer and use it in GitHub Desktop.
public protocol PositiveInt: Equatable {}
public struct Succ<T>: PositiveInt where T: PositiveInt {
private let x: T
fileprivate init(_ x: T) { self.x = x }
}
public struct Zero: PositiveInt {
public static func ==(lhs: Zero, rhs: Zero) -> Bool { return true }
}
public typealias One = Succ<Zero>
public typealias Two = Succ<One>
public typealias Three = Succ<Two>
public typealias Four = Succ<Three>
public typealias Five = Succ<Four>
public typealias Six = Succ<Five>
public typealias Seven = Succ<Six>
public typealias Eight = Succ<Seven>
public typealias Nine = Succ<Eight>
public typealias Ten = Succ<Nine>
public typealias Eleven = Succ<Ten>
public let zero = Zero()
public let one = Succ(zero)
public let two = Succ(one)
public let three = Succ(two)
public let four = Succ(three)
public let five = Succ(four)
public let six = Succ(five)
public let seven = Succ(six)
public let eight = Succ(seven)
public let nine = Succ(eight)
public let ten = Succ(nine)
public let eleven = Succ(ten)
func main() {
let r = add(one, two)
print(type(of: r))
// Succ(Succ(Succ(Zero))) -> Three
}
public func add<A>(_ a: A, _ b: Zero) -> A { return a }
public func add<B>(_ a: Zero, _ b: B) -> B { return b }
public func add(_ a: One, _ b: One) -> Two { return Succ(b) }
public func add(_ a: One, _ b: Two) -> Three { return Succ(b) }
public func add(_ a: One, _ b: Three) -> Four { return Succ(b) }
public func add(_ a: One, _ b: Four) -> Five { return Succ(b) }
public func add(_ a: One, _ b: Five) -> Six { return Succ(b) }
public func add(_ a: One, _ b: Six) -> Seven { return Succ(b) }
public func add(_ a: One, _ b: Seven) -> Eight { return Succ(b) }
public func add(_ a: One, _ b: Eight) -> Nine { return Succ(b) }
public func add(_ a: One, _ b: Nine) -> Ten { return Succ(b) }
public func add(_ a: One, _ b: Ten) -> Eleven { return Succ(b) }
public func add(_ a: One, _ b: Eleven) -> Zero { return zero }
public func add(_ a: Two, _ b: One) -> Three { return Succ(Succ(b)) }
public func add(_ a: Two, _ b: Two) -> Four { return Succ(Succ(b)) }
public func add(_ a: Two, _ b: Three) -> Five { return Succ(Succ(b)) }
public func add(_ a: Two, _ b: Four) -> Six { return Succ(Succ(b)) }
public func add(_ a: Two, _ b: Five) -> Seven { return Succ(Succ(b)) }
public func add(_ a: Two, _ b: Six) -> Eight { return Succ(Succ(b)) }
public func add(_ a: Two, _ b: Seven) -> Nine { return Succ(Succ(b)) }
public func add(_ a: Two, _ b: Eight) -> Ten { return Succ(Succ(b)) }
public func add(_ a: Two, _ b: Nine) -> Eleven { return Succ(Succ(b)) }
public func add(_ a: Two, _ b: Ten) -> Zero { return zero }
public func add(_ a: Two, _ b: Eleven) -> One { return one }
// ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment