question about type lits and optimization in ghc

[Carter Schonwald]

Hey GHC folks!

In the case where type lits (naturals specifically) are statically known
(rather than abstract), is it possible to have a sort of static copy
propagation / Singelton simplification happen at compile time? (Ie can GHC
do such things with  type lits as presently implemented?)

a simple example might be that a statically sized matrix, and being able to
specialize the stride and bounds checking at compile time (pseudo code
example follows)

data Mat (row::Nat) (col::Nat) elem = ... some vector representation


index:: (Mat r c  el) -> (Word,Word) -> el
index mt ix = ... some stride based indexing calculation that gets at the
"r"  and "c" numbers via the singletons  to translate the ix tuple into the
index into the underlying vector
representation
{-# perhaps an inline pragma? #-}

indexSpec3x3:: (Mat 3 3 el) -> (Word, Word) -> el
indexSpec3x3 smat ix = smat `index` ix

under what circumstances can i get something like the body of indexSpec3x3
to use the static type level natural number machinery to partially
specialize the computation?
Does my question even make sense as phrased?

thanks!

-Carter
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120821/3d0e9060/attachment.htm>