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

[Félix Fischer]

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?

Cheers,
Félix

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