Difference between revisions of "Talk:Type arithmetic"
(Why?) |
(Is this why?) |
||
| Line 1: | Line 1: | ||
| + | == Why? == |
||
| + | |||
This page seems to explain ''what'' but not ''why''. I don't know about anyone else, but when I read 'arithmetic at the type level', the very first thought that pops into my head is 'why in the name of God would you ''want'' to do such an insane thing?' [[User:MathematicalOrchid|MathematicalOrchid]] 11:53, 12 March 2007 (UTC) |
This page seems to explain ''what'' but not ''why''. I don't know about anyone else, but when I read 'arithmetic at the type level', the very first thought that pops into my head is 'why in the name of God would you ''want'' to do such an insane thing?' [[User:MathematicalOrchid|MathematicalOrchid]] 11:53, 12 March 2007 (UTC) |
||
| + | |||
| + | == This why? == |
||
| + | |||
| + | Following some discussions in #haskell, I understand this is related to that widespread Haskell obsession with attempting to "prove" things about programs (in spite of the fact that this is obviously impossible). |
||
| + | |||
| + | If I'm understanding this right, the idea is to be able to construct a type that means not merely "a List containing Integers", but "a List containing at least 6 Integers". And the "arithmetic" part comes in when one wants to say something like |
||
| + | |||
| + | : "This function takes a List containing at least X objects of type T and another List containing at least Y objects of type T, and returns a List containing at least X+Y objects of type T." |
||
| + | |||
| + | In other words, the "arithmetic" part is calculating X+Y at compile-time. And any function that calls the one so-described must prove to the type system that it satisfies the constrains. And, once the constraints are statically verified, no further runtime checks are required. |
||
| + | |||
| + | Is that roughly what this is all about? (And if so, can somebody add some statements to that effect to the content page?) [[User:MathematicalOrchid|MathematicalOrchid]] 20:07, 12 March 2007 (UTC) |
||
Revision as of 20:07, 12 March 2007
Why?
This page seems to explain what but not why. I don't know about anyone else, but when I read 'arithmetic at the type level', the very first thought that pops into my head is 'why in the name of God would you want to do such an insane thing?' MathematicalOrchid 11:53, 12 March 2007 (UTC)
This why?
Following some discussions in #haskell, I understand this is related to that widespread Haskell obsession with attempting to "prove" things about programs (in spite of the fact that this is obviously impossible).
If I'm understanding this right, the idea is to be able to construct a type that means not merely "a List containing Integers", but "a List containing at least 6 Integers". And the "arithmetic" part comes in when one wants to say something like
- "This function takes a List containing at least X objects of type T and another List containing at least Y objects of type T, and returns a List containing at least X+Y objects of type T."
In other words, the "arithmetic" part is calculating X+Y at compile-time. And any function that calls the one so-described must prove to the type system that it satisfies the constrains. And, once the constraints are statically verified, no further runtime checks are required.
Is that roughly what this is all about? (And if so, can somebody add some statements to that effect to the content page?) MathematicalOrchid 20:07, 12 March 2007 (UTC)