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