Can I get KnownNat n to mean KnownNat (n * 3) etc.?

Question

I work with the data types of this form using V from linear :

 type Foo n = V (n * 3) Double -> Double 

Fixed to n , this is very important because I want to be able to ensure that I go through the right amount of elements at compile time. This is part of my program that is already working well, regardless of what I'm doing here.

For any KnownNat n I can generate a Foo n that satisfies the behavior that my program requires. For the purposes of this question it may be something stupid like

 mkFoo :: KnownNat (n * 3) => Foo n mkFoo = sum 

Or for a more meaningful example, it can generate a random V the same length and use dot for the two. The KnownNat restriction is redundant here, but in fact it needs to make Foo . I make one Foo and use it for my entire program (or with multiple inputs), so this guarantees me that whenever I use it, I use things with the same length and on what the Foo structure dictates.

And finally, I have a function that introduces inputs for Foo :

 bar :: KnownNat (n * 3) => Proxy n -> [V (n * 3) Double] 

bar is actually the reason that I use n * 3 as a type function, rather than just manually extending it. The reason is that bar can do its job using three vectors of length n and attaching them all together as a vector of length n * 3 . In addition, n is a much more significant parameter for a function, semantically than n * 3 . It also allows me to forbid invalid values ​​like n which are not a multiple of 3, etc.

Now, before, everything worked fine, as long as I defined the type synonym at the beginning:

 type N = 5 

And I can just pass Proxy :: Proxy N to bar and use mkFoo :: Foo N And it worked fine.

 -- works fine doStuff :: [Double] doStuff = let inps = bar (Proxy :: Proxy N) in map (mkFoo :: Foo N) inps 

But now I want to configure n at run time, loading information from a file or from command line arguments.

I tried to do this by calling reflectNat :

 doStuff :: Integer -> Double doStuff n = reflectNat 5 $ \ pn@ (Proxy :: Proxy n) -> let inps = bar (Proxy :: Proxy n) in map (mkFoo :: Foo n) inps 

But ... bar and mkFoo require KnownNat (n * 3) , but reflectNat just gives me KnownNat n .

Is there any way to generalize the proof that reflectNat allows me to satisfy Foo ?

Answer 1

I am sending another answer, since it is more direct, editing the previous one does not make sense.

In fact, using the trick (popularized, if not invented by Edward Kmett), from the reifyNat reflection :

 {-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleContexts #-} import GHC.TypeLits import Data.Proxy import Unsafe.Coerce newtype MagicNat3 r = MagicNat3 (forall (n :: Nat). KnownNat (n * 3) => Proxy n -> r) trickValue :: Integer -> Integer trickValue = (*3) -- No type-level garantee that the function will be called with (n * 3) -- you have to believe us trick :: forall a n. KnownNat n => Proxy n -> (forall m. KnownNat (m * 3) => Proxy m -> a) -> a trick pf = unsafeCoerce (MagicNat3 f :: MagicNat3 a) (trickValue (natVal p)) Proxy test :: forall m. KnownNat (m * 3) => Proxy m -> Integer test _ = natVal (Proxy :: Proxy (m * 3)) 

So, when you run it:

 λ *Main > :t trick (Proxy :: Proxy 4) test :: Integer trick (Proxy :: Proxy 4) test :: Integer :: Integer λ *Main > trick (Proxy :: Proxy 4) test :: Integer 12 

The trick is based on the fact that in the GHC, dictionaries of the same class (e.g. KnownNat ) are represented by the member himself. In a KnownNat situation this turns out to be an Integer . So we are just unsafeCoerce there. Universal quantification makes sound outside.

Answer 2

So, three months later, I went back and forth along good paths to achieve this, but I finally settled on the very very concise trick that does not require any one-time beginners; it includes using the Dict from the constraints library; you can easily write:

 natDict :: KnownNat n => Proxy n -> Dict (KnownNat n) natDict _ = Dict triple :: KnownNat n => Proxy n -> Dict (KnownNat (n * 3)) triple p = reifyNat (natVal p * 3) $ \p3 -> unsafeCoerce (natDict p3) 

And as soon as you get Dict (KnownNat (n * 3) , you can map it to a template to get an instance (n * 3) in the scope:

 case triple (Proxy :: Proxy n) of Dict -> -- KnownNat (n * 3) is in scope 

You can also set them as general:

 addNats :: (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Dict (KnownNat (n * m)) addNats px py = reifyNat (natVal px + natVal py) $ \pz -> unsafeCoerce (natDict pz) 

Or you can make them statements, and you can use them to "combine" Dicts:

 infixl 6 %+ infixl 7 %* (%+) :: Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n + m)) (%*) :: Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n * m)) 

And you can do things like:

 case d1 %* d2 %+ d3 of Dict -> -- in here, KnownNat (n1 * n2 + n3) is in scope 

I wrapped this in a beautiful library, typelits-witnesses , which I used. Thank you all for your help!

Answer 3

Your question is not very descriptive, so I will try my best to feel the spaces:

Suppose Blah n is Proxy n .

I also suggest that reflectNat is a way to call a universally quantified function (like Nat level) using a natural number at the term level.

I don’t know a better way than to write my own reflectNat providing

 {-# LANGUAGE RankNTypes #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleContexts #-} import GHC.TypeLits import Data.Proxy data Vec a (n :: Nat) where Nil :: Vec a 0 Cons :: a -> Vec an -> Vec a (1 + n) vecToList :: Vec an -> [a] vecToList Nil = [] vecToList (Cons ht) = h : vecToList t repl :: forall n a. KnownNat n => Proxy n -> a -> Vec an repl px = undefined -- this is a bit tricky with Nat from GHC.TypeLits, but possible foo :: forall (n :: Nat). KnownNat (1 + n) => Proxy n -> Vec Bool (1 + n) foo _ = repl (Proxy :: Proxy (1 + n)) True -- Here we have to write our own version of 'reflectNat' providing right 'KnownNat' instances -- so we can call `foo` reflectNat :: Integer -> (forall n. KnownNat (1 + n) => Proxy (n :: Nat) -> a) -> a reflectNat = undefined test :: [Bool] test = reflectNat 5 $ \p -> vecToList (foo p) 

---

Alternatively, using singletons , you can use SomeSing . Then the types will be different

 reflectNat :: Integer -> (forall (n :: Nat). SomeSing (n :: Nat) -> a) -> a 

those. instead of dict KnownNat magic, you have a specific singleton value. So in foo you need to explicitly build SomeSing (1 + n) , given SomeSing n - it's pretty simple.

At runtime, both KnownNat and SomeSing will be passed based on the value of the number, and explicit will be IMHO better in this situation. p)