You mean something like this?

withMatrix :: forall z . Matrix ℝ -> (forall m n . (KnownNat m, KnownNat n) => L m n -> z) -> z withMatrix a f = case someNatVal $ fromIntegral $ rows a of Nothing -> error "static/dynamic mismatch" Just (SomeNat (_ :: Proxy m)) -> case someNatVal $ fromIntegral $ cols a of Nothing -> error "static/dynamic mismatch" Just (SomeNat (_ :: Proxy n)) -> f (mkL a :: L m n)

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

Dominic Steinitz dominic@steinitz.org http://idontgetoutmuch.wordpress.com