writing a function to make a correspondance between type-level integers and value-level integers
I'm late to this discussion and must have missed the motivation for it. Specifically, how is your goal, vector/tensor operations that are statically assured well-dimensioned differs from general well-dimensioned linear algebra, for which several solutions have been already offered. For example, the Vectro library has been described back in 2006: http://ofb.net/~frederik/vectro/draft-r2.pdf http://ofb.net/~frederik/vectro/ The paper also talks about reifying type-level integers to value-level integers, and reflecting them back. Recent GHC extensions (like DataKinds) make the code much prettier but don't fundamentally change the game.
oleg@okmij.org wrote:
I'm late to this discussion and must have missed the motivation for it. Specifically, how is your goal, vector/tensor operations that are statically assured well-dimensioned differs from general well-dimensioned linear algebra, for which several solutions have been already offered. For example, the Vectro library has been described back in 2006: http://ofb.net/~frederik/vectro/draft-r2.pdf http://ofb.net/~frederik/vectro/
The paper also talks about reifying type-level integers to value-level integers, and reflecting them back. Recent GHC extensions (like DataKinds) make the code much prettier but don't fundamentally change the game.
Thanks Oleg for pointing out to this library. For the time being, I'm interested in doing component-free computations: http://gs1.dlut.edu.cn/newVersion/Files/dsxx/610.pdf But this library (and the corresponding article) may help me in the future. Thanks, TP
participants (2)
-
oleg＠okmij.org -
TP