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 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>
More information about the Glasgow-haskell-users
mailing list