tagged-list 1.0 → 1.1
raw patch · 4 files changed
+76/−25 lines, 4 filesdep +type-equalitysetup-changed
Dependencies added: type-equality
Files
- Data/List/Tagged.hs +51/−15
- Setup.hs +0/−2
- Setup.lhs +4/−0
- tagged-list.cabal +21/−8
Data/List/Tagged.hs view
@@ -11,6 +11,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE UnicodeSyntax #-} -- @-node:gcross.20100918210837.1285:<< Language extensions >>@@ -24,6 +25,7 @@ ATL(..), -- * Utility functions append,+ castTag, eqLists, extractRightsOrLefts, fromList,@@ -68,10 +70,16 @@ import Data.Binary (Binary,get,put) import Data.Foldable (Foldable,foldMap)+import Data.List ((++))+import qualified Data.List as List+import Data.Maybe (Maybe(Just,Nothing)) import Data.Monoid (Monoid,mappend,mempty) import Data.Traversable (Traversable,traverse)+import Data.Type.Equality ((:=:)(Refl),eqT) import Data.Typeable (Typeable) +import Text.Show (show)+ import TypeLevel.NaturalNumber (N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10,N11,N12,N13,N14,N15 ,Zero@@ -105,12 +113,12 @@ -- @-node:gcross.20100918210837.1288:TaggedList -- @+node:gcross.20100918210837.1289:UntaggedList -- | 'UntaggedList' is a wrapper around TaggedList that lets you hide the length tag; the purpose of this is to allow for situations in which you have a tagged list with an unknown length.-data UntaggedList α = ∀ n. UntaggedList (TaggedList n α) deriving Typeable+data UntaggedList α = ∀ n. NaturalNumber n ⇒ UntaggedList (TaggedList n α) deriving Typeable -- @-node:gcross.20100918210837.1289:UntaggedList -- @-node:gcross.20100918210837.1287:Types -- @+node:gcross.20100918210837.1290:Instances -- @+node:gcross.20100918210837.1291:Binary TaggedList-instance (Induction n, Binary α) ⇒ Binary (TaggedList n α) where+instance (NaturalNumber n, Binary α) ⇒ Binary (TaggedList n α) where get = fmap fromList get put = put . toList -- @nonl@@ -125,7 +133,13 @@ instance (Induction n, Eq α) ⇒ Eq (TaggedList n α) where x == y = runAbort (deduction2M () (\_ _ _ → return True) step (TL x) (TL y)) where- step :: Eq α ⇒ TL α (SuccessorTo n) → TL α (SuccessorTo n) → () → Abort Bool (TL α n,TL α n,())+ step ::+ forall n α.+ Eq α ⇒+ TL α (SuccessorTo n) →+ TL α (SuccessorTo n) →+ () →+ Abort Bool (TL α n,TL α n,()) step (TL (x :. xs)) (TL (y :. ys)) b | x /= y = abort False | otherwise = return (TL xs,TL ys,())@@ -135,7 +149,13 @@ instance Induction n ⇒ Foldable (TaggedList n) where foldMap f l = deduction mempty (const id) (step f) (TL l) where- step :: Monoid m ⇒ (α → m) → TL α (SuccessorTo n) → m → (TL α n,m)+ step ::+ forall α n m.+ Monoid m ⇒+ (α → m) →+ TL α (SuccessorTo n) →+ m →+ (TL α n,m) step f (TL (x :. xs)) a = (TL xs,a `mappend` f x) -- @nonl -- @-node:gcross.20100918210837.1294:Foldable TaggedList@@ -164,6 +184,12 @@ append E = id append (x :. xs) = (x :.) . append xs -- @-node:gcross.20100918210837.1300:append+-- @+node:gcross.20101019112709.1288:castTag+-- | Casts the tag of a list, given a proof that the new tag is equal to the old tag.+castTag :: m :=: n → TaggedList m α → TaggedList n α+castTag Refl = id+-- @nonl+-- @-node:gcross.20101019112709.1288:castTag -- @+node:gcross.20100918210837.1308:eqLists -- | Compares two lists, which may be of different sizes; 'False' is returned if the lists do not have the same size. eqLists :: Eq α ⇒ TaggedList m α → TaggedList n α → Bool@@ -188,13 +214,19 @@ -- @-node:gcross.20100918210837.1303:extractRightsOrLefts -- @+node:gcross.20100928114649.1287:fromList -- | Converts a list to a 'TaggedList', returning _|_ if the length of the list does not match the length tag of the return type.-fromList :: Induction n ⇒ [α] → TaggedList n α-fromList = unwrapTL . snd . induction z i+fromList :: NaturalNumber n ⇒ [α] → TaggedList n α+fromList l = r where- z [] = (undefined,TL E)- z _ = error "List is too long to convert into a tagged list of the given length."- i (x:xs) (TL l) = (xs,TL (x :. l))- i [] _ = error "List is too short to convert into a tagged list of the given length."+ r = case fromListAsUntagged l of+ UntaggedList t →+ case eqT (length t) (length r) of+ Just proof → castTag proof t+ Nothing →+ error $+ "Cannot convert a list of length "+ ++ show (List.length l) +++ " to a tagged list of fixed length "+ ++ show (length r) -- @nonl -- @-node:gcross.20100928114649.1287:fromList -- @+node:gcross.20100918210837.1306:fromListAsUntagged@@ -216,11 +248,15 @@ -- | Appends two lists together, and returns both the result and a splitter function that allows you to take another list of the same size as the result (though possible of a different type) and split it back into two lists of the sizes of the arguments to this function. join :: TaggedList m α → TaggedList n α → (TaggedList (Plus m n) α,TaggedList (Plus m n) β → (TaggedList m β,TaggedList n β)) join E v = (v,\z → (E,z))-join (x :. xs) v =- let (vv,split) = join xs v - in (x :. vv- ,(\(y :. ys) → let (a,b) = split ys in (y :. a,b))- )+join (x :. xs) v = (x :. vv, bumpJoin split)+ where+ (vv,split) = join xs v+ -- Note: The abstraction over split' is to avoid having to use ScopedTypeVariables+ bumpJoin :: (TaggedList k a -> (TaggedList k1 a,+ TaggedList k2 a)) ->+ (TaggedList (SuccessorTo k) a -> (TaggedList (SuccessorTo k1) a,+ TaggedList k2 a))+ bumpJoin split' (y :. ys) = let (a,b) = split' ys in (y :. a,b) -- @-node:gcross.20100918210837.1301:join -- @+node:gcross.20100918210837.1297:length -- | Returns the length of the list as a value-level natural number.
− Setup.hs
@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain
+ Setup.lhs view
@@ -0,0 +1,4 @@+#! /usr/bin/env runhaskell++> import Distribution.Simple+> main = defaultMain
tagged-list.cabal view
@@ -3,29 +3,42 @@ -- @@language Haskell Name: tagged-list-Version: 1.0+Version: 1.1 License: BSD3 License-file: LICENSE Author: Gregory Crosswhite-Maintainer: Gregory Crosswhite <gcross@phys.washington.edu>+Maintainer: Gregory Crosswhite <gcrosswhite@gmail.com> Stability: Provisional Synopsis: Lists tagged with a type-level natural number representing their length. Description: This package contains a datatype, 'TaggedList', that provides a fixed-length list tagged with a phantom type-level natural number that corresponds to the length of the list. It also contains some basic operations on these lists, as well as a typeclass for converting tagged lists to and from tuples.-Cabal-version: >=1.2.3+ .+ New in version 1.1: added function castTag, improved error reporting in fromList,+ and fixed compiler error with GHC 7.0.*+Cabal-version: >= 1.6 Build-type: Simple Category: Data +Source-Repository head+ Type: git+ Location: git://github.com/gcross/tagged-list.git++Source-Repository this+ Type: git+ Location: git://github.com/gcross/tagged-list.git+ Tag: 1.1+ Library- Build-depends: base >= 3 && < 5,+ Build-depends: AbortT-transformers >= 1.0 && < 1.1,+ base >= 3 && < 5,+ binary >= 0.5 && < 0.6,+ natural-number >= 1.0 && < 1.1,+ type-equality >= 0.1 && < 0.2, type-level-natural-number >= 1.0 && < 1.2, type-level-natural-number-induction >= 1.0 && < 1.1,- type-level-natural-number-operations >= 1.0 && < 1.1,- natural-number >= 1.0 && < 1.1,- AbortT-transformers >= 1.0 && < 1.1,- binary >= 0.5 && < 0.6+ type-level-natural-number-operations >= 1.0 && < 1.1 Exposed-modules: Data.List.Tagged -- @-node:gcross.20100917231323.1281:@thin tagged-list.cabal -- @-leo