8

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.

fho
  • 6,787
  • 26
  • 71
  • 1
    Pretty much any code one might write with `Nat`-s should work equally with statically known and unknown values. Is there something specific you'd like to do, but don't know how to implement? – András Kovács Jun 10 '15 at 12:58
  • You can define `Vec` as `Vec (n :: Maybe Nat) a`, but I wouldn't do such a thing in Haskell. One another option is to [check your invariants](http://stackoverflow.com/a/27070207/3237465). Or you can use [ornaments](http://stackoverflow.com/a/27220545/3237465). – effectfully Jun 10 '15 at 15:39

1 Answers1

11

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.
Carl
  • 26,500
  • 4
  • 65
  • 86
  • Thanks that was informative. To be honest I don't know if I can apply it if the need comes up (see edit above), but the concept seems clear. – fho Jun 11 '15 at 08:27