Skip to content

Instantly share code, notes, and snippets.

@wouter-swierstra
Created October 13, 2014 06:54
Show Gist options
  • Save wouter-swierstra/0b6062c9660e751cd535 to your computer and use it in GitHub Desktop.
Save wouter-swierstra/0b6062c9660e751cd535 to your computer and use it in GitHub Desktop.
A type-level SAT solver in Swift
// A type-level SAT solver in Swift
// Two types to model Booleans
struct True { }
struct False { }
// Negation, Conjunction, Disjunction
func not (t : True) -> False {
return False()
}
func not (f : False) -> True {
return True()
}
func and (t1:True, t2: True) -> True {
return True()
}
func and (t:True, f: False) -> False {
return False()
}
func and (f : False, t: True) -> False {
return False()
}
func and (f1:False, f2: False) -> False {
return False()
}
func or (t1:True, t2: True) -> True {
return True()
}
func or (t:True, f: False) -> True{
return True()
}
func or (f : False, t: True) -> True {
return True()
}
func or (f1:False, f2: False) -> False {
return False()
}
// The solve function is responsible for choosing how to instantiate variables
func solve<T> (problem : T -> True) -> () {
return
}
// Examples
solve{x in x} // Command-click on x - it needs to be True
solve{x,y in and(x,y)} // Both x and y need to be True
solve{x,y in and(not(x),y)} // Now x is False and y is True
// Non-examples
// This problem has no solution - it doesn't type check
// solve{x in and(x,not(x))}
// This problem has more than one solution - it doesn't type check
// solve{x,y in or(x,y)}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment