packages feed

sized-vector (empty) → 0.0.1.0

raw patch · 6 files changed

+549/−0 lines, 6 filesdep +basesetup-changed

Dependencies added: base

Files

+ Data/Type/Natural.hs view
@@ -0,0 +1,390 @@+{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs        #-}+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude     #-}+{-# LANGUAGE PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}+-- | Type level peano natural number, some arithmetic functions and their singletons.+module Data.Type.Natural (+                         -- * Natural numbers and its singleton type+                           Nat(..), SNat(..)+                         -- ** Smart constructors+                         , sZ, sS+                         -- ** Arithmetic functions and thir singletons.+                         , min, Min, sMin, max, Max, sMax, (:+:), (%+), (:*:), (%*), (:-:), (%-)+                         -- ** Type-level predicate & judgements+                         , Leq(..), (:<=), (:<<=), LeqInstance, leqRefl, leqSucc+                         , boolToPropLeq, boolToClassLeq, propToClassLeq+                         -- * Type-classes for singletons+                         --   (These will be removed once singletons package available for the latest singletons package)+                         , Sing(..), SingInstance(..), singInstance+                         -- * Conversion functions+                         , natToInt, intToNat, sNatToInt+                         -- * Useful type synonyms and constructors+                         , Zero, One, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten+                         , Eleven, Twelve, Thirteen, Fourteen, Fifteen, Sixteen, Seventeen, Eighteen, Nineteen, Twenty+                         , sZero, sOne, sTwo, sThree, sFour, sFive, sSix, sSeven, sEight, sNine, sTen, sEleven+                         , sTwelve, sThirteen, sFourteen, sFifteen, sSixteen, sSeventeen, sEighteen, sNineteen, sTwenty+                         , N0, N1, N2, N3, N4, N5, N6, N7, N8, N9, N10, N11, N12, N13, N14, N15, N16, N17, N18, N19, N20+                         , sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14+                         , sN15, sN16, sN17, sN18, sN19, sN20+                         ) where+import Prelude (Eq (..), Integral (..), Num (..), Ord ((<)), Show (..), error,+                id, otherwise, ($), Bool(..))++--------------------------------------------------+-- * Natural numbers and its singleton type+--------------------------------------------------++-- | Peano natural numbers. It will be promoted to the type-level natural number.+data Nat = Z | S Nat+           deriving (Show, Eq, Ord)++-- | Singleton type for 'Nat'.+--   When constructing data, use smart constructors such as 'sZ' and 'sS'.+data SNat (n :: Nat) where+  SZ :: SNat Z+  SS :: SNat n -> SNat (S n)++--------------------------------------------------+-- ** Smart constructors.+--------------------------------------------------++-- | The smart constructor for @SZ@.+sZ :: SNat Z+sZ = case singInstance SZ of+       SingInstance -> SZ++-- | The smart constructor for @SS n@.+sS :: SNat n -> SNat (S n)+sS n = case singInstance n of+         SingInstance -> SS n++--------------------------------------------------+-- ** Arithmetic functions.+--------------------------------------------------++-- | Minimum function.+min :: Nat -> Nat -> Nat+min Z     Z     = Z+min Z     (S _) = Z+min (S _) Z     = Z+min (S m) (S n) = S (min m n)++-- | Type-level minimum function.+type family Min (n :: Nat) (m :: Nat) :: Nat+type instance Min Z Z     = Z+type instance Min Z (S n) = Z+type instance Min (S m) Z = Z+type instance Min (S n) (S m) = S (Min n m)++-- | Singleton function for minimum function.+sMin :: SNat n -> SNat m -> SNat (Min n m)+sMin SZ     SZ     = sZ+sMin SZ     (SS _) = sZ+sMin (SS _) SZ     = sZ+sMin (SS m) (SS n) = sS (sMin m n)++-- | Maximum function.+max :: Nat -> Nat -> Nat+max Z     Z     = Z+max Z     (S n) = S n+max (S n) Z     = S n+max (S n) (S m) = S (max n m)++-- | Type-level maximum function.+type family Max (n :: Nat) (m :: Nat) :: Nat+type instance Max Z Z     = Z+type instance Max Z (S n) = S n+type instance Max (S n) Z = S n+type instance Max (S n) (S m) = S (Max n m)++-- | Singleton function for maximum.+sMax :: SNat n -> SNat m -> SNat (Max n m)+sMax SZ     SZ     = SZ+sMax (SS n) SZ     = SS n+sMax SZ     (SS n) = SS n+sMax (SS n) (SS m) = SS (sMax n m)++instance Num Nat where+  n   - Z   = n+  S n - S m = n - m+  Z     + n = n+  (S m) + n = S (m + n)+  Z     * _ = 0+  (S m) * n = m * n + n+  abs = id+  signum Z = Z+  signum _ = S Z+  fromInteger 0             = Z+  fromInteger n | n < 0     = error "negative integer"+                | otherwise = S $ fromInteger (n - 1)++infixl 6 :-:, %-+type family (n :: Nat) :-: (m :: Nat) :: Nat+type instance n     :-: Z     = n+type instance (S n) :-: (S m) = n :-: m++(%-) :: (n :<<= m) ~ True => SNat n -> SNat m -> SNat (n :-: m)+n   %- SZ    = n+SS n %- SS m = n %- m+_    %- _    = error "impossible!"++infix 6 :+:, %+++-- | Type-level addition.+type family (n :: Nat) :+: (m :: Nat) :: Nat+type instance  Z   :+: n = n+type instance  S m :+: n = S (m :+: n)++-- | Addition for singleton numbers.+(%+) :: SNat n -> SNat m -> SNat (n :+: m)+SZ   %+ n = n+SS n %+ m = sS (n %+ m)++infix 7 :*:, %*++-- | Type-level multiplication.+type family   (n :: Nat) :*: (m :: Nat) :: Nat+type instance Z   :*: n = Z+type instance S m :*: n = m :*: n :+: n++-- | Multiplication for singleton numbers.+(%*) :: SNat n -> SNat m -> SNat (n :*: m)+SZ   %* _ = sZ+SS n %* m = n %* m %+ m++--------------------------------------------------+-- ** Type-level predicate & judgements.+--------------------------------------------------+-- | Comparison via type-class.+class (n :: Nat) :<= (m :: Nat)+instance Z :<= n+instance (n :<= m) => S n :<= S m++-- | Comparison function+type family   (n :: Nat) :<<= (m :: Nat) :: Bool+type instance Z   :<<= n   = True+type instance S n :<<= Z   = False+type instance S n :<<= S m = n :<<= m++-- | Comparison witness via GADTs.+data Leq (n :: Nat) (m :: Nat) where+  ZeroLeq     :: SNat m -> Leq Zero m+  SuccLeqSucc :: Leq n m -> Leq (S n) (S m)++data LeqInstance n m where+  LeqInstance :: (n :<= m) => LeqInstance n m++boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m+boolToPropLeq SZ     m      = ZeroLeq m+boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m+boolToPropLeq _      _      = error "impossible happend!"++boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m+boolToClassLeq SZ     _      = LeqInstance+boolToClassLeq (SS n) (SS m) =+  case boolToClassLeq n m of+    LeqInstance -> LeqInstance+boolToClassLeq _ _ = error "impossible!"++propToClassLeq :: Leq n m -> LeqInstance n m+propToClassLeq (ZeroLeq _) = LeqInstance+propToClassLeq (SuccLeqSucc leq) =+  case propToClassLeq leq of+    LeqInstance -> LeqInstance++leqRefl :: SNat n -> LeqInstance n n+leqRefl SZ = LeqInstance+leqRefl (SS n) =+  case leqRefl n of+    LeqInstance -> LeqInstance++leqSucc :: SNat n -> LeqInstance n (S n)+leqSucc SZ = LeqInstance+leqSucc (SS n) =+    case leqSucc n of+      LeqInstance -> LeqInstance+++--------------------------------------------------+-- * Type classes for singletons.+--------------------------------------------------++-- | Singleton type-class.+-- This class will be removed soon after singletons package available for the latest Haskell Paltform.+class Sing n where+  -- | Automatically compute singletons.+  sing :: SNat n++instance Sing Z where+  sing = SZ++instance Sing n => Sing (S n) where+  sing = SS sing++-- | Witness for 'Sing' instance.+--   This type will be removed soon after singletons package available for the latest Haskell Paltform.+data SingInstance a where+  SingInstance :: Sing a => SingInstance a++-- | Get witness for singleton integers.+--   This function will be removed soon after singletons package available for the latest Haskell Paltform.+singInstance :: SNat n -> SingInstance n+singInstance SZ = SingInstance+singInstance (SS n) =+    case singInstance n of+      SingInstance -> SingInstance++--------------------------------------------------+-- * Conversion functions.+--------------------------------------------------++-- | Convert integral numbers into 'Nat'+intToNat :: (Integral a, Ord a) => a -> Nat+intToNat 0 = Z+intToNat n+    | n < 0     = error "negative integer"+    | otherwise = S $ intToNat (n - 1)++-- | Convert 'Nat' into normal integers.+natToInt :: Integral n => Nat -> n+natToInt Z     = 0+natToInt (S n) = natToInt n + 1++-- | Convert 'SNat n' into normal integers.+sNatToInt :: Num n => SNat x -> n+sNatToInt SZ     = 0+sNatToInt (SS n) = sNatToInt n + 1++--------------------------------------------------+-- Useful type synonyms and constructors.+--------------------------------------------------++type Zero      = Z+type One       = S Zero+type Two       = S One+type Three     = S Two+type Four      = S Three+type Five      = S Four+type Six       = S Five+type Seven     = S Six+type Eight     = S Seven+type Nine      = S Eight+type Ten       = S Nine+type Eleven    = S Ten+type Twelve    = S Eleven+type Thirteen  = S Twelve+type Fourteen  = S Thirteen+type Fifteen   = S Fourteen+type Sixteen   = S Fifteen+type Seventeen = S Sixteen+type Eighteen  = S Seventeen+type Nineteen  = S Eighteen+type Twenty    = S Nineteen++type N0  = Z+type N1  = One+type N2  = Two+type N3  = Three+type N4  = Four+type N5  = Five+type N6  = Six+type N7  = Seven+type N8  = Eight+type N9  = Nine+type N10 = Ten+type N11 = Eleven+type N12 = Twelve+type N13 = Thirteen+type N14 = Fourteen+type N15 = Fifteen+type N16 = Sixteen+type N17 = Seventeen+type N18 = Eighteen+type N19 = Nineteen+type N20 = Twenty++sZero :: SNat 'Z+sZero = sZ++sOne :: SNat One+sOne = sS sZero+sTwo :: SNat Two+sTwo = sS sOne+sThree :: SNat Three+sThree = sS sTwo+sFour :: SNat Four+sFour = sS sThree+sFive :: SNat Five+sFive = sS sFour+sSix :: SNat Six+sSix = sS sFive+sSeven :: SNat Seven+sSeven = sS sSix+sEight :: SNat Eight+sEight = sS sSeven+sNine :: SNat Nine+sNine = sS sEight+sTen :: SNat Ten+sTen = sS sNine+sEleven :: SNat Eleven+sEleven = sS sTen+sTwelve :: SNat Twelve+sTwelve = sS sEleven+sThirteen :: SNat Thirteen+sThirteen = sS sTwelve+sFourteen :: SNat Fourteen+sFourteen = sS sThirteen+sFifteen :: SNat Fifteen+sFifteen = sS sFourteen+sSixteen :: SNat Sixteen+sSixteen = sS sFifteen+sSeventeen :: SNat Seventeen+sSeventeen = sS sSixteen+sEighteen :: SNat Eighteen+sEighteen = sS sSeventeen+sNineteen :: SNat Nineteen+sNineteen = sS sEighteen+sTwenty :: SNat Twenty+sTwenty = sS sNineteen++sN0 :: SNat 'Z+sN0  = sZ+sN1 :: SNat One+sN1  = sOne+sN2 :: SNat Two+sN2  = sTwo+sN3 :: SNat Three+sN3  = sThree+sN4 :: SNat Four+sN4  = sFour+sN5 :: SNat Five+sN5  = sFive+sN6 :: SNat Six+sN6  = sSix+sN7 :: SNat Seven+sN7  = sSeven+sN8 :: SNat Eight+sN8  = sEight+sN9 :: SNat Nine+sN9  = sNine+sN10 :: SNat Ten+sN10 = sTen+sN11 :: SNat Eleven+sN11 = sEleven+sN12 :: SNat Twelve+sN12 = sTwelve+sN13 :: SNat Thirteen+sN13 = sThirteen+sN14 :: SNat Fourteen+sN14 = sFourteen+sN15 :: SNat Fifteen+sN15 = sFifteen+sN16 :: SNat Sixteen+sN16 = sSixteen+sN17 :: SNat Seventeen+sN17 = sSeventeen+sN18 :: SNat Eighteen+sN18 = sEighteen+sN19 :: SNat Nineteen+sN19 = sNineteen+sN20 :: SNat Twenty+sN20 = sTwenty
+ Data/Vector/Sized.hs view
@@ -0,0 +1,98 @@+{-# LANGUAGE DataKinds, GADTs, MultiParamTypeClasses, PolyKinds #-}+{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators    #-}+-- | Size-parameterized vector types and functions.+module Data.Vector.Sized where+import Control.Applicative+import Data.Maybe+import Data.Type.Natural+import Prelude             hiding (map, foldl, foldr, head, splitAt, tail, zipWith, take)++data Vector (a :: *) (n :: Nat)  where+  Nil  :: Vector a Z+  (:-) :: a -> Vector a n -> Vector a (S n)++infixr 5 :-++deriving instance Show a => Show (Vector a n)+instance (Eq a) => Eq (Vector a n) where+  Nil == Nil = True+  (x :- xs) == (y :- ys) = x == y && xs == ys+  _ == _ = error "impossible!"++sLength :: Vector a n -> SNat n+sLength Nil       = sZ+sLength (_ :- xs) = sS $ sLength xs++length :: Vector a n -> Int+length = sNatToInt . sLength++append :: Vector a n -> Vector a m -> Vector a (n :+: m)+append (x :- xs) ys = x :- append xs ys+append Nil       ys = ys++foldr :: (a -> b -> b) -> b -> Vector a n -> b+foldr _ b Nil       = b+foldr f a (x :- xs) = f x (foldr f a xs)++foldl :: (a -> b -> a) -> a -> Vector b n -> a+foldl _ a Nil       = a+foldl f a (b :- bs) = foldl f (f a b) bs++singleton :: a -> Vector a (S Z)+singleton = (:- Nil)++zipWithSame :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n+zipWithSame _ Nil Nil = Nil+zipWithSame f (x :- xs) (y :- ys) = f x y :- zipWithSame f xs ys+zipWithSame _ _ _ = error "cannot happen"++zipWith :: (a -> b -> c) -> Vector a n -> Vector b m -> Vector c (Min n m)+zipWith _ Nil Nil             = Nil+zipWith _ Nil (_ :- _)        = Nil+zipWith _ (_ :- _) Nil        = Nil+zipWith f (x :- xs) (y :- ys) = f x y :- zipWith f xs ys++toList :: Vector a n -> [a]+toList = foldr (:) []++fromList :: SNat n -> [a] -> Maybe (Vector a n)+fromList SZ     _      = Just Nil+fromList (SS n) (x:xs) = (x :-) <$> fromList n xs+fromList _      _      = Nothing++unsafeFromList :: SNat n -> [a] -> Vector a n+unsafeFromList len = fromMaybe (error "Length too short") . fromList len++fromList' :: Sing n => [a] -> Maybe (Vector a n)+fromList' = fromList sing++unsafeFromList' :: Sing n => [a] -> Vector a n+unsafeFromList' = unsafeFromList sing++all :: (a -> Bool) -> Vector a n -> Bool+all p = foldr ((&&) . p) False++splitAt :: (n :<<= m) ~ True => SNat n -> Vector a m -> (Vector a n, Vector a (m :-: n))+splitAt SZ     xs        = (Nil, xs)+splitAt (SS n) (x :- xs) =+  case splitAt n xs of+    (xs', ys') -> (x :- xs', ys')+splitAt _ _ = error "could not happen!"++drop :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a (m :-: n)+drop n = snd . splitAt n++take :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a n+take SZ     _         = Nil+take (SS n) (x :- xs) = x :- take n xs+take _ _ = error "imposible!"++map :: (a -> b) -> Vector a n -> Vector b n+map _ Nil       = Nil+map f (x :- xs) = f x :- map f xs++head :: Vector a (S n) -> a+head (x :- _) = x++tail :: Vector a (S n) -> Vector a n+tail (_ :- xs) = xs
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2013, Hiromi ISHII++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Hiromi ISHII nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,4 @@+Type-level sized vector library+================================++
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ sized-vector.cabal view
@@ -0,0 +1,25 @@+-- Initial sized-vector.cabal generated by cabal init.  For further +-- documentation, see http://haskell.org/cabal/users-guide/++name:                sized-vector+version:             0.0.1.0+synopsis:            Size-parameterized vector types and functions.+description:         Size-parameterized vector types and functions using a data-type promotion.+homepage:            https://github.com/konn/sized-vector+license:             BSD3+license-file:        LICENSE+extra-source-files:  README.md+author:              Hiromi ISHII+maintainer:          konn.jinro_at_gmail.com+copyright:           (C) Hiromi ISHII 2013+category:            Data+build-type:          Simple+cabal-version:       >=1.8+source-repository head+  Type: git+  Location: git://github.com/konn/sized-vector.git++library+  exposed-modules:     Data.Type.Natural, Data.Vector.Sized+  -- other-modules:       +  build-depends:       base >= 2.0 && < 5