<div dir="ltr">I asked the same question on <a href="https://stackoverflow.com/questions/43399332/convert-a-list-to-list-with-type-constrained-fixed-length">stackoverflow</a>.<div><br><div>It is impossible now. If it is possible we have a language with dependent types. Unfortunately we haven't it at least till 2020.</div></div><div><br></div><div>I spent some time trying to find a decision but had no success. Success here means a bug in type system.</div><div><br></div><div>Regards,</div><div>Dmitry</div></div><div class="gmail_extra"><br><div class="gmail_quote">2017-11-14 17:01 GMT+03:00 Johannes Waldmann <span dir="ltr"><<a href="mailto:johannes.waldmann@htwk-leipzig.de" target="_blank">johannes.waldmann@htwk-leipzig.de</a>></span>:<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>