Timeline for Is there a practical use for dependent types?
Current License: CC BY-SA 4.0
Post Revisions
19 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 22, 2023 at 13:33 | answer | added | lyhokia | timeline score: 1 | |
| Jul 8, 2020 at 13:46 | vote | accept | zooby | ||
| Nov 23, 2019 at 9:00 | history | tweeted | twitter.com/StackSoftEng/status/1198164432884514816 | ||
| Nov 19, 2019 at 0:28 | comment | added | Eric Lippert | You might be interested in the example of how to type tensors used in machine learning and other applications of linear algebra. A tensor is logically an array of arbitrarily many dimensions; making a type system flexible enough to check the correctness of code that does complex tensor manipulations is quite tricky. | |
| Nov 18, 2019 at 18:52 | comment | added | user833970 | Programmer's have very different notions of what "every day" language should mean. You may be interested in ATS, ats-lang.org which aims to be a systems language like C/C++. Or Idris, idris-lang.org which aims to be a high level language like Haskell. | |
| Nov 18, 2019 at 14:38 | comment | added | Jared Smith | Ever have a divide by zero error? Ever wish you could constrain the divisor to be a non-zero integer (or even a counting number!) statically at compile time? Statically verify you can't have a null reference? I don't understand how you could possibly not find stuff like that practical... now whether such verification can be done fast enough to be useful is a practical consideration. | |
| Nov 18, 2019 at 13:06 | comment | added | Giacomo Alzetta | You can follow exactly the same "logic" to end up claiming that any type system is "useless". Type systems are a continuum of "logic systems", the types are formulas and the functions/programs are the corresponding proofs. The more refined the logic the more expressive the formulas and thus the harder to write a proof, because it has to be very precise... this means only a few programs have that type which means there is small room for errors once the code compiles. The less refined the formulas, the easier to write bogus proofs that produce buggy programs. | |
| Nov 18, 2019 at 10:58 | answer | added | MSalters | timeline score: 7 | |
| Nov 18, 2019 at 9:32 | history | became hot network question | |||
| Nov 18, 2019 at 4:22 | comment | added | Theraot | @zooby yes, although there is value in that for library authors. You could do a lot of 1D, 2D, 3D, and 4D in one swap, even if the final application will only use, say 3D. | |
| Nov 18, 2019 at 3:44 | history | edited | zooby | CC BY-SA 4.0 |
added 60 characters in body
|
| Nov 18, 2019 at 3:44 | comment | added | zooby | @Theraort Usually we use vectors of a given length like 3 dimensional. Rather than having functions output vectors of arbitrary length depending on the paramters of the function. | |
| Nov 18, 2019 at 1:44 | answer | added | Theraot | timeline score: 7 | |
| Nov 18, 2019 at 1:28 | answer | added | Karl Bielefeldt | timeline score: 20 | |
| Nov 18, 2019 at 1:20 | comment | added | Theraot | Isn't your example useful in game development? We use a lot of linear and vector algebra there. Sometimes a bit of calculus. | |
| Nov 17, 2019 at 22:44 | comment | added | zooby | @Telastyn true but I mean like, it's not trying to prove Fermat's Last Theorem using set theory. | |
| Nov 17, 2019 at 22:20 | review | Close votes | |||
| Nov 23, 2019 at 3:00 | |||||
| Nov 17, 2019 at 21:55 | comment | added | Telastyn | You ask like everyday programming isn’t abstract logic... | |
| Nov 17, 2019 at 21:50 | history | asked | zooby | CC BY-SA 4.0 |