[Haskell-cafe] ANNOUNCE: type-level-natural-number and friends!
Gregory Crosswhite
gcross at phys.washington.edu
Thu Oct 14 14:25:24 EDT 2010
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
More information about the Haskell-Cafe
mailing list