[Haskell-cafe] how to make a KnownNat at runtime?

[dominic at steinitz.org]

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 at steinitz.org
http://idontgetoutmuch.wordpress.com