Ha, I knew the answer lay in Richard's Gist all along. We need a way to represent implicit equality constraints on enum cases, or in the words of @rxwei:
/// A type equality guarantee is capable of safely casting one value to a
/// different type. It can only be created when `S` and `T` are statically known
/// to be equal.
struct TypeEqualityGuarantee<S, T> {
private init() {}
/// Safely cast a value to the other type.
func cast(_ value: T) -> S {
return value as! S
}
/// Safely cast a value to the other type.
func cast(_ value: S) -> T {
return value as! T
}
}
// The same-type constraint guarantees that `TypeEqualityGuarantee` is only
// constructed when `S` is statically known to be equal to `T`.
extension TypeEqualityGuarantee where S == T {
// Creates a type equality guarantee.
init() {}
}
...
// Example expression GADT.
// Each enum case has an explicit `where T == Blah` clause.
// Jordan and Matt say we should support this explicit equality clause
// in the language.
indirect enum Expression<T> {
case number(TypeEqualityGuarantee<T, Int>, Int)
case bool(TypeEqualityGuarantee<T, Bool>, Bool)
case arithmetic(TypeEqualityGuarantee<T, Int>, Arithmetic<Int>, Expression<Int>, Expression<Int>)
case compare(TypeEqualityGuarantee<T, Bool>, Comparator<Int>, Expression<Int>, Expression<Int>)
case negate(TypeEqualityGuarantee<T, Bool>, Expression<Bool>)
}
FWIW, this gist is more similar to Jordan’s first suggestion rather than the refinement that only supports same type constraints on type parameters (but not associated types).
I've wondered about difference and quotient types, as counters to sum and product types. They do exist in type theory; "difference" types are called subtypes, and just exclude certain states from their source type. Quotient types put the set of states into categories, and we work with those categories instead. I've envisioned a subtype with an "init?" that specifies which states to not support, and a quotient type as an init with a (Base) -> Base or (Base) -> Base? argument to specify the canonical values (and possibly specify values that are forbidden).
I couldn't come up too much farther, wondering what happens if we apply a base operation to a sub/quotient type and the result is a forbidden state. Do sub/quotient types fit in the framework here? What about strong type-aliases, which are a subtype with zero states removed? What about something that poses as a struct type but is actually a strong type-alias to a specific enum case? Or am I mis-groking what's going on?
I ran across a code example in swift-driver where having GADTs would make things a little bit nicer. Pasted the code below:
/// Encapsulates some of the common queries of the ExplicitDependencyBuildPlanner with error-checking
/// on the dependency graph's structure.
internal extension InterModuleDependencyGraph {
func moduleInfo(of moduleId: ModuleDependencyId) throws -> ModuleInfo {
guard let moduleInfo = modules[moduleId] else {
throw Driver.Error.missingModuleDependency(moduleId.moduleName)
}
return moduleInfo
}
func swiftModuleDetails(of moduleId: ModuleDependencyId) throws -> SwiftModuleDetails {
guard case .swift(let swiftModuleDetails) = try moduleInfo(of: moduleId).details else {
throw Driver.Error.malformedModuleDependency(moduleId.moduleName, "no Swift `details` object")
}
return swiftModuleDetails
}
func swiftPrebuiltDetails(of moduleId: ModuleDependencyId)
throws -> SwiftPrebuiltExternalModuleDetails {
guard case .swiftPrebuiltExternal(let prebuiltModuleDetails) =
try moduleInfo(of: moduleId).details else {
throw Driver.Error.malformedModuleDependency(moduleId.moduleName,
"no SwiftPrebuiltExternal `details` object")
}
return prebuiltModuleDetails
}
func clangModuleDetails(of moduleId: ModuleDependencyId) throws -> ClangModuleDetails {
guard case .clang(let clangModuleDetails) = try moduleInfo(of: moduleId).details else {
throw Driver.Error.malformedModuleDependency(moduleId.moduleName, "no Clang `details` object")
}
return clangModuleDetails
}
What is happening here is that there is a constraint between the keys and values that cannot expressed directly. Specifically, with GADTs, you could make ModuleDependencyId and ModuleInfo GADTs and give func moduleInfo a more precise type:
This is inaccurate, sorry. "Function returns specific enum case" is possible today but unsafe in the implementation because the typechecker lacks information.
From the OP:
enum Expression<T> {
case bool(Bool)
case number(Int)
}
func evaluate<T>(_ expression: Expression<T>) -> T {
switch expression {
case .bool(let bool):
return bool as! T // unsafe
case .number(let int):
return int as! T // unsafe
}
}
I should clarify: my point was that you cannot encapsulateas! (or avoid it altogether). For the module example I gave, I can wrap a dictionary in a way that encapsulates casting:
public struct ModuleDict {
// can't be of type [ModuleDependencyId<K>: ModuleInfo<K>] because there
// is no K in scope, and K can be different for different keys
var dict: [Any: Any]
// Can only add key and value if they have the same Kind
public func insert<Kind>(key: ModuleDependencyId<Kind>, value: ModuleInfo<Kind>) { ... }
public func lookup<Kind>(key: ModuleDependencyId<Kind>) throws -> ModuleInfo<Kind> {
// implementation uses as!, but that won't crash at runtime
// because the public API is impossible to misuse
try dict[key] as! ModuleInfo<Kind>
}
}
moduleDict.insert(.swift(...), .clang(...))
// ^ error: .clang case requires Kind == Clang, but Kind == Swift
In the example you've shared, someone can call evaluate<Int>(.bool(true)) without any compiler error and that would result in a runtime trap. I wouldn't call that "unsafe in the implementation" though (which in my mind implies that "the implementation does unsafe stuff but it's encapsulated so you don't have to worry about it").
After encountering a similar problem (how to safely encapsulate as!) in my weekend's project on free monads (available here: GitHub - AnarchoSystems/LazyMonad), I came up with a solution based on Church encoding (Church encoding - Wikipedia) that kind of works in today's Swift:
struct Expression<T> {
let kind : Kind
fileprivate init(_ kind: Kind){self.kind = kind}
enum Kind {
case bool(Bool, continuation: (Bool) -> T) //safe
case number(Int, continuation: (Int) -> T) //safe
}
func evaluate() -> T {
switch kind {
case .bool(let bool, let cont):
return cont(bool)
case .number(let num, let cont):
return cont(num)
}
}
}
extension Expression where T == Bool {
static func bool(_ value: Bool) -> Self {
.init(value, continuation: {$0})
}
}
extension Expression where T == Int {
static func number(_ value: Int) -> Self {
.init(value, continuation: {$0})
}
}
In my Free.xctemplate, I even have an example where the stored type differs from the type that the continuation accepts. An interpreter is then responsible for converting the stored type ("request") to the type that the continuation requires ("response") - or even bypassing the (possibly mapped) continuation altogether because the interpreter returns a T? and one can derive that nil is appropriate.