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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
