Last active
September 9, 2018 06:13
Star
You must be signed in to star a gist
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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