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

[Taylor Swift]

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 at 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:
> 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/
>
> _______________________________________________
> swift-evolution mailing list
> swift-evolution at swift.org
> https://lists.swift.org/mailman/listinfo/swift-evolution
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.swift.org/pipermail/swift-evolution/attachments/20171002/071f2099/attachment.html>