[Haskell-cafe] ANNOUNCE: type-level-natural-number and friends!
Gregory Crosswhite
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
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Henning Thielemann
> === 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.)
Is there also a 'reify' function, that allows to convert an Int or Peano
value locally to a type level number?
reifyInteger :: Integer -> (forall n. Nat n => n -> a) -> a
Gregory Crosswhite
> Gregory Crosswhite schrieb:
>
>> === 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.)
> Is there also a 'reify' function, that allows to convert an Int or Peano
> value locally to a type level number?
>
> reifyInteger :: Integer -> (forall n. Nat n => n -> a) -> a
>
Not presently, but it is easy to implement such a function:
reifyInt :: Int -> (forall n. NaturalNumber n => N n -> a) -> a
reifyInt i f =
case intToUnknownN i of
UnknownN n -> f n
Is this what you were thinking of?
Cheers,
Greg
Henning Thielemann
> On 10/14/10 1:35 AM, Henning Thielemann wrote:
>> Is there also a 'reify' function, that allows to convert an Int or Peano
>> value locally to a type level number?
>>
>> reifyInteger :: Integer -> (forall n. Nat n => n -> a) -> a
>>
>
> Not presently, but it is easy to implement such a function:
>
> reifyInt :: Int -> (forall n. NaturalNumber n => N n -> a) -> a
> reifyInt i f =
> case intToUnknownN i of
> UnknownN n -> f n
>
> Is this what you were thinking of?
I don't find the string "Unknown" in any of the three
type-level-natural* packages.
Gregory Crosswhite
> Gregory Crosswhite schrieb:
>
>> On 10/14/10 1:35 AM, Henning Thielemann wrote:
>>> Is there also a 'reify' function, that allows to convert an Int or Peano
>>> value locally to a type level number?
>>>
>>> reifyInteger :: Integer -> (forall n. Nat n => n -> a) -> a
>>>
>> Not presently, but it is easy to implement such a function:
>>
>> reifyInt :: Int -> (forall n. NaturalNumber n => N n -> a) -> a
>> reifyInt i f =
>> case intToUnknownN i of
>> UnknownN n -> f n
>>
>> Is this what you were thinking of?
> I don't find the string "Unknown" in any of the three
> type-level-natural* packages.
It is in the package natural-number. (I thought that was the one to
which you were referring since that was the section of my message that
you quoted.) natural-number differs from the other packages in that it
provides a value-level representation of natural numbers rather than a
type-level representation.
If you were actually thinking about something along the lines of, say,
reifyInteger :: Integer -> (forall n. Induction n => n -> a) -> a
then the implementation would be
reifyInteger = go n0
where
go :: Induction n => n -> Integer -> (forall n. Induction n
=> n -> a) -> a
go n 0 f = f n
go n i f = go (successorTo n) (i-1) f