<div dir="ltr"><div><div>Hi Johannes,<br><br></div>I believe you can parse your argument into an `Integer`, and then use `someNatVal` [1] to produce `SomeNat`, an existential (unknown) type level number. Then, you can pattern match on this to gain access to the `KnownNat` instance.<br></div><div><br></div><div>Regards,</div><div><br></div>Erik<br><div><br>[1] <a href="http://hackage.haskell.org/package/base-4.9.0.0/docs/GHC-TypeLits.html#v:someNatVal">http://hackage.haskell.org/package/base-4.9.0.0/docs/GHC-TypeLits.html#v:someNatVal</a><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 14 November 2017 at 15:01, Johannes Waldmann <span dir="ltr"><<a href="mailto:johannes.waldmann@htwk-leipzig.de" target="_blank">johannes.waldmann@htwk-leipzig.de</a>></span> wrote:<br><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/<wbr>ersatz/blob/master/tests/Z001.<wbr>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>
______________________________<wbr>_________________<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-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div><br></div>