I think most of the singletons stuff has been moved to the 'singletons' package [0]. Erik [0] http://hackage.haskell.org/package/singletons On Sat, Mar 15, 2014 at 6:26 PM, Henning Thielemann wrote:

Am 15.03.2014 18:13, schrieb adam vogt:

...

http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/syntax-extns.html... is the trick

Great, this works!

Now I run into the next problem: How can I convert a type-level natural number into a data-level number? The Trac-Wiki mentions singletons: https://ghc.haskell.org/trac/ghc/wiki/TypeNats/Basics and the base package of GHC-7.6 exports the Sing class: http://hackage.haskell.org/package/base-4.6.0.1/docs/GHC-TypeLits.html but it seems to have gone in GHC-7.8. :-(

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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@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@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users