[swift-evolution] [Generics] [Pitch] Dependent Types

Félix Fischer felix91gr at gmail.com
Mon Oct 2 18:23:22 CDT 2017

Hi swift-evolution,

I’ve been thinking for the past months of making math libraries that could
benefit from a dependent types system (see the Wikipedia article:
https://en.wikipedia.org/wiki/Dependent_type?wprov=sfti1). Dependent types
would allow for the type system to enforce certain correctness in design
that otherwise would have to be test-based. It would also discourage type
hacks that sort of implement it, but have poor semantics and clarity.

Lemme give you an example:
- Let’s say you want to make a modulo arithmetic library. It has
applications in cryptography, but the fields existing there can also be
used for complete and *exact* linear algebra operations.
- Anyway. You want to make that. How?
- You’d want to have a struct that represented a number from a modulo field.
- These numbers can be multiplied, added, have inverses, etc.
- But those operations only make sense if the prime P used for the modulo
operation is the same between them. Otherwise, what’s the point?
—> (Basically, you can’t just add (2 modulo 3) with (3 modulo 5). It
doesn’t make sense)
- You could do this in many different ways, and only a few (very hacky,
“static class in a where clause”-like) will actually enforce this condition
from the type system, which afaik is usually the best way to do so; both at
compile time and at run time.

On the other hand, having dependent types allows you to have exactly this
kind of behavior:
- Now you can define a “dependent type”, for example ModuloInteger<P>,
where P is the integer value that defines the type.
- Like this, you’ll have:
—> MI<2>: {0, 1}, where 1 + 1 = 0.
—> MI<3>: {0, 1, 2}, where 1 + 1 = 2, and 2 • 2 = 1
—> ... and so on.
- Such a type system can be used for even stronger type qualities (read the
Wikipedia article for good examples).
- Such strong type qualities are super nice for any critical systems and
for math libraries in general.
- And I guess for just general correctness and documentation. It gives
better semantics to our types.

So, what do you say? Is this too crazy?


Btw if you know Haskell (which I don’t, but appreciate), you can check a
decent, Haskell-inspired, dependently typed language... here ~>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.swift.org/pipermail/swift-evolution/attachments/20171002/52fbd54c/attachment.html>

More information about the swift-evolution mailing list