Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Type constraints using type equality are unsound #45

Open
mxswd opened this issue Jun 19, 2014 · 10 comments
Open

Type constraints using type equality are unsound #45

mxswd opened this issue Jun 19, 2014 · 10 comments

Comments

@mxswd
Copy link
Contributor

mxswd commented Jun 19, 2014

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 mxswd added bug labels Jun 19, 2014
@mxswd
Copy link
Contributor Author

mxswd commented Jun 19, 2014

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

@mxswd mxswd closed this as completed Jun 19, 2014
@mxswd mxswd reopened this Jun 19, 2014
@mxswd mxswd changed the title Report unsound example in radar Type constraints using type equality are unsound Jun 19, 2014
@jonsterling
Copy link

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
Copy link
Member

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
Copy link

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
Copy link
Member

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
Copy link
Member

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
Copy link
Contributor Author

mxswd commented Jul 6, 2014

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

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.

@CodaFi CodaFi mentioned this issue Nov 4, 2014
@mpurland
Copy link
Member

Is this still an issue in Swift 2?

@CodaFi
Copy link
Member

CodaFi commented Nov 13, 2015

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

@CodaFi
Copy link
Member

CodaFi commented Nov 14, 2015

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

5 participants