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

[Greg Horn]

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:KnownNat>
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.html#v:reifyNat

On Tue, Nov 14, 2017 at 6:11 AM Johannes Waldmann <
johannes.waldmann at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20171114/f7111e2c/attachment.html>