<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">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">—&gt; (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&lt;P&gt;, where P is the integer value that defines the type.</div><div dir="auto">- Like this, you’ll have:</div><div dir="auto">—&gt; MI&lt;2&gt;: {0, 1}, where 1 + 1 = 0.</div><div dir="auto">—&gt; MI&lt;3&gt;: {0, 1, 2}, where 1 + 1 = 2, and 2 • 2 = 1</div><div dir="auto">—&gt; ... 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 ~&gt; <a href="https://www.idris-lang.org/">https://www.idris-lang.org/</a></div>