Type literals

typenats.hs

-- 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 Yes, it's only for very recent HEAD builds; the GHC type-nats branch was merged recently.