summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlexanderThiemann <>2015-07-19 20:41:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2015-07-19 20:41:00 (GMT)
commit5769b6b1ab70b8fba64230adcdf14a62980d6d15 (patch)
tree53a4143dad514c37492178420e00674d446de00d
parent392a26c2e7f6e83e751c97ade950f5c57d48c984 (diff)
version 0.2.0.00.2.0.0
-rw-r--r--hvect.cabal4
-rw-r--r--src/Data/HVect.hs68
-rw-r--r--test/Data/HVectTest.hs20
3 files changed, 84 insertions, 8 deletions
diff --git a/hvect.cabal b/hvect.cabal
index f04a14c..2129d89 100644
--- a/hvect.cabal
+++ b/hvect.cabal
@@ -1,6 +1,6 @@
name: hvect
-version: 0.1.0.0
-synopsis: Simple heterogeneous lists
+version: 0.2.0.0
+synopsis: Simple strict heterogeneous lists
description: Small, concise and simple implementation of heterogeneous lists with useful utility functions
homepage: https://github.com/agrafix/hvect
bug-reports: https://github.com/agrafix/hvect/issues
diff --git a/src/Data/HVect.hs b/src/Data/HVect.hs
index 441a288..252d480 100644
--- a/src/Data/HVect.hs
+++ b/src/Data/HVect.hs
@@ -1,6 +1,6 @@
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-} -- for ReverseLoop type family
-{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
@@ -9,9 +9,12 @@
{-# LANGUAGE FlexibleInstances #-}
module Data.HVect
- ( HVect (..)
- , empty, null, head
+ ( -- * typesafe strict vector
+ HVect (..)
+ , empty, null, head, tail
, singleton
+ , length, HVectLen (..)
+ , (!!), HVectIdx (..)
, HVectElim
, Append, (<++>)
, ReverseLoop, Reverse, reverse
@@ -19,14 +22,18 @@ module Data.HVect
, Rep (..), HasRep (..)
, curryExpl, curry
, packExpl, pack
+ -- * type level numeric utilities
+ , Nat (..), SNat (..), sNatToInt
+ , intToSNat, AnySNat (..)
+ , (:<)
) where
-import Prelude hiding (reverse, uncurry, curry, head, null)
+import Prelude hiding (reverse, uncurry, curry, head, null, (!!), length, tail)
-- | Heterogeneous vector
data HVect (ts :: [*]) where
HNil :: HVect '[]
- (:&:) :: t -> HVect ts -> HVect (t ': ts)
+ (:&:) :: !t -> !(HVect ts) -> HVect (t ': ts)
instance Eq (HVect '[]) where
_ == _ =
@@ -82,8 +89,59 @@ null _ = False
head :: HVect (t ': ts) -> t
head (a :&: as) = a
+tail :: HVect (t ': ts) -> HVect ts
+tail (a :&: as) = as
+
+length :: HVect as -> SNat (HVectLen as)
+length HNil = SZero
+length (a :&: as) = SSucc (length as)
+
+sNatToInt :: SNat n -> Int
+sNatToInt SZero = 0
+sNatToInt (SSucc n) = 1 + (sNatToInt n)
+
+intToSNat :: Int -> AnySNat
+intToSNat 0 = AnySNat SZero
+intToSNat n =
+ case intToSNat (n - 1) of
+ AnySNat n -> AnySNat (SSucc n)
+
+data Nat where
+ Zero :: Nat
+ Succ :: Nat -> Nat
+
+data SNat (n :: Nat) where
+ SZero :: SNat Zero
+ SSucc :: SNat n -> SNat (Succ n)
+
+data AnySNat where
+ AnySNat :: forall n. SNat n -> AnySNat
+
+type family HVectLen (ts :: [*]) :: Nat
+type instance HVectLen '[] = Zero
+type instance HVectLen (t ': ts) = Succ (HVectLen ts)
+
+type family HVectIdx (n :: Nat) (ts :: [*]) :: *
+type instance HVectIdx Zero (a ': as) = a
+type instance HVectIdx (Succ n) (a ': as) = HVectIdx n as
+type instance HVectIdx a '[] = ()
+
+type family (m :: Nat) :< (n :: Nat) :: Bool
+type instance m :< Zero = False
+type instance Zero :< (Succ n) = True
+type instance (Succ m) :< (Succ n) = m :< n
+
+type family (m :: Nat) :- (n :: Nat) :: Nat
+type instance n :- Zero = n
+type instance (Succ m) :- (Succ n) = m :- n
+
+(!!) :: ((n :< HVectLen as) ~ True) => SNat n -> HVect as -> HVectIdx n as
+SZero !! (a :&: as) = a
+(SSucc s) !! (a :&: as) = s !! as
+
infixr 5 :&:
infixr 5 <++>
+infixl 9 !!
(<++>) :: HVect as -> HVect bs -> HVect (Append as bs)
(<++>) HNil bs = bs
diff --git a/test/Data/HVectTest.hs b/test/Data/HVectTest.hs
index 508d6f3..f0e401f 100644
--- a/test/Data/HVectTest.hs
+++ b/test/Data/HVectTest.hs
@@ -35,6 +35,11 @@ test_head =
do assertEqual 1 (HV.head $ 1 :&: empty)
assertEqual 1 (HV.head $ 1 :&: 2 :&: empty)
+test_tail :: IO ()
+test_tail =
+ do assertEqual empty (HV.tail $ 1 :&: empty)
+ assertEqual (2 :&: empty) (HV.tail $ 1 :&: 2 :&: empty)
+
test_null :: IO ()
test_null =
do assertBool (HV.null empty)
@@ -45,12 +50,25 @@ test_concat =
do assertEqual (1 :&: 2 :&: "foo" :&: "bar" :&: empty) ((1 :&: 2 :&: empty) <++> ("foo" :&: "bar" :&: empty))
assertEqual (1 :&: 2 :&: empty) ((1 :&: 2 :&: empty) <++> empty)
+
test_curryUncurry :: IO ()
test_curryUncurry =
do assertEqual "12" (fun (1 :&: 2 :&: empty))
assertEqual "12" (HV.curry fun 1 2)
assertEqual "12" (HV.uncurry (HV.curry fun) (1 :&: 2 :&: empty))
where
- fun :: HVect '[Int, Int] -> String
+ fun :: HVect [Int, Int] -> String
fun (a :&: b :&: HNil) = show a ++ show b
fun _ = "OOPS!"
+
+test_length :: IO ()
+test_length =
+ do assertEqual 0 (sNatToInt $ HV.length empty)
+ assertEqual 2 (sNatToInt $ HV.length ("foo" :&: "bar" :&: empty))
+ assertEqual 5 (sNatToInt $ HV.length ("aaa" :&: False :&: True :&: "foo" :&: "bar" :&: empty))
+
+test_idxAccess :: IO ()
+test_idxAccess =
+ do assertEqual "foo" (SZero HV.!! ("foo" :&: "bar" :&: empty))
+ assertEqual "bar" (SSucc SZero HV.!! ("foo" :&: "bar" :&: empty))
+ assertEqual "bar" (SSucc (SSucc SZero) HV.!! (True :&: "foo" :&: "bar" :&: empty))