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

[Félix Fischer]

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

On Mon, Oct 2, 2017 at 8:39 PM Taylor Swift <kelvin13ma at 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 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/20171003/f37c96d3/attachment.html>