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@swift.org https://lists.swift.org/mailman/listinfo/swift-evolution