Changelog for the parameterized-utils package

2.1.5.0 -- 2022 Mar 08

• Add support for GHC 9.2. Drop support for GHC 8.4 (or earlier).
• Add a Data.Parameterized.NatRepr.leqZero :: LeqProof 0 n function. Starting with GHC 9.2, GHC is no longer able to conclude that forall (n :: Nat). 0 <= n due to changes in how the (<=) type family works. As a result, this fact must be asserted as an axiom, which the leqZero function accomplishes.

2.1.4.0 -- 2021 Oct 1

• Added the ifoldLM and fromSomeList, fromListWith, and fromListWithM functions to the List module.
• Fix the description of the laws of the OrdF class.
• Fix a bug in which Data.Parameterized.Vector.{join,joinWith,joinWithM} and Data.Parameterized.NatRepr.plusAssoc could crash at runtime if compiled without optimizations.
• Add a Data.Parameterized.Axiom module providing unsafeAxiom and unsafeHeteroAxiom, which can construct proofs of equality between types that GHC isn't able to prove on its own. These functions are unsafe if used improperly, so the responsibility is on the programmer to ensure that these functions are used appropriately.
• Various Proxy enhancements: adds KnownRepr, EqF, and ShowF instances.
• Adds mkRepr and mkKnownReprs Template Haskell functions.
• Added TraversableFC.WithIndex module which provides the FunctorFCWithIndex, FoldableFCWithIndex, and TraversableFCWithIndex classes, with instances defined for Assignment and List.
• Added indicesUpTo, and indicesOf as well as iterateN and iterateNM for the Vector module.
• Added Data.Parameterized.Fin for finite types which can be used to index into a Vector n or other size-indexed datatypes.

2.1.3.0 -- 2021 Mar 23

• Add support for GHC 9.
• In the Context module:
  • Added sizeToNatRepr function for converting a Context Size.
  • Added unzip to unzip an Assignment of Product(Pair) into a separate Assignment for each element of the Pair (the inverse of the zipWith Pair operation).
  • Added flattenAssignment to convert an Assignment of Assignment into an Assignment of CtxFlatten. Also adds flattenSize to combine the sizes of each context into the size of the corresponding CtxFlatten.
• In the Vector module:
  • Added fromAssignment and toAssignment to allow conversions between Assignment and Vector.
  • Added unsnoc, unfoldr, unfoldrM, unfoldrWithIndex, and unfoldrWithIndexM functions.
• Various haddock documentation updates and corrections.
• Updated the Cabal specification to Cabal-version 2.2.

2.1.2 -- 2021 Jan 25

• Added SomeSym and viewSomeSym for existentially hidden Symbol values which retain the KnownSymbol constraint.
• Added leftIndex and rightIndex for re-casting indexes of the individual parts of an Assignment into the concatenated Assignment.
• Additional tests and updated documentation.

2.1.1 -- 2020 Jul 30

• Added drop and appendEmbeddingLeft functions to the Context module.
• Fixes/updates to haddock documentation (fixing Issue #74).
• Allow tasty v1.3 for testing (thanks to felixonmars)

2.1.0 -- 2020 May 08

• Added plusAssoc to the NatRepr module to produce + associativity evidence.
• Changed the HashTable module to use the Basic instead of the Cuckoo implementation strategy.
• Added explicit kind parameters to various definitions to support GHC 8.10's adoption of proposal 103. This is a modification to the type signatures which may impact backward-compatibility and require updates, especially for any uses of TypeApplications.
• No longer verifying support for GHC 8.2 or earlier.
• Updated the minimum cabal version to 1.10 and specify the default-language as Haskell2010.

2.0.2 -- 2020 Feb 10

• Add the dropPrefix operation to Context which splits an Assignment.
• Add intersectWithKeyMaybe and mergeWithKey to Map.
• Add mapAt, mapAtM, and replace to Vector.
• Add dependency on base-orphans to handle the TestEquality instance for Compose; needed for GHC 8.10.
• Bump upper limit of lens dependency to allow 4.19.

2.0.1 -- 2019 Nov 06

• Documentation updates
• Dependency constraint updates: constraints, lens, th-abstraction, hashable, hashtables, and vector.
• Now supports building under GHC 8.8.1.
• Added monadic folds and more traversals:
  • lazy folds: foldlMF, foldrMF, foldlMFC, foldrMFC
  • strict folds: foldlMF', foldrMF', foldlMFC', foldrMFC'
  • forF, forF_
  • forFC, forFC_
  • lengthF
• Added monadic folds, ascending or descending list conversions to Parameterized.Map:
  • Added monadic folds: foldlMWithKey, foldrMWithKey
  • Added ascending or descending list conversions: toAscList (equivalent to existing toList) and toDescList.
  • Added findWithDefault to lookup a key or return a default value.
  • Added traverseMaybeWithKey.
  • Fixes traverse to do an in-order rather than a pre-order traversal.
• Added the Data.Parameterized.All module for universal quantification/parametricity over a type variable.
• Additions to Data.Parameterized.Context:
  • Added IndexView type and viewIndex functions.
  • Added addDiff function to explicitly describe the (flipped) binary operator for the Diff instance of the Category class from Control.Category.
  • Added traverseWithIndex_
• Added Data.Parameterized.DataKind providing the PairRepr type with associated fst and snd functions.
• Added TypeAp to Data.Parameterized.Classes
• Added runSTNonceGenerator to Data.Parameterized.Nonce for a global ST generator.
• Added a Hashable instance for list Index l x types.
• Changes in GADT TH code generator:
  • Added structuralHashWithSalt to
  • Fixed off by one bug in output
  • Fixed generation and constructor generation to use constructor type arguments, not type parameters.
• The Some type is now an instance of FunctorF, FoldableF, and TraversableF.
• Adjusted structuralShowsPrec precedence to match GHC derived Show instances.
• The Data.Parameterized.Nonce.Unsafe module is now deprecated: clients should switch to Data.Parameterized.Nonce.

2.0 -- 2019 Apr 03

• Drop support for GHC versions prior to GHC 8.2
• Various Haddock and module updates.
• Data.Parameterized.Classes
  • Added function: ordFCompose
  • Added OrdF instance for Compose
• Data.Parameterized.ClassesC
  • Marked as Safe haskell via pragma
  • Added OrdC instance for Some
• Data.Parameterized.Compose
  • Update testEqualityComposeBare to be more kind-polymorphic.
  • Marked as Safe haskell via pragma
• Data.Parameterized.Context
  • Added diffIsAppend function to extract the contextual difference between two Contexts (as a Diff) as an IsAppend (new) data value if the left is a sub-context of the right.
• Data.Parameterized.NatRepr
  • Change runtime representation from Int to Natural
  • Add function intValue to recover an Int from a NatRepr.
  • Add constructor function mkNatRepr to construct a NatRepr from a Natural.
  • Removed awkward backdoor for directly creating NatRepr values; the single needed internal usage is now handled internally.
• Data.Parameterized.Peano
  • Newly added module.
  • Defines a type Peano and PeanoRepr for representing a type-level natural at runtime.
  • The runtime representation of PeanoRepr is Word64
  • Has both safe and unsafe implementations.
• Data.Parameterized.WithRepr
  • Newly added module.
  • This module declares a class IsRepr with a single method withRepr that can be used to derive a 'KnownRepr' constraint from an explicit 'Repr' argument. Clients of this method need only create an empty instance. The default implementation suffices.

1.0.8 -- 2019 Feb 01

• Data.Parameterized.Map
  • Fixed MapF functions filter and filterWithKey
  • Added MapF function: mapWithKey
• Data.Parameterized.NatRepr
  • Un-deprecate withKnownNat
• Data.Parameterized.Context
  • Updated some haddock documentation (esp. CtxEmbedding data structure).
• Data.Parameterized.Nonce
  • Fixed newIONonceGenerator haddock documentation (IO monad, not ST monad).
  • Added countNoncesGenerated for profiling Nonce usage.
• Data.Parameterized.TraversableF
  • Added FunctorF, FoldableF, and TraversableF instances for Compose from Data.Functor.Compose
• Data.Parameterized.ClassesC
  • Newly added module.
  • Declares TestEqualityC and OrdC classes for working with types that have kind (k -> *) -> * for any k.
• Data.Parameterized.Compose
  • Newly added module.
  • Orphan instance and testEqualityComposeBare function for working with Data.Functor.Compose.
• Data.Parameterized.TestEquality
  • Newly added module.
  • Utilities for working with Data.Type.TestEquality.

1.0.7 -- 2018 Nov 17

• Data.Parameterized.Map
  • Added MapF functions:
    • filter
    • filterWithKey

1.0.6 -- 2018 Nov 19

• Add support for GHC 8.6.
• Data.Parameterized.Map
  • Added functions:
    • foldlWithKey and foldlWithKey' (strict)
    • foldrWithKey and foldrWithKey' (strict)
    • mapMaybeWithKey

1.0.5 -- 2018 Sep 04

• Data.Parameterized.Context
  • Add function: take, appendEmbedding, appendDiff
  • Diff is type role nominal in both parameters.

1.0.4 -- 2018 Aug 29

• Data.Parameterized.Context
  • Add traverseAndCollect. Allows traversal of an Assignment in order from left to right, collecting the results of a visitor function monoidically.
• Data.Parameterized.DecidableEq
  • Newly added module. The DecidableEq class represents decideable equality on a type family as a superclass of TestEquality, where the latter cannot provide evidence of non-equality.
• Data.Parameterized.NatRepr
  • Add DecidableEq instance for NatRepr.
  • Add functions:
    • decideLeq
    • isZeroOrGT1
    • lessThanIrreflexive
    • lessThanAsymmetric
    • natRecStrong -- recursor with strong induction
    • natRecBounded -- bounded recursor
    • natFromZero
• Data.Parameterized.Vector
  • Add construction functions: singleton, cons, snoc, generate, and generateM
  • Add functions: splitWithA (applicative splitWith).

1.0.3 -- 2018 Aug 24

• Move lemmaMul from Vector to NatRepr.
• Add stricter role annotations:
  • NatRepr is nominal.
  • Vector is nominal in the first parameter and representational in the second.
• Data.Parameterized.NatRepr
  • Provide a backdoor for directly creating NatRepr values. Use carefully.
• Data.Parameterized.Vector
  • Add Show and Eq instances
  • Add functions: joinWithM, reverse

1.0.2 -- 2018 Aug 23

• Allow function passed to traverseF_, traverseFC_, and forMFC_ to return a value instead of null (()).
• Data.Parameterized.Vector
  • Newly added module. A fixed-size vector of typed elements.
• Data.Parameterized.Utils.Endian
  • Newly added module. Used in Vector.

1.0.1 -- 2018 Aug 13

Baseline for changelog tracking.