packages feed

IndexedList (empty) → 0.1.0.0

raw patch · 6 files changed

+237/−0 lines, 6 filesdep +PeanoWitnessesdep +basesetup-changed

Dependencies added: PeanoWitnesses, base

Files

+ Data/List/Indexed.hs view
@@ -0,0 +1,36 @@+{- |+Module      :  Data.List.Indexed+Description :  A library providing length-indexed and element-indexed lists which sit somewhere between homogeneous and fully heterogeneous lists.+Copyright   :  Copyright (c) 2014 Kenneth Foner++Maintainer  :  kenneth.foner@gmail.com+Stability   :  experimental+Portability :  non-portable++This module re-exports the 'ConicList' and 'CountedList' types and functions to work with them.+-}++{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE GADTs      #-}+{-# LANGUAGE PolyKinds  #-}++module Data.List.Indexed+   ( heterogenize , homogenize+   , module Data.List.Indexed.Counted+   , module Data.List.Indexed.Conic+   ) where++import Data.List.Indexed.Counted+import Data.List.Indexed.Conic++-- We can convert between them using cones and co-cones++-- | Turn a 'CountedList' into a 'ConicList' by means of a function from some @a@ to an @(f t)@.+heterogenize :: (a -> f t) -> CountedList n a -> ConicList f (Replicate n t)+heterogenize _ CountedNil = ConicNil+heterogenize f (x ::: xs) = f x :-: heterogenize f xs++-- | Given a function to collapse any @(f t)@ into an @a@, turn a 'ConicList' into a 'CountedList'.+homogenize :: (forall t. f t -> a) -> ConicList f ts -> CountedList (Length ts) a+homogenize _ ConicNil   = CountedNil+homogenize f (x :-: xs) = f x ::: homogenize f xs
+ Data/List/Indexed/Conic.hs view
@@ -0,0 +1,54 @@+{- |+Module      :  Data.List.Indexed.Conic+Description :  A library providing length-indexed and element-indexed lists which sit somewhere between homogeneous and fully heterogeneous lists.+Copyright   :  Copyright (c) 2014 Kenneth Foner++Maintainer  :  kenneth.foner@gmail.com+Stability   :  experimental+Portability :  non-portable++This module implements conic lists, which are lists where every element is of type @(f a)@ for /some/ @a@, but the @a@ +index may vary. This sits between homogeneous and fully heterogeneous lists in terms of expressivity and also the ease+to manipulate.+-}++{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-} ++module Data.List.Indexed.Conic where++import Data.Numeric.Witness.Peano++infixr 5 :-:+data x :-: y+data Nil++-- | Conic lists are lists where each element is an (f a) for some a, but the a may be different for each element. Types of elements are kept track of in the type of the list.+data ConicList f ts where+   (:-:) :: f a -> ConicList f rest -> ConicList f (a :-: rest)+   ConicNil  :: ConicList f Nil++type family Replicate n x where+   Replicate Zero     x = Nil+   Replicate (Succ n) x = x :-: Replicate n x++type family Length ts where+   Length Nil        = Zero+   Length (x :-: xs) = Succ (Length xs)++type family Tack x xs where+   Tack a Nil        = a :-: Nil+   Tack a (x :-: xs) = x :-: Tack a xs++tack :: f t -> ConicList f ts -> ConicList f (Tack t ts)+tack a ConicNil   = a :-: ConicNil+tack a (x :-: xs) = x :-: tack a xs
+ Data/List/Indexed/Counted.hs view
@@ -0,0 +1,90 @@+{- |+Module      :  Data.List.Indexed.Counted+Description :  A library providing length-indexed and element-indexed lists which sit somewhere between homogeneous and fully heterogeneous lists.+Copyright   :  Copyright (c) 2014 Kenneth Foner++Maintainer  :  kenneth.foner@gmail.com+Stability   :  experimental+Portability :  non-portable++This module implements homogeneous counted lists, which are type-indexed by length.+-}++{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-} ++module Data.List.Indexed.Counted where++import Data.Numeric.Witness.Peano++import Control.Applicative+import Data.List hiding ( replicate , zip )+import Prelude   hiding ( replicate , zip )++infixr 5 :::++-- | Counted lists are indexed by length in the type.+data CountedList n a where+   (:::) :: a -> CountedList n a -> CountedList (Succ n) a+   CountedNil :: CountedList Zero a++instance (Show x) => Show (CountedList n x) where+   showsPrec p xs = showParen (p > 10) $+      (showString $ ( intercalate " ::: "+                    $ map show+                    $ unCount xs ) ++ " ::: CountedNil")++-- | The 'count' of a list is the natural number corresponding to its length.+count :: CountedList n a -> Natural n+count CountedNil = Zero+count (x ::: xs) = Succ (count xs)++-- | Convert a counted list to a regular Haskell list.+unCount :: CountedList n a -> [a]+unCount CountedNil       = []+unCount (x ::: xs) = x : unCount xs++-- | Replicate some element a certain number of times.+replicate :: Natural n -> x -> CountedList n x+replicate Zero     _ = CountedNil+replicate (Succ n) x = x ::: replicate n x++-- | Appending two counted lists yields one of length equal to the sum of the lengths of the two initial lists.+append :: CountedList n a -> CountedList m a -> CountedList (m + n) a+append CountedNil       ys = ys+append (x ::: xs) ys = x ::: append xs ys++-- | Take the nth element of a list. We statically prevent taking the nth element of a list of length less than n.+nth :: (n < m) => Natural n -> CountedList m a -> a+nth Zero     (a ::: _)  = a+nth (Succ n) (_ ::: as) = nth n as+nth _ _ = error "nth: the impossible occurred" -- like in minus, GHC can't prove this is unreachable++-- | Pad the length of a list to a given length. If the number specified is less than the length of the list given,+--   it won't pass the type-checker.+padTo :: (m <= n) => Natural n -> x -> CountedList m x -> CountedList ((n - m) + m) x+padTo n x list =+   list `append` replicate (n `minus` count list) x++-- | Zip two equal-length lists together.+zip :: CountedList n a -> CountedList n b -> CountedList n (a,b)+zip (a ::: as) (b ::: bs) = (a,b) ::: zip as bs+zip CountedNil _ = CountedNil+zip _ CountedNil = CountedNil++instance Functor (CountedList n) where+   fmap f CountedNil = CountedNil+   fmap f (a ::: as) = f a ::: fmap f as++instance (ReifyNatural n) => Applicative (CountedList n) where+   pure x    = replicate (reifyNatural :: Natural n) x+   fs <*> xs = uncurry id <$> zip fs xs
+ IndexedList.cabal view
@@ -0,0 +1,25 @@+-- Initial IndexedList.cabal generated by cabal init.  For further +-- documentation, see http://haskell.org/cabal/users-guide/++name:                IndexedList+version:             0.1.0.0+synopsis:            Length-indexed and element-indexed lists which sit somewhere between homogeneous and fully heterogeneous lists.+description:         This library implements /counted lists/ linked to type-level naturals indexing length, compatible with the Peano natural numbers found in "Data.Numeric.Witness.Peano", as well as so-called /conic lists/, which are linked to a type index listing the type indices of partially-heterogeneous values contained within.+license:             BSD3+license-file:        LICENSE+author:              Kenneth Foner+maintainer:          kenneth.foner@gmail.com+copyright:           Copyright (c) 2014 Kenneth Foner+homepage:            https://github.com/kwf/IndexedList+category:            Data+build-type:          Simple+-- extra-source-files:  +cabal-version:       >=1.10++library+  exposed-modules:     Data.List.Indexed, Data.List.Indexed.Conic, Data.List.Indexed.Counted+  -- other-modules:       +  other-extensions:    RankNTypes, GADTs, PolyKinds, ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies, TypeOperators+  build-depends:       base >=4.7 && <4.8, PeanoWitnesses >= 0.1+  -- hs-source-dirs:      +  default-language:    Haskell2010
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2014, Kenneth Foner++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 Kenneth Foner 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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain