Can I have an unknown KnownNat?

Question

I wonder if I can have my cake and eat it too regarding KnownNats. Can I write code that uses Nats that may be both KnownNats and UnknownNats (SomeNats?).

For example if I have a dependently typed vector Vec (n :: Nat) a, can I write code that works both if the size is known at compile and at runtime? Thing is that I don't want to duplicate the whole code for statically and dynamically sized "things". And I don't want to lose static guarantees by storing sizes in the data structure.

Edit

Answer to András Kovács:

My specific usecase is reading images from disk (which are luckily of fixed size) and then extracting patches from that, so basically I have a function extractPatch :: (KnownNat w2, KnownNat h2) => Image w1 h1 a -> Patch w2 h2 a where both Image and Patch are instances of a common Mat (w :: Nat) (h :: Nat) a type.

If I wouldn't know the image size I would have to encode this in "runtime types". Just wondering.

Answer 1

Here's something potentially interesting...

{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables #-}

import GHC.TypeLits
import Data.Proxy

data Bar (n :: Nat) = Bar String deriving Show

bar :: KnownNat n => Bar n -> (String, Integer)
bar b@(Bar s) = (s, natVal b)

Ok, it's very pointless. But it's an example of using KnownNat to get at compile-time information. But thanks to the other functions in GHC.TypeLits, it can be used with run-time information as well.

Just add this on to the above code, and try it out.

main :: IO ()
main = do
    i <- readLn
    let Just someNat = someNatVal i
    case someNat of
       SomeNat (_ :: Proxy n) -> do
           let b :: Bar n
               b = Bar "hello!"
           print $ bar b

Let's break down what happens here.

1. Read an Integer from stdin.
2. Create a SomeNat-typed value from it, failing the pattern-match if the input was negative. For such a simple example, handling that error just gets in the way.
3. Here's the real magic. Pattern-match with a case expression, using ScopedTypeVariables to bind the (statically unknown) Nat-kinded type to the type variable n.
4. Finally, create a Bar value with that particular n as its type variable and then do things with it.