[Pitch] Dependent Types & Universes (Stage 1 of Proof-Driven Development?)

Evolution Pitches
, , ,
41

Frankly I've been waiting a long time for someone to post exactly this pitch. I think that AI (and possibly CAD) is the biggest motivation for me wanting dependent types. As AI operates more broadly in software ecosystems and programming I want tools that can prove certain restrictions in an AI's model or its output in a far more rigorous way that what's currently offered by compilers. Combining that with differential swift my hope is these can also open doors to more bespoke learning architectures to solve specific problems, or entirely different architectures that aren't based just on feed-forward neural networks. For those concerned with adding complexity to the language, I would refer to this, "Our goals for Swift are ambitious: we want to make programming simple things easy, and difficult things possible." https://www.swift.org/ -- not trying to be dismissive of concern, just pointing out the goal should be to make that complexity progressively disclose for those who want it or need it.

Yet from what I'm reading, there's already some clear stepping stones that will get us closer to this vision without yet requiring universes and dependent types in the language, as pointed out. GADTs, const functions, everything codafi pointed out, and actually mainlining auto-diff itself. Not to mention generalizing keypaths to optics and including broadcasting (there was some mention of this in this thread Ongoing work on differentiable Swift - #16 by Troy_Harvey) and whatevers' left in the generics manifesto swift/GenericsManifesto.md at main · apple/swift · GitHub.

Is there good reason "Dependent Types & Universes" is the thing that should be tackled first? Makes me wonder if there's an evolution to the GenericsManifesto or a new manifesto that can accurately capture the 30k ft view of how these pieces should connect and lay out some relative prioritization. Maybe there's a way to split up some of these ideas to be spec'd out a bit and recombined into a larger viewpoint?

P.S. I really liked the straw man syntax discussed in the thread you posted by anachron and also was very excited about that conversation before it seemed to fade away.

2 Likes
42

To elaborate a bit here, my personal wish is that those concerned with too much complexity collaborate with those like myself who really want to see this vision reach fruition, so that we meet everyone's needs.

43

Just checking: is the leading dot in the case declarations there to mark it as a GADT, or is it just an oversight? Feels strange to deviate from current case declaration syntax like that.

44

I haven't read very far yet, but I do want to make sure I understand these types correctly.

Would that be like the getValue function in this TS snippet?

interface ValueTypes {
  foo: number;
  bar: string;
}

function getValue<T extends keyof ValueTypes>(key: T): ValueTypes[T] {
  switch (key) {
    case 'foo': return 1;
    case 'bar': return '1';
  }
}

This sounds a lot like enums with associated values.

I'm struggling to think of a use case for these, but perhaps it's because I haven't yet seen them in practice.

I've seen this abused in languages that allow this, like TS and C++, resulting in things like type-level mergesort (though it's still not as bad as what constexpr allows). If there's even a slight concern about compile times now, this could cause them to explode.

1 Like
45

Sorry, that was just a typo on my part.

1 Like