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
Hi Johannes, 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. Regards, Erik [1] http://hackage.haskell.org/package/base-4.9.0.0/docs/GHC-TypeLits.html#v:som... On 14 November 2017 at 15:01, Johannes Waldmann < johannes.waldmann@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.
I asked the same question on stackoverflow <https://stackoverflow.com/questions/43399332/convert-a-list-to-list-with-type-constrained-fixed-length> . 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.
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.htm... On Tue, Nov 14, 2017 at 6:11 AM Johannes Waldmann < johannes.waldmann@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.
On 14.11.2017 17:20, Greg Horn wrote:
http://hackage.haskell.org/package/reflection-2.1.2/docs/Data-Reflection.htm...
Thanks! That is exactly what I want. - J. main :: IO () main = getArgs >>= \ case [ s ] -> reifyNat (read s :: Integer) handle handle :: forall (n::Nat) . KnownNat n => Proxy n -> IO () ...
participants (4)
-
Dmitry Olshansky -
Erik Hesselink -
Greg Horn -
Johannes Waldmann