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

[Gregory Crosswhite]

  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