how to make a KnownNat at runtime?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

how to make a KnownNat at runtime?

Johannes Waldmann-2
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.
Reply | Threaded
Open this post in threaded view
|

Re: how to make a KnownNat at runtime?

Erik Hesselink
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

On 14 November 2017 at 15:01, Johannes Waldmann <[hidden email]> 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.


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: how to make a KnownNat at runtime?

Dmitry Olshansky
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,

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.


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: how to make a KnownNat at runtime?

Greg Horn
In reply to this post by Johannes Waldmann-2
I think the functionality you're looking for is

reifyNat :: Integer -> (forall n. KnownNat n => Proxy n -> r) -> r  

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,

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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: how to make a KnownNat at runtime?

Johannes Waldmann-2
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.
Reply | Threaded
Open this post in threaded view
|

Re: how to make a KnownNat at runtime?

Dominic Steinitz-2
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.