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