Skip to content

Instantly share code, notes, and snippets.

@thoughtpolice
Created April 9, 2012 18:48
Show Gist options
  • Save thoughtpolice/2345391 to your computer and use it in GitHub Desktop.
Save thoughtpolice/2345391 to your computer and use it in GitHub Desktop.
Type literals
-- probably broken
-- no polymorphic kind signatures, which may make things cleaner
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators#-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ViewPatterns #-}
import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)
-- Proxies and polymorphic kinds
data Proxy p = Proxy
f :: SingI n => Proxy n -> SingRep n
f (_ :: Proxy n) = fromSing (sing :: Sing n)
test1 :: IO ()
test1 = mapM_ putStrLn [show $ f n, show $ f s]
where n = Proxy :: Proxy 4096
s = Proxy :: Proxy "lol"
-- Vectors
data Vec (n :: Nat) (a :: *) where
Nil :: Vec 0 a
Cons :: a -> (Vec n a) -> Vec (n+1) a
instance Show a => Show (Vec n a) where
show Nil = "Nil"
show (Cons x xs) = "Cons " ++ show x ++ " (" ++ show xs ++ ")"
{--}
vappend :: (m+n) ~ r => Vec n a -> Vec m a -> Vec r a
vappend Nil Nil = unsafeCoerce $ Nil
vappend Nil z@(Cons{}) = unsafeCoerce $ z
vappend z@(Cons{}) Nil = unsafeCoerce $ z
vappend (Cons x xs) y@(Cons{}) = unsafeCoerce $ Cons x (vappend xs y)
--}
-- Pointers
newtype IntBound (n :: Nat) = IntBound { unIntBound :: Sing n }
-- A pointer pointing to 'w' words of memory, each
-- 'b' bits wide
data Ptr (w :: Nat) (b :: Nat) = Ptr
type PtrBounds w b i j = (SingI i, SingI j, SingI w, SingI b, i <= w, j <= (2^b))
new_memory :: (SingI w, SingI b) => IO (Ptr w b)
new_memory = return Ptr
bound :: SingI (n :: Nat) => Integer -> Maybe (IntBound n)
bound i = maybe Nothing (Just . IntBound) $ singThat (>= i)
write_memory :: (PtrBounds w b i j) => Ptr w b -> IntBound i -> IntBound j -> IO ()
write_memory _ a1 a2 = do
-- write ptr
return ()
where i = fromSing $ unIntBound a1
j = fromSing $ unIntBound a2
test2 :: IO ()
test2 = do
m <- new_memory :: IO (Ptr 20 8)
let Just i = bound 5 :: Maybe (IntBound 5)
Just j = bound 10 :: Maybe (IntBound 10)
write_memory m i j
return ()
@cartazio
Copy link

is this only for ghc head and not 7.4?

@thoughtpolice
Copy link
Author

@cartazio Yes, it's only for very recent HEAD builds; the GHC type-nats branch was merged recently.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment