[Generics] [Pitch] Dependent Types

Evolution Pitches
1

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:
Dependent type - Wikipedia). 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/

3 Likes
2

don’t we need something like this for Fixed Size Arrays™ too?

···

On Mon, Oct 2, 2017 at 6:23 PM, Félix Fischer via swift-evolution < swift-evolution@swift.org> wrote:

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:
Dependent type - Wikipedia). 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/

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution

3

I rather suspect that we would be best served by starting with integer
literals as the only accepted “values in generics”. This would let us
define fixed-size arrays and matrices, the modular arithmetic types you
describe, and several other mathematical entities.

Nevin.

4

Yes. At least, that’s a really good way to implement it.

···

On Mon, Oct 2, 2017 at 8:39 PM Taylor Swift <kelvin13ma@gmail.com> wrote:

don’t we need something like this for Fixed Size Arrays™ too?

On Mon, Oct 2, 2017 at 6:23 PM, Félix Fischer via swift-evolution < > swift-evolution@swift.org> wrote:

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:
Dependent type - Wikipedia). 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/

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution