converting data-level natural numbers to type-level

[Christiaan Baaij]

To answer your second question using GADT-style vectors:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# 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 [0].
>>
>
> 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"?
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140316/b55b63c7/attachment-0001.html>