diff --git a/Data/List/Tagged.hs b/Data/List/Tagged.hs --- a/Data/List/Tagged.hs +++ b/Data/List/Tagged.hs @@ -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. diff --git a/Setup.hs b/Setup.hs deleted file mode 100644 --- a/Setup.hs +++ /dev/null @@ -1,2 +0,0 @@ -import Distribution.Simple -main = defaultMain diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,4 @@ +#! /usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain diff --git a/tagged-list.cabal b/tagged-list.cabal --- a/tagged-list.cabal +++ b/tagged-list.cabal @@ -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 +Maintainer: Gregory Crosswhite 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