<div><div dir="auto">Yes. At least, that’s a really good way to implement it.</div><br><div class="gmail_quote"><div>On Mon, Oct 2, 2017 at 8:39 PM Taylor Swift <<a href="mailto:kelvin13ma@gmail.com">kelvin13ma@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>don’t we need something like this for Fixed Size Arrays™ too?<br></div><div class="gmail_extra"><br><div class="gmail_quote"></div></div><div class="gmail_extra"><div class="gmail_quote">On Mon, Oct 2, 2017 at 6:23 PM, Félix Fischer via swift-evolution <span><<a href="mailto:swift-evolution@swift.org" target="_blank">swift-evolution@swift.org</a>></span> wrote:<br></div></div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">Hi swift-evolution,</div><div dir="auto"><br></div><div dir="auto">I’ve been thinking for the past months of making math libraries that could benefit from a dependent types system (see the Wikipedia article: <a href="https://en.wikipedia.org/wiki/Dependent_type?wprov=sfti1" target="_blank">https://en.wikipedia.org/wiki/Dependent_type?wprov=sfti1</a>). 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.</div><div dir="auto"><br></div><div dir="auto">Lemme give you an example:</div><div dir="auto">- 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 <b>exact</b> linear algebra operations. </div><div dir="auto">- Anyway. You want to make that. How?</div><div dir="auto">- You’d want to have a struct that represented a number from a modulo field.</div><div dir="auto">- These numbers can be multiplied, added, have inverses, etc.</div><div dir="auto">- 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?</div><div dir="auto">—> (Basically, you can’t just add (2 modulo 3) with (3 modulo 5). It doesn’t make sense)</div><div dir="auto">- 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.</div><div dir="auto"><br></div><div dir="auto">On the other hand, having dependent types allows you to have exactly this kind of behavior:</div><div dir="auto">- Now you can define a “dependent type”, for example ModuloInteger<P>, where P is the integer value that defines the type.</div><div dir="auto">- Like this, you’ll have:</div><div dir="auto">—> MI<2>: {0, 1}, where 1 + 1 = 0.</div><div dir="auto">—> MI<3>: {0, 1, 2}, where 1 + 1 = 2, and 2 • 2 = 1</div><div dir="auto">—> ... and so on.</div><div dir="auto">- Such a type system can be used for even stronger type qualities (read the Wikipedia article for good examples).</div><div dir="auto">- Such strong type qualities are super nice for any critical systems and for math libraries in general.</div><div dir="auto">- And I guess for just general correctness and documentation. It gives better semantics to our types.</div><div dir="auto"><br></div><div dir="auto">So, what do you say? Is this too crazy?</div><div dir="auto"><br></div><div dir="auto">Cheers,</div><div dir="auto">Félix</div><div dir="auto"><br></div><div dir="auto">Btw if you know Haskell (which I don’t, but appreciate), you can check a decent, Haskell-inspired, dependently typed language... here ~> <a href="https://www.idris-lang.org/" target="_blank">https://www.idris-lang.org/</a></div>
<br></blockquote></div></div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">_______________________________________________<br>
swift-evolution mailing list<br>
<a href="mailto:swift-evolution@swift.org" target="_blank">swift-evolution@swift.org</a><br>
<a href="https://lists.swift.org/mailman/listinfo/swift-evolution" rel="noreferrer" target="_blank">https://lists.swift.org/mailman/listinfo/swift-evolution</a><br>
<br></blockquote></div><br></div>
</blockquote></div></div>