Re: converting data-level natural numbers to type-level

16 Mar 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@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

Re: converting data-level natural numbers to type-level

Christiaan Baaij