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. |
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, On 14 November 2017 at 15:01, Johannes Waldmann <[hidden email]> wrote: Dear Cafe, _______________________________________________ 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. |
In reply to this post by Johannes Waldmann-2
I asked the same question on stackoverflow. 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 <[hidden email]>: Dear Cafe, _______________________________________________ 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. |
In reply to this post by Johannes Waldmann-2
I think the functionality you're looking for is
http://hackage.haskell.org/package/reflection-2.1.2/docs/Data-Reflection.html#v:reifyNat On Tue, Nov 14, 2017 at 6:11 AM Johannes Waldmann <[hidden email]> wrote: Dear Cafe, _______________________________________________ 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.html#v:reifyNat 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 () ... _______________________________________________ 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. |
In reply to this post by Johannes Waldmann-2
You mean something like this?
> withMatrix > :: forall z > . Matrix ℝ > -> (forall m n . (KnownNat m, KnownNat n) => L m n -> z) > -> z > withMatrix a f = > case someNatVal $ fromIntegral $ rows a of > Nothing -> error "static/dynamic mismatch" > Just (SomeNat (_ :: Proxy m)) -> > case someNatVal $ fromIntegral $ cols a of > Nothing -> error "static/dynamic mismatch" > Just (SomeNat (_ :: Proxy n)) -> > f (mkL a :: L m n) > 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 > Dominic Steinitz [hidden email] http://idontgetoutmuch.wordpress.com _______________________________________________ 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. |
Free forum by Nabble | Edit this page |