[Haskell-cafe] ANNOUNCE: type-level-natural-number and friends!

[Gregory Crosswhite]

  Hey everyone,

I am pleased to announce the release of a family of packages for 
type-level natural numbers.  The emphasis on these packages is 
minimality in order to provide simple core functionality that requires 
as few extensions as possible beyond Haskell-2010.  The (probably 
foolish) hope is that this will encourage people to use these packages 
for their simple type-level natural number needs so that the different 
packages can have interoperable type-level natural numbers.

=== type-level-natural-numbers v1.1 ===

This is an update to type-level-natural-numbers, a Haskell-2010 
compatible package which provides simple type-level natural numbers.  
(The only non-Haskell-98 extension that it requires is EmptyDataDecls.)  
This release adds word aliases for N1..N15 (i.e., One, Two, Three...) as 
well as a Typeable instance for type-level natural numbers.

=== type-level-natural-number-operations v1.0 ===

This package contains the type functions Plus and Minus for performing 
addition and subtraction on natural numbers;  by keeping the 
functionality minimal I avoided the need to use UndecideableInstances, 
so the only extension that is required is TypeFamilies.

=== type-level-natural-number-induction v1.0 ===

This is the most interesting of the three packages.  It provides 
high-level combinators for expressing inductive operations on data 
structures tagged with a natural number, which at the moment I call 
"inductive structures".  The idea is that you express your operation in 
terms of a base case and an inductive case, and then call one of the 
combinators to do the rest for you.  There are combinators for building 
up an inductive structure from a seed value, folding over/tearing down 
an inductive structure to get a result, and transforming one inductive 
structure into another.  These combinators are supplied in both monadic 
and non-monadic versions. The only extension that is required to use 
this package is Rank2Types.

=== natural-number v1.0 ===

This package provides *value*-level natural numbers that are tagged with 
a type-level natural number corresponding to their value by using GADTs, 
as well as some simple operations on them.  I also provide an instance 
for the EqT class in type-equality, which means that you can compare two 
natural numbers with possibly different tags and obtain a proof of 
equality if and only if they are the same type.  The extensions that are 
required to use this package are  Rank2Types and GADTs.  (The package 
itself only uses GADTs, but it pulls in 
type-level-natural-number-induction which uses Rank2Types.)

========================

Feedback is always welcome!

Cheers,
Greg