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

[Gregory Crosswhite]

  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