Type constraints using type equality are unsound

[mxswd]

Radar submitted. Radar: 17377676

---

With https://github.com/maxpow4h/swiftz/blob/54870ca7b81a2595b3707646cba4d83a71bb6667/swiftz/TypeEquality.swift and https://github.com/maxpow4h/swiftz/blob/54870ca7b81a2595b3707646cba4d83a71bb6667/swiftz/List.swift#L47-L56 you can show Int =:= String and define the function:

func apply(a: Int) -> String {
  return a
}

that correctly type checks, showing unsoundness.

---

Commentary: It appears swift isn't fully obeying the type constraints provided in where clauses.

[mxswd]

import Foundation

protocol TypeEquality {
  typealias From
  typealias To
  func apply(a: From) -> To
}

struct Refl<X> : TypeEquality {
  typealias From = X
  typealias To = X
  func apply(a: From) -> To {
    return a
  }
}

struct Tuple2<A, B> {
  typealias T = (A, B)
}

extension Array {
  func lookup<Key: Equatable, Value, EV: TypeEquality where EV.From == T, EV.To == Tuple2<Key, Value>.T>(ev: EV, key: Key) -> Value? {
    return nil
  }
}

let xs: Array<Int> = []

let r: String? = xs.lookup(Refl(), key: 1)
//     ^ This is impossible, Refl.apply is Int -> String

[jonsterling]

There seems to be a much more fundamental problem with this definition beyond the bug in the typechecker: You've essentially defined equality of types S,T to be witnessed by a single function S -> T. By this definition, every type is equal to any pointed type.

struct UtterlyBroken<T> : TypeEquality {
    typealias A = T
    typealias B = String
    func coe(a: A) -> B {
        return "Welp";
    }
}

It is not clear to me that a TypeEquality type can be expressed in Swift, since it would seem that at the very least you would need to be able to be polymorphic over type constructors to achieve Leibniz equality, which is not presently possible. I suggest that things like this which are presently not possible be avoided, since it seems more harmful than helpful to cloak incorrect definitions in the trust-inducing vocabulary of Type Theory.

[pthariensflame]

Once we get sealed hierarchies, we'll be able to express it as:

@sealed protocol TypeEquality {
  typealias A
  typealias B
  func apply(v : A) -> B
  var inverse: TypeEquality<B, A> { get }
}
struct Refl<X>: TypeEquality {
  typealias A = X
  typealias B = X
  func apply(v: X) -> X {
    return v
  }
  var inverse {
    return self
  }
}

I agree with @jonsterling though, and would get rid of this until then.

[jonsterling]

Seems to me that a much better solution would be to wait until we've got higher-kinded quantification and then just give leibniz equality...

[pthariensflame]

Or wait until this works:

struct TypeEquality<X, Y> where X: Y && Y: X { ... }

I seriously doubt Swift is gaining higher kinds any time soon. :(

[pthariensflame]

I just confirmed that the following code causes the compiler to segfault:

protocol TypeEquality {
  typealias A: B
  typealias B: A
  func apply(v: A) -> B
  func unapply(v: B) -> A
}

struct Refl<X>: TypeEquality {
  typealias A = X
  typealias B = X
  func apply(v: X) -> X {
    return v
  }
  func unapply(v: X) -> X {
    return v
  }
}

[mxswd]

@jonsterling Yup, I agree. I removed it in 4959b4d428989ee6386024386cf51db0b9c40a16.

One point though, type equality is definitely expressible in swift in a sound way, as a function. https://github.com/maxpow4h/swiftz/blob/master/swiftz_core/swiftz_core/List.swift#L55-L64

Leibniz equality would also be much better. One day...

On the representation, I think sealed / closed protocols would stop people from defining their own axioms.

[mpurland]

Is this still an issue in Swift 2?

[CodaFi]

Yeah. Terrible, really, that all of this still works.

[CodaFi]

The last time I had a crack at this, the problem was if you tried to express something like X : Y, Y : X or X == Y, Y == X, Swift would complain about you having a duplicate type variable -- which is kind of the point, and this is when it doesn't outright crash. It's disgusting trying to express these kinds of equalities still.