parameterized-data (empty) → 0.1
raw patch · 6 files changed
+555/−0 lines, 6 filesdep +basedep +ghcdep +template-haskellsetup-changed
Dependencies added: base, ghc, template-haskell, type-level
Files
- LICENSE +26/−0
- README +32/−0
- Setup.hs +7/−0
- parameterized-data.cabal +34/−0
- src/Data/Param.hs +18/−0
- src/Data/Param/FSVec.hs +438/−0
+ LICENSE view
@@ -0,0 +1,26 @@+Copyright (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch and+ SAM Group at the School of Information and Communication Technology,+ (Royal Institute of Technology, Stockholm, Sweden)+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 The ForSyDe Team nor the+ names of its 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 ``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 HOLDERS TEAM 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 view
@@ -0,0 +1,32 @@+parameterized-data : Parameterized data library implementing lightweight +dependent types++DESCRIPTION++ This library provides an implementation of parameterized types using+ type-level computations to implement the type parameters and emulate+ dependent types.++ Right now only fixed-sized vectors are provided.+++DEPENDENCIES+ + parameterized-data depends on GHC (due to the use of Template Haskell)+ and the type-level library++INSTALLATION++to install globally, for the whole system (requires admin permissions)++$ ./Setup.hs configure+$ ./Setup.hs build+$ ./Setup.hs haddock # generate documentation, optional+$ ./Setup.hs install++to install locally and just for your own user++$ ./Setup.hs configure --prefix=The/selected/local/directory+$ ./Setup.hs build+$ ./Setup.hs haddock # generate documentation, optional+$ ./Setup.hs install --user
+ Setup.hs view
@@ -0,0 +1,7 @@+#! /usr/bin/env runhaskell+module Main (main) where++import Distribution.Simple++main :: IO ()+main = defaultMain
+ parameterized-data.cabal view
@@ -0,0 +1,34 @@+name: parameterized-data+version: 0.1+cabal-version: >= 1.2+build-type: Simple+license: BSD3+license-file: LICENSE+copyright: + Copyright (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch+ and KTH's SAM group+author: Alfonso Acosta+maintainer: alfonso.acosta@gmail.com+homepage: http://code.haskell.org/parameterized-data+stability: alpha+package-url: http://code.haskell.org/parameterized-data+synopsis: Parameterized data library implementing lightweight dependent + types+description:+ This library provides an implementation of parameterized types using+ type-level computations to implement the type parameters and emulate+ dependent types.++ Right now only fixed-sized vectors are provided.++category: Data+tested-with: GHC==6.8.2+++-- depends on ghc due to the use of Template Haskell+Library+ build-depends: base, ghc > 6.6, type-level, template-haskell > 2.0+ hs-source-dirs: src+ exposed-modules: Data.Param,+ Data.Param.FSVec+ ghc-options: -Wall
+ src/Data/Param.hs view
@@ -0,0 +1,18 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.Param+-- Copyright : (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch+-- and KTH's SAM group +-- License : BSD-style (see the file LICENSE)+-- +-- Maintainer : alfonso.acosta@gmail.com+-- Stability : experimental+-- Portability : non-portable+--+-- This module is a wrapper for all the publicly usable types and functions+-- of the parameterized-data library.+-- +-----------------------------------------------------------------------------+module Data.Param (module Data.Param.FSVec) where++import Data.Param.FSVec
+ src/Data/Param/FSVec.hs view
@@ -0,0 +1,438 @@+{-# LANGUAGE Rank2Types, ScopedTypeVariables, PatternSignatures,+ MultiParamTypeClasses, DeriveDataTypeable, + GeneralizedNewtypeDeriving, TemplateHaskell, CPP #-}+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-name-shadowing #-}+-----------------------------------------------------------------------------+-- |+-- Module : Data.Param.FSVec+-- Copyright : (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch+-- and KTH's SAM group +-- License : BSD-style (see the file LICENSE)+-- +-- Maintainer : alfonso.acosta@gmail.com+-- Stability : experimental+-- Portability : non-portable+--+-- 'FSVec': Fixed sized vectors. Vectors with numerically parameterized size.+--+----------------------------------------------------------------------------+module Data.Param.FSVec + (FSVec, empty, (+>), singleton, vectorCPS, vectorTH,+#if __GLASGOW_HASKELL__ >= 609+ v,+#endif+ unsafeVector, reallyUnsafeVector, readFSVec, length, genericLength,+ lengthT, fromVector, null, (!), replace, head, last,+ init, tail, take, drop, select, group, (<+), (++),+ map, zipWith, foldl, foldr, zip, unzip, shiftl, shiftr,+ rotl, rotr, concat, reverse, iterate, generate, copy + ) where++import Data.TypeLevel.Num hiding ((-),(+),(*),(>),(<),(>=),(<=),(==))+import Data.TypeLevel.Num.Aliases.TH (dec2TypeLevel)++import Data.Generics (Data, Typeable)+import qualified Prelude as P+import Prelude hiding (+ null, length, head, tail, last, init, take, drop, + (++), map, foldl, foldr, + zipWith, zip, unzip, + concat, reverse, iterate)+import qualified Data.Foldable as DF (Foldable, foldr)+import qualified Data.Traversable as DT (Traversable(traverse)) +import Language.Haskell.TH+import Language.Haskell.TH.Syntax (Lift(..))+#if __GLASGOW_HASKELL__ >= 609+import Language.Haskell.TH.Quote+#endif+++-- | Fixed-Sized Vector data type, indexed with type-level naturals, the +-- first index for all vectors is 0+newtype Nat s => FSVec s a = FSVec {unFSVec :: [a]}+ deriving (Eq, Typeable, Data)++instance Show a => Show (FSVec s a) where+ showsPrec _ = showV.unFSVec+ where showV [] = showString "<>"+ showV (x:xs) = showChar '<' . shows x . showl xs+ where showl [] = showChar '>'+ showl (x:xs) = showChar ',' . shows x .+ showl xs++-------------------------+-- Constructing functions+-------------------------++empty :: FSVec D0 a+empty = FSVec []++-- | Cons operator, note it's not a constructor+(+>) :: (Nat s, Pos s', Succ s s') => a -> FSVec s a -> FSVec s' a+x +> (FSVec xs) = FSVec (x:xs)++infixr 5 +>+++-- | A FSVec with a single element+singleton :: a -> FSVec D1 a+singleton x = x +> empty+++-- | Build a vector from a list (CPS style)+vectorCPS :: [a] -> (forall s . Nat s => FSVec s a -> w) -> w+vectorCPS xs = unsafeVectorCPS (P.length xs) xs++-- | Build a vector from a list (using Template Haskell)+vectorTH :: Lift a => [a] -> ExpQ+vectorTH xs = (vectorCPS xs) lift++#if __GLASGOW_HASKELL__ >= 609+-- | Vector quasiquoter+v :: QuasiQuoter+v = QuasiQuoter parseFSVecExp parseFSVecPat++-- Build a vector using quasiquotation+-- Not possible in the general case! It is feasible, though, when only +-- allowing monomorphic vectors. For example, in the case of Ints:+-- parseFSVecExp :: String -> ExpQ+-- parseFSVecExp str = (readFSVec str) (lift :: Nat s => FSVec s Int -> ExpQ)+parseFSVecExp :: String -> ExpQ+parseFSVecExp str = undefined -- (readFSVec str) lift ++-- Pattern match a vector using quasiquotation+parseFSVecPat :: String -> PatQ+parseFSVecPat = error "Data.Param.FSVec: quasiquoting paterns not supported"++-- __GLASGOW_HASKELL__+#endif ++-- | Build a vector from a list (unsafe version: The static/dynamic size of +-- the list is checked to match at runtime)+unsafeVector :: Nat s => s -> [a] -> FSVec s a+unsafeVector l xs+ | toNum l /= P.length xs = + error "unsafeVector: dynamic/static length mismatch"+ | otherwise = FSVec xs++-- | Build a vector from a list. +-- +-- Unlike unsafeVector, reallyunsafeVector doesn't have access to the +-- static size of the list and thus cannot not check it against its+-- dynamic size (which saves traversing the list at runtime to obtain +-- the dynamic length).+--+-- Therefore, reallyUnsafeVector (the name is that long on purspose)+-- can be used to gain some performance but may break the consistency+-- of the size parameter if not handled with care (i.e. the size+-- parameter can nolonger be checked statically and the fullfilment of+-- function constraints is left to the programmers judgement).+-- +-- Do not use reallyUnsafeVector unless you know what you're doing!+reallyUnsafeVector :: [a] -> FSVec s a+reallyUnsafeVector = FSVec++-- | Read a vector. As it happens with vectorCPS, this is the best we can +-- achieve+readFSVec :: Read a => String -> (forall s . Nat s => FSVec s a -> w) -> w+readFSVec str = unsafeVectorCPS l xs+ where + (xs, l) = readFSVecList str+ -- modified version of Prelude.read which accepts < > instead+ -- of [ ] to read lists and also provides the list length+ readFSVecList :: (Read a) => String -> ([a], Int)+ readFSVecList s = case [(x,n) | (x,n,t) <- readList' s, ("","") <- lex t] of+ [x] -> x+ [] -> error "FSVec.readFSVec: no parse"+ _ -> error "FSVec.readFSVec: ambiguous parse"+ where+ readList' :: Read a => String -> [([a], Int, String)]+ readList' = readParen' False (\r -> [pr | ("<",s) <- lex r,+ pr <- readl s])+ readl s = [([],0,t) | (">",t) <- lex s] P.+++ [(x:xs,1+n,u) | (x,t) <- reads s,+ (xs,n,u) <- readl' t]+ readl' s = [([],0,t) | (">",t) <- lex s] P.+++ [(x:xs,1+n,v) | (",",t) <- lex s,+ (x,u) <- reads t,+ (xs,n,v) <- readl' u]+ readParen' b g = if b then mandatory else optional+ where optional r = g r P.++ mandatory r+ mandatory r = [(x,n,u) | ("(",s) <- lex r,+ (x,n,t) <- optional s,+ (")",u) <- lex t ]+----------------------+-- Observing functions+----------------------++-- | value-level length of a vector +length :: forall s a . Nat s => FSVec s a -> Int+length _ = toInt (undefined :: s)++-- | generic value-level length of a vector +genericLength :: forall s a n . (Nat s, Num n) => FSVec s a -> n+genericLength _ = toNum (undefined :: s)++-- | type-level version of length+lengthT :: Nat s => FSVec s a -> s+lengthT = undefined++-- | Transform Vector to a list+fromVector :: Nat s => FSVec s a -> [a]+fromVector (FSVec xs) = xs ++-- | Check if a Vector is empty+null :: FSVec D0 a -> Bool+null _ = True+-- Note: This definition checks the length at _runtime_, we don't want it+-- null (FSVec []) = True+-- null _ = False++-- | Access an element of a vector+(!) :: (Pos s, Nat i, i :<: s) => FSVec s a -> i -> a+(FSVec xs) ! i = xs !! (toInt i)++-------------------------+-- Transforming functions+-------------------------++-- | Replace an element of a vector+replace :: (Nat s, Nat i) => FSVec s a -> i -> a -> FSVec s a+-- alternative, more restrictive type +-- replace :: (Pos s, Nat i, n :<: s) => FSVec s a -> i -> a -> FSVec s a+replace (FSVec xs) i y = FSVec $ replace' xs (toInt i) y+ where replace' [] _ _ = []+ replace' (_:xs) 0 y = (y:xs)+ replace' (x:xs) n y = x : (replace' xs (n - 1) y)++-- | Take the first element of a vector+head :: Pos s => FSVec s a -> a+head = P.head . unFSVec ++-- | Take the last element of a vector+last :: Pos s => FSVec s a -> a +last = P.last . unFSVec ++-- | Return all but the first element of a vector+tail :: (Pos s, Succ s' s) => FSVec s a -> FSVec s' a+tail = liftV P.tail + +-- | Return all but the last element of a vector+init :: (Pos s, Succ s' s) => FSVec s a -> FSVec s' a+init = liftV P.init + +-- | Take the first i elements of a vector+take :: (Nat i, Nat s, Min s i s') => i -> FSVec s a -> FSVec s' a+take i = liftV $ P.take (toInt i) ++-- | Drop the first i elements of a vector+drop :: (Nat i, Nat s, Min s i sm, Sub s sm s') => i -> FSVec s a -> FSVec s' a+drop i = liftV $ P.drop (toInt i) +++-- | The function 'select' selects elements in the vector. The first argument+-- gives the initial element, starting from zero, the second argument gives the+-- stepsize between elements and the last argument gives the number of +-- elements.+select :: (Nat f, Nat s, Nat n, f :<: i, {- f + s * n <= i -}+ Mul s n smn, Add f smn fasmn, fasmn :<=: i) => + f -> s -> n -> FSVec i a -> FSVec n a+select f s n = liftV (select' f' s' n')+ where (f', s', n') = (toInt f, toInt s, toInt n)+ select' f s n = ((selectFirst0 s n).(P.drop f)) + -- list version of select assuming 0 is the index for the first element+ selectFirst0 :: Int -> Int -> [a] -> [a]+ selectFirst0 s n l@(x:_) + | n > 0 = x : selectFirst0 s (n - 1) (P.drop s l) + | otherwise = []+ selectFirst0 _ 0 [] = []++-- | break a vector into subvectors of size n.+group :: (Pos n, Nat s, Div s n s') => + n -> FSVec s a -> FSVec s' (FSVec n a)+group n = liftV (group' (toInt n)) + where group' :: Int -> [a] -> [FSVec s a]+ group' n xs = case splitAtM n xs of+ Nothing -> []+ Just (ls, rs) -> FSVec ls : group' n rs+ +-- | add an element at the end of a vector. (Inverse of '(+>)') +(<+) :: (Nat s, Pos s', Succ s s') => FSVec s a -> a -> FSVec s' a+-- This should work, but it doesn't because+-- "Could not deduce (Data.TypeLevel.Num.Ops.Add' s D1 s')+-- from the context (Nat s, Pos s', Succ s s')"+-- xs <+ x = xs Data.Param.FSVec.++ (singleton x)+(<+) (FSVec xs) x = FSVec (xs P.++ [x]) ++-- | Concatenate two vectors+(++) :: (Nat s1, Nat s2, Add s1 s2 s3) => + FSVec s1 a -> FSVec s2 a -> FSVec s3 a+(++) = liftV2 (P.++)++infixl 5 <++infixr 5 ++++-- | Apply a function on all elements of a vector+map :: Nat s => (a -> b) -> FSVec s a -> FSVec s b+map f = liftV (P.map f)++-- | Applies function pairwise on two vectors+zipWith :: Nat s => (a -> b -> c) -> FSVec s a -> FSVec s b -> FSVec s c+zipWith f = liftV2 (P.zipWith f)+ +-- | Folds a function from the right to the left over a vector using an+-- initial value.+foldl :: Nat s => (a -> b -> a) -> a -> FSVec s b -> a +foldl f e = (P.foldl f e) . unFSVec++-- | Folds a function from the left to the right over a vector using an +-- initial value.+foldr :: Nat s => (b -> a -> a) -> a -> FSVec s b -> a+foldr f e = (P.foldr f e) . unFSVec++-- 'filter' takes a predicate function and a vector and creates a new vector +-- with the elements for which the predicate is true. +-- filterV :: (a -> Bool) -> Vector a -> Vector a+-- FIXME: +-- Imposible to define, the result does not have a predictable static size+++-- | zip two vectors into a vector of tuples.+zip :: Nat s => FSVec s a -> FSVec s b -> FSVec s (a, b)+zip = liftV2 P.zip+ +-- | unzip a vector of tuples into two vectors.+unzip :: Nat s => FSVec s (a, b) -> (FSVec s a, FSVec s b)+unzip (FSVec xs) = let (a,b) = P.unzip xs in (FSVec a, FSVec b)++-- | shift a value from the left into a vector. +shiftl :: Pos s => FSVec s a -> a -> FSVec s a +-- This doesn't work+-- shiftl xs x = x +> init xs+shiftl xs x = liftV ((x:) . P.init) xs++-- | shift a value from the left into a vector. +shiftr :: Pos s => FSVec s a -> a -> FSVec s a +-- This doesn't work+-- shiftr xs x = tail xs <+ x+shiftr xs x = liftV (P.tail . (P.++[x])) xs++-- | Rotate a vector to the left. Note that this fuctions does not change the +-- size of a vector.+rotl :: forall s a . Nat s => FSVec s a -> FSVec s a+-- This doesn't work (it's highly inneficient anyway)+-- rotl [] = []+-- rotl vs = lastV vs +> initV vs +rotl = liftV rotl'+ where vl = toInt (undefined :: s)+ rotl' [] = []+ rotl' xs = let (i,[l]) = splitAt (vl - 1) xs + in l : i+ +-- | Rotate a vector to the left. Note that this fuctions does not change the +-- size of a vector.+rotr :: Nat s => FSVec s a -> FSVec s a+-- This doesn't work +-- rotr [] = []+-- rotr vs = tailV vs <: headV vs+rotr = liftV rotr'+ where rotr' [] = []+ rotr' l@(x:_) = P.tail l P.++ [x] + ++-- | flatten a vector of vectors to a single vector+concat :: (Nat s1, Nat s2, Nat s3, Mul s1 s2 s3) =>+ FSVec s1 (FSVec s2 a) -> FSVec s3 a+-- this won't work: +-- concat = foldr (++) empty+concat = liftV (P.foldr ((P.++).unFSVec) [])+ +-- | reverse a vector+reverse :: Nat s => FSVec s a -> FSVec s a+reverse = liftV P.reverse+++-- | generate a vector with a given number of elements starting from an +-- initial element using a supplied function for the generation of elements. +--+-- > FSVec> iterate d5 (+1) 1+--+-- > <1,2,3,4,5> :: Num a => FSVec D5 a+iterate :: Nat s => s -> (a -> a) -> a -> FSVec s a+iterate s f x = let s' = toInt s in FSVec (P.take s' $ P.iterate f x)+++-- | 'generate' behaves in the same way as 'iterate', but starts with the +-- application of the supplied function to the supplied value. +--+-- > Vector> generate d5 (+1) 1+-- +-- > <2,3,4,5,6> :: Num a => FSVec D5 a+generate :: Nat s => s -> (a -> a) -> a -> FSVec s a+generate s f x = let s' = toInt s in FSVec (P.take s' $ P.tail $ P.iterate f x)+++-- | generates a vector with a given number of copies of the same element. +--+-- > Vector> copy d7 5 +-- +-- > <5,5,5,5,5,5,5> :: Vector Integer+copy :: Nat s => s -> a -> FSVec s a+copy s x = iterate s id x++------------+-- Instances+------------++instance Nat s => DF.Foldable (FSVec s) where+ foldr = foldr+ +instance Nat s => Functor (FSVec s) where+ fmap = map++instance Nat s => DT.Traversable (FSVec s) where + traverse f = (fmap FSVec).(DT.traverse f).unFSVec++instance (Lift a, Nat s) => Lift (FSVec s a) where+ lift (FSVec xs) = [| unsafeFSVecCoerce $(undefSigE lengthType) (FSVec xs) |]+ where -- Get the vector length in a type-level decimal+ lengthType :: TypeQ+ lengthType = dec2TypeLevel $ toInt (undefined :: s)++---------------------+-- Internal functions+---------------------++-- the FSVec equivalent of liftM+-- note it is unsafe and shouldn't be exported+liftV :: ([a] -> [b]) -> FSVec s a -> FSVec s' b+liftV f = FSVec . f . unFSVec++-- the FSVec equivalent of liftM+-- note it is unsafe and shouldn't be exported+liftV2 :: ([a] -> [b] -> [c]) -> FSVec s1 a -> FSVec s2 b -> FSVec s3 c+liftV2 f a b = FSVec (f (unFSVec a) (unFSVec b))+ +-- version of splitAt which checks if the list contains enough elements+splitAtM :: Int -> [a] -> Maybe ([a],[a])+splitAtM n xs = splitAtM' n [] xs + where splitAtM' 0 xs ys = Just (xs,ys)+ splitAtM' n xs (y:ys) | n > 0 = do+ (ls,rs) <- splitAtM' (n - 1) xs ys+ return (y:ls,rs)+ splitAtM' _ _ _ = Nothing++-- Arbitraly coerce the length parameter of a vector+unsafeFSVecCoerce :: s' -> FSVec s a -> FSVec s' a+unsafeFSVecCoerce _ (FSVec v) = (FSVec v)++-- Obtain a TH expression of undefined coerced to certain type+undefSigE :: TypeQ -> ExpQ+undefSigE t = sigE [| undefined |] t++-- unsafely (a trusted length is provided) create a vector using CPS style+unsafeVectorCPS :: forall a w . Int -> [a] -> + (forall s . Nat s => FSVec s a -> w) -> w+unsafeVectorCPS l xs f = reifyIntegral l + (\(_ :: lt) -> f ((FSVec xs) :: (FSVec lt a)))+