I think the functionality you're looking for is reifyNat :: Integer http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#t:Integer -> (forall n. KnownNat http://hackage.haskell.org/package/base-4.8.2.0/docs/GHC-TypeLits.html#t:Kno... n => Proxy http://hackage.haskell.org/package/base-4.8.2.0/docs/Data-Proxy.html#t:Proxy n -> r) -> r http://hackage.haskell.org/package/reflection-2.1.2/docs/Data-Reflection.htm... On Tue, Nov 14, 2017 at 6:11 AM Johannes Waldmann < johannes.waldmann@htwk-leipzig.de> wrote:
Dear Cafe,
I am using type-level numbers for representing dimensions of vectors and matrices (similar to https://github.com/ekmett/ersatz/blob/master/tests/Z001.hs ) Now when I indeed know all the dimensions at compile time, (in the example code, line 20) everything works nicely.
But what do I do when the dimensions will only become available at run time?
Here is a simplified example: print the null vector where the size is read from the command line - of course in my application "handle" does more, but it essentially has the type given here.
I can extend the "case" in the "main" function to include all the values I want to handle. Looks ugly. Is there a better way?
- J.
{-# language KindSignatures, RankNTypes, LambdaCase, TypeApplications, DataKinds, ScopedTypeVariables #-}
import GHC.TypeLits import Data.Proxy import System.Environment
main :: IO () main = getArgs >>= \ case [ "2" ] -> handle (Proxy :: Proxy 2) [ "3" ] -> handle (Proxy :: Proxy 3)
handle :: forall (n::Nat) . KnownNat n => Proxy n -> IO () handle (_ :: Proxy n) = print (zero :: V n Int)
data V (n::Nat) a = V [a] deriving Show
zero :: forall (n::Nat) a . (KnownNat n, Num a) => V n a zero = V $ replicate (fromIntegral $ natVal (Proxy :: Proxy n)) 0 _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.