Yes. At least, that’s a really good way to implement it. On Mon, Oct 2, 2017 at 8:39 PM Taylor Swift <kelvin1...@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@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@swift.org >> https://lists.swift.org/mailman/listinfo/swift-evolution >> >> >
_______________________________________________ swift-evolution mailing list swift-evolution@swift.org https://lists.swift.org/mailman/listinfo/swift-evolution