question about type lits and optimization in ghc

Carter Schonwald carter.schonwald at
Tue Aug 21 20:14:02 CEST 2012

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
{-# 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?


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the Glasgow-haskell-users mailing list