18 Jun 2013 07:37

## 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.
```
22 Jun 2013 15:54

### Re: writing a function to make a correspondance between type-level integers and value-level integers

```oleg <at> 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
```

Gmane