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