/*: | |
# Seemingly Impossible Swift Programs | |
*/ | |
/*: | |
# 1.) Completely possible programs | |
*/ | |
[1, 2, 3] | |
.allSatisfy { $0 >= 2 } | |
[1, 2, 3] | |
.allSatisfy { $0 >= 1 } | |
extension Array { | |
func anySatisfy(_ p: (Element) -> Bool) -> Bool { | |
return !self.allSatisfy { !p($0) } | |
} | |
} | |
// !(a || b) == !a && !b | |
[1, 2, 3] | |
.anySatisfy { $0 >= 4 } | |
[1, 2, 3] | |
.anySatisfy { $0 >= 1 } | |
/*: | |
# 2.) Approaching impossible programs | |
*/ | |
extension Bool { | |
static func allSatisfy(_ p: (Bool) -> Bool) -> Bool { | |
return p(true) && p(false) | |
} | |
} | |
Bool | |
.allSatisfy { $0 == true } | |
Bool | |
.allSatisfy { $0 == true || $0 == false } | |
extension CaseIterable { | |
static func allSatisfy(_ p: (Self) -> Bool) -> Bool { | |
return self.allCases.allSatisfy(p) | |
} | |
} | |
enum Direction: CaseIterable { | |
case up, down, left, right | |
} | |
Direction | |
.allSatisfy { $0 == .up } | |
extension Direction { | |
var rotatedLeft: Direction { | |
switch self { | |
case .up: return .left | |
case .left: return .down | |
case .down: return .right | |
case .right: return .up | |
} | |
} | |
var rotatedRight: Direction { | |
switch self { | |
case .up: return .right | |
case .left: return .up | |
case .down: return .left | |
case .right: return .down | |
} | |
} | |
} | |
Direction | |
.allSatisfy { $0.rotatedLeft.rotatedRight == $0 } | |
/*: | |
# 3.) Impossible programs | |
*/ | |
extension Int { | |
static func allSatisfy(_ p: (Int) -> Bool) -> Bool { | |
fatalError() | |
} | |
} | |
//Int | |
// .allSatisfy { $0 >= 0 } | |
//Int | |
// .allSatisfy { $0 % 2 == 0 || $0 % 2 == 1 } | |
extension String { | |
static func allSatisfy(_ p: (String) -> Bool) -> Bool { | |
fatalError() | |
} | |
} | |
//String | |
// .allSatisfy { $0 == "cat" } | |
//String | |
// .allSatisfy { $0.count >= 0 } | |
//func == (f: (Int) -> Int, g: (Int) -> Int) -> Bool { | |
// return Int.allSatisfy { f($0) == g($0) } | |
//} | |
/*: | |
# 4.) Seeimingly impossible programs | |
*/ | |
enum Bit { | |
case one | |
case zero | |
} | |
struct BitSequence { | |
let atIndex: (UInt) -> Bit | |
} | |
let xs = BitSequence { _ in .one } | |
let ys = BitSequence { $0 < 1000 ? .zero : .one } | |
ys.atIndex(0) | |
ys.atIndex(2000) | |
func + (head: Bit, tail: @escaping @autoclosure () -> BitSequence) -> BitSequence { | |
return BitSequence { idx in | |
idx == 0 ? head : tail().atIndex(idx - 1) | |
} | |
} | |
.one + ys | |
/*: | |
# 5.) Achieving the seemingly impossible | |
*/ | |
extension BitSequence { | |
static func allSatisfy(_ p: @escaping (BitSequence) -> Bool) -> Bool { | |
return !self.anySatisfy { !p($0) } | |
} | |
} | |
extension BitSequence { | |
static func anySatisfy(_ p: @escaping (BitSequence) -> Bool) -> Bool { | |
let found = BitSequence { idx in self.find(p).atIndex(idx)} | |
return p(found) | |
} | |
} | |
extension BitSequence { | |
static func find(_ p: @escaping (BitSequence) -> Bool) -> BitSequence { | |
if self.anySatisfy({ s in p(.zero + s) }) { | |
return .zero + self.find({ s in p(.zero + s) }) | |
} else { | |
return .one + self.find({ s in p(.one + s) }) | |
} | |
} | |
} | |
let someSequence = BitSequence.find { s in | |
s.atIndex(0) == .one | |
&& s.atIndex(2) == .one | |
&& s.atIndex(4) == .one | |
&& s.atIndex(6) == .one | |
&& s.atIndex(8) == .one | |
} | |
someSequence.atIndex(0) | |
someSequence.atIndex(1) | |
someSequence.atIndex(2) | |
someSequence.atIndex(3) | |
someSequence.atIndex(4) | |
someSequence.atIndex(5) | |
someSequence.atIndex(6) | |
someSequence.atIndex(7) | |
someSequence.atIndex(8) | |
someSequence.atIndex(9) | |
someSequence.atIndex(10) | |
someSequence.atIndex(11) | |
BitSequence | |
.allSatisfy { s in s.atIndex(0) == .zero } | |
BitSequence | |
.allSatisfy { s in s.atIndex(0) == .zero || s.atIndex(1) == .one } | |
BitSequence | |
.allSatisfy { s in s.atIndex(0) == .zero || s.atIndex(0) == .one } | |
BitSequence | |
.anySatisfy { s in s.atIndex(4) == s.atIndex(8) } | |
func == <A: Equatable> (lhs: @escaping (BitSequence) -> A, rhs: @escaping (BitSequence) -> A) -> Bool { | |
return BitSequence.allSatisfy { s in lhs(s) == rhs(s) } | |
} | |
let const1: (BitSequence) -> Int = { _ in 1 } | |
let const2: (BitSequence) -> Int = { _ in 2 } | |
const1 == const1 | |
const2 == const2 | |
const1 == const2 | |
extension Bit { | |
var toUInt: UInt { | |
switch self { | |
case .one: return 1 | |
case .zero: return 0 | |
} | |
} | |
} | |
let f: (BitSequence) -> UInt = { s in | |
s.atIndex(1).toUInt * s.atIndex(2).toUInt | |
} | |
let g: (BitSequence) -> UInt = { s in | |
s.atIndex(1).toUInt + s.atIndex(2).toUInt | |
} | |
f == f | |
g == g | |
f == g | |
let h: (BitSequence) -> UInt = { s in | |
switch (s.atIndex(1), s.atIndex(2)) { | |
case (.zero, _), (_, .zero): | |
return 0 | |
case (.one, let other), (let other, .one): | |
return other.toUInt | |
} | |
} | |
h == f | |
h == g | |
let k: (BitSequence) -> UInt = { s in | |
((s.atIndex(1).toUInt + s.atIndex(2).toUInt + 908) % 6) / 4 | |
} | |
k == f | |
k == g | |
k == h | |
/*: | |
# 6.) Topology | |
*/ | |
/*: | |
# References | |
## Infinite sets that admit fast exhaustive search | |
Martín Escardó | |
http://www.cs.bham.ac.uk/~mhe/papers/exhaustive.pdf | |
--- | |
## Synthetic topology of data types and classical spaces | |
Martín Escardó | |
http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf | |
--- | |
## Seemingly Impossible Functional Programs | |
Martín Escardó | |
http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ | |
--- | |
## The topology of Seemingly impossible functional programs (Slides) | |
Martín Escardó | |
https://www.cs.bham.ac.uk/~mhe/.talks/popl2012/escardo-popl2012.pdf | |
*/ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment