Dependent Types and Protocols

Evolution Discussion
1

Hey there,

I've recently worked my way through a tutorial of the language lean and found their type system super intriguing. In lean, values can implement type classes. For instance, is_even would be a type class (with the requirement that there ought to be a natural number k such that the conforming value n satisfies n=2*k). That allows for "for all" statements (which are basically functions where the dependent value with assumed properties is in contra-variant position [an input] and a protocol-conformance for the value is in covariant position [output]) and even "there is" statements (which are opaque values along with proofs that they have some properties). On top of all of that, you can actually proof some sort of equality of types and then use them basically interchangeably.

Given how Swift's protocols work and that we already have opaque return types, it felt like this would be a natural direction where to go when Swift finally introduces dependent types. I was wondering if people thing that this is at all feasible in Swift or even useful, since right now, the main use-case of such a type system seems to be proving math stuff. At least regarding the ability to use types interchangeably, I imagine that this might unlock some static optimizations, but that's just speculation at this point.

1 Like
2

I'm not sure if I understand the advantage of what you are suggesting without more detailed examples. But I think the direction Swift is currently going is to enable more domain specific language which started with things like property wrappers and function builders, but now we're also getting expression macros. Maybe those can (partly) solve what you are striving for?

Again, sorry if I misunderstood what you're trying to achieve here.

3

The really really cool thing that I would like to borrow from lean (or at least explore possibilities of doing so) is that values (not only types types) can conform to protocols. Pseudocode example where I use "valueprotocol" to describe such a protocol that applies to values:

valueprotocol<Self : Numeric> Even where 2 * witness == self {
   var witness : Self {get}
}

extension<Int> 42 : Even {
   var witness : Int {21}
}

I'm making up a lot of swift syntax in the above example which may be totally incoherent, but the idea is that you can now e.g. have a type

EvenDimMatrix<Rows : Even, Cols : Even> {...}

where the compiler knows that you have an even number of rows and an even number of columns and what it means for a value to be even.

Or you can do crazy stuff like:

extension<T : Numeric, x: T & Even, y: T & Even>
 x + y : Even {
   var witness : T {x.witness + y.witness}
}

again with made up swift syntax that may be totally incoherent, but hopefully I get my point across.

Regarding the expression macros: wow, thanks, I hadn't seen these yet! GREAT, I love it!

3 Likes
4

I don't quite get the advantage of what you're suggesting (it's also hard to understand the code with all the made-up Swift syntax :sweat_smile:), couldn't you just write something like this instead:

struct EvenInt {
  let value: Int

  init?(_ value: Int) {
    guard value % 2 == 0 else { return nil }
    self.value = value
  }
}

Of course you would need to confirm this type to all kinds of protocols that Int conforms to that you might need in the contexts where you use this type. But how is what you're suggesting different from this? Is the difference that you no longer need to conform to the Int protocols?

5

In lean, the information is encoded statically rather than dynamically and you're able to express complex relations between variables. For instance: Sure, if you already have an EvenInt, you know that %2 == 0 has passed. But how do you let the compiler know that the sum of two EvenInt is yet another EvenInt? You would have to provide another constructor and encode your knowledge of this fact rather than letting the compiler check a proof you provide.

A better approximation in contemporary Swift would be:

protocol EvenInt {
   static var half : Int {get}
}

extension EvenInt {
   static var value : Int {2 * half}
}

struct SumOfEvensIsEven<E1 : EvenInt, E2 : EvenInt> : EvenInt {
   static var half : Int {E1.half + E2.half}
}

But even there, you're just encoding your knowledge of the fact that 2*(a+b) = 2*a + 2*b rather than having the compiler check that statement at compile time.

6

There's actually a way to dynamically encode the above:

struct EvenInt {
   let half : Int
   init(half: Int) {self.half = half}
   init?(value: Int) {
      guard value % 2 == 0 else {return nil}
      self.half = value/2
   }

   static func +(lhs: Self, rhs: Self) -> Self {
      EvenInt(half: lhs.half + rhs.half)
   }   

}

But the problem that you're just encoding your knowledge rather than having the compiler check it at compile time remains.