ANNOUNCE: type-level-natural-number and friends!
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
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
On 10/14/10 1:35 AM, Henning Thielemann wrote:
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
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.
On 10/14/10 11:07 AM, Henning Thielemann wrote:
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
participants (2)
-
Gregory Crosswhite -
Henning Thielemann