# converting data-level natural numbers to type-level

Christiaan Baaij christiaan.baaij at gmail.com
Sun Mar 16 09:21:34 UTC 2014

```To answer your second question using GADT-style vectors:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators#-}
{-# LANGUAGE ScopedTypeVariables #-}
module WithVector where

import Data.Maybe
import Data.Proxy
import GHC.TypeLits
import Unsafe.Coerce

data Vector :: Nat -> * -> * where
Nil  :: Vector 0 a
(:>) :: a -> Vector n a -> Vector (n + 1) a

infixr 5 :>

data SNat :: Nat -> * where
SZero :: SNat 0
SSucc :: SNat n -> SNat (n + 1)

snat :: forall proxy n . KnownNat n => proxy n ->  SNat n
snat = snat' . natVal
where
snat' :: Integer -> SNat m
snat' 0 = unsafeCoerce SZero
snat' n = unsafeCoerce (SSucc (snat' (n-1)))

vreplicate :: SNat n -> a -> Vector n a
vreplicate SZero _     = Nil
vreplicate (SSucc n) a = a :> vreplicate n a

asVector :: KnownNat n => proxy n -> [a] -> Vector n a
asVector s as = asVector' as (vreplicate (snat s) undefined)
where
asVector' :: [a] -> Vector m b -> Vector m a
asVector' _      Nil       = Nil
asVector' []     (_ :> _ ) = error "static/dynamic mismatch"
asVector' (x:xs) (_ :> vs) = x :> asVector' xs vs

withVector :: forall a b . [a] -> (forall n . KnownNat n => Vector n a ->
b) -> b
withVector xs f = case sn of SomeNat s -> f (asVector s xs)
where
sn = fromMaybe (error "static/dynamic mismatch") (someNatVal (toInteger
(length xs)))

vlength :: forall n a . KnownNat n => Vector n a -> Integer
vlength _ = natVal (Proxy :: Proxy n)

On Sat, Mar 15, 2014 at 9:48 PM, Henning Thielemann <
lemming at henning-thielemann.de> wrote:

> Am 15.03.2014 19:17, schrieb Erik Hesselink:
>
>  I think most of the singletons stuff has been moved to the
>> 'singletons' package .
>>
>
> Yes, that's it. It means that all Nat related functionality in
> 'singletons' can be implemented using GHC.TypeLits - interesting.
>
> Using the library I succeeded to convert type-level Nats to data-level
> Integer. Now I need the other way round. I want to implement:
>
> withVector ::
>    [a] ->
>    (forall n. (KnownNat n) => Vector n a -> b) ->
>    b
>
> I want to have the (KnownNat n) constraint, since I want to call 'sing'
> within the continuation and this requires (KnownNat n). I guess, in order
> to implement withVector I need toSing, but this one does not give me a
> (KnownNat n). :-(
>
> Thus I have two questions: What is the meaning of KnownNat and how can I
> implement "withVector"?
>
> _______________________________________________