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