<div dir="ltr">To answer your second question using GADT-style vectors:<div><br></div><div><div>{-# LANGUAGE RankNTypes #-}</div><div>{-# LANGUAGE DataKinds #-}</div><div>{-# LANGUAGE KindSignatures #-}</div><div>{-# LANGUAGE GADTs #-}</div>
<div>{-# LANGUAGE TypeOperators#-}</div><div>{-# LANGUAGE ScopedTypeVariables #-}</div><div>module WithVector where</div><div><br></div><div>import Data.Maybe</div><div>import Data.Proxy</div><div>import GHC.TypeLits</div>
<div>import Unsafe.Coerce</div><div><br></div><div>data Vector :: Nat -> * -> * where</div><div>  Nil  :: Vector 0 a</div><div>  (:>) :: a -> Vector n a -> Vector (n + 1) a</div><div><br></div><div>infixr 5 :></div>
<div><br></div><div>data SNat :: Nat -> * where</div><div>  SZero :: SNat 0</div><div>  SSucc :: SNat n -> SNat (n + 1)</div><div><br></div><div>snat :: forall proxy n . KnownNat n => proxy n ->  SNat n</div><div>
snat = snat' . natVal</div><div>  where</div><div>    snat' :: Integer -> SNat m</div><div>    snat' 0 = unsafeCoerce SZero</div><div>    snat' n = unsafeCoerce (SSucc (snat' (n-1)))</div><div><br></div>
<div>vreplicate :: SNat n -> a -> Vector n a</div><div>vreplicate SZero _     = Nil</div><div>vreplicate (SSucc n) a = a :> vreplicate n a</div><div><br></div><div>asVector :: KnownNat n => proxy n -> [a] -> Vector n a</div>
<div>asVector s as = asVector' as (vreplicate (snat s) undefined)</div><div>  where</div><div>    asVector' :: [a] -> Vector m b -> Vector m a</div><div>    asVector' _      Nil       = Nil</div><div>    asVector' []     (_ :> _ ) = error "static/dynamic mismatch"</div>
<div>    asVector' (x:xs) (_ :> vs) = x :> asVector' xs vs</div><div><br></div><div>withVector :: forall a b . [a] -> (forall n . KnownNat n => Vector n a -> b) -> b</div><div>withVector xs f = case sn of SomeNat s -> f (asVector s xs)</div>
<div>  where</div><div>    sn = fromMaybe (error "static/dynamic mismatch") (someNatVal (toInteger (length xs)))</div><div><br></div><div>vlength :: forall n a . KnownNat n => Vector n a -> Integer</div><div>
vlength _ = natVal (Proxy :: Proxy n)</div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sat, Mar 15, 2014 at 9:48 PM, Henning Thielemann <span dir="ltr"><<a href="mailto:lemming@henning-thielemann.de" target="_blank">lemming@henning-thielemann.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Am 15.03.2014 19:17, schrieb Erik Hesselink:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I think most of the singletons stuff has been moved to the<br>
'singletons' package [0].<br>
</blockquote>
<br>
Yes, that's it. It means that all Nat related functionality in 'singletons' can be implemented using GHC.TypeLits - interesting.<br>
<br>
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:<br>
<br>
withVector ::<br>
   [a] -><br>
   (forall n. (KnownNat n) => Vector n a -> b) -><br>
   b<br>
<br>
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). :-(<br>

<br>
Thus I have two questions: What is the meaning of KnownNat and how can I implement "withVector"?<br>
<br>
______________________________<u></u>_________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.<u></u>org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/glasgow-<u></u>haskell-users</a><br>
</blockquote></div><br></div>