typelits-witnesses

Existential witnesses, singletons, and classes for operations on GHC TypeLits

https://github.com/mstksg/typelits-witnesses

Version on this page:0.4.0.1
LTS Haskell 22.36:0.4.1.0
Stackage Nightly 2024-10-05:0.4.1.0
Latest on Hackage:0.4.1.0

See all snapshots typelits-witnesses appears in

MIT licensed by Justin Le
Maintained by [email protected]
This version can be pinned in stack with:typelits-witnesses-0.4.0.1@sha256:864d566dfcfa8a7173ced437ec398e050985cd278535dd40539fc1d3e8df681c,1906

Module documentation for 0.4.0.1

Used by 1 package in nightly-2024-07-16(full list with versions):

typelits-witnesses

typelits-witnesses on Hackage typelits-witnesses on Stackage LTS typelits-witnesses on Stackage Nightly Build Status

This library contains:

  • A small specialized subset of the singletons library as it pertains to Nat and Symbol, for when you need some simple functionality without wanting to invoke the entire singletons library.
  • Operations for manipulating these singletons and KnownNat and KnownSymbol instances, such as addition and multiplication of singletons/KnownNat instances.
  • Operations for the comparison of Nats in a way that works well with GHC.TypeLits’s different comparison systems. This is helpful for bridging together libraries that use different systems; this functionality is not yet provided by singletons.

Changes

Changelog

Version 0.4.0.1

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.4.0.1

November 29, 2023

  • Fix for GHC 8.2+
  • Fix type of (%*)
  • minusSNat fixed
  • Qualified cmpNat

Version 0.4.0.0

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.4.0.0

June 20, 2019

  • Complete overhaul of GHC.TypeLits.Witnesses to more or less match the interface of singletons. This changes the role of the module to be a “lightweight” version of the singletons library as it pertains to Nat and Symbol.
  • Removal of the GHC.TypeLits.List module. We could perform the same overhaul as GHC.TypeLits.Witnesses, but it is complex enough that it would be better to just use singletons instead at that point.
  • Remove all external dependencies, except for base and dependent-sum.
  • Break compatibility with GHC < 8.2

Version 0.3.0.3

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.3.0.3

October 1, 2018

  • Fix build for GHC 8.6 and TypeIsStar changes.
  • Break compatibility with GHC < 8.0

Version 0.3.0.2

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.3.0.2

March 30, 2018

  • Functions taking multiple p m in GHC.TypeLits.Compare now are able to take different “proxy” types (p and q).

Version 0.3.0.1

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.3.0.1

  • Documentation fixes because deprecation warnings were not showing up on haddocks for GHC.TypeLits.List.

Version 0.3.0.0

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.3.0.0

  • Added extra witnesses inside the constructors of (:<=?).
  • Allowed functions to polymorphically expect p n instead of Proxy n whenever possible.
  • Soft deprecation of GHC.TypeLits.Witnesses, in case people want to use the functionality of singletons without the full library.
  • Formal deprecation of GHC.TypeLits.List, with migration information, because it’s just so much more unweidly than using singletons.

Version 0.2.3.0

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.2.3.0

  • Added the GHC.TypeLits.Compare module for refining bounds and proving inequalities on KnownNats and associated utility functions.

Version 0.2.2.0

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.2.2.0

  • Removed redundant KnownNats and KnownSymbols constraints for sameNats and sameSymbols.

Version 0.2.1.0

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.2.1.0

  • Added “eliminators”, a staple of dependently typed programming, for NatList and SymbolList.

Version 0.2.0.0

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.2.0.0

  • Breaking: Changed the name of someNatsVal' to someNatsValPos, to break away from the “just add '” anti-pattern and to make the function name a bit more meaningful.

  • Added reifyNats', a “safe” version of reifyNats. Ideally, reifyNats should be the safe one, but its connection to reifyNat from the reflection package is very strong and worth preserving, I think.

Version 0.1.2.0

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.1.2.0

  • Added mapNatList' and mapSymbolList' companions to mapNatList and mapSymbolList; they use NatList and SymbolList instead of Rank-2 types, so they can work better with function composition with (.) and other things that Rank-2 types would have trouble with.

  • Added sameNats and sameSymbols, modeled after sameNat and sameSymbol. They provide witnesses to GHC that KnownNats passed in are both the same.

Version 0.1.1.0

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.1.1.0

  • Added strict fields to NatList, SomeNats, SymbolList, and SomeSymbols. It really doesn’t make any sense for them to be lazy.

Version 0.1.0.1

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.1.0.1

  • Added README to the cabal package as an extra source file, for viewing on Hackage.

Version 0.1.0.0

https://github.com/mstksg/typelits-witnesses/releases/tag/v0.1.0.0

  • Initial version.