A type-level SAT solver in Swift

gistfile1.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)}