atom feed5 messages in org.haskell.haskell-cafeRe: [Haskell-cafe] ANNOUNCE: type-lev...
FromSent OnAttachments
Gregory CrosswhiteOct 13, 2010 7:01 pm 
Henning ThielemannOct 14, 2010 1:33 am 
Gregory CrosswhiteOct 14, 2010 10:12 am 
Henning ThielemannOct 14, 2010 11:05 am 
Gregory CrosswhiteOct 14, 2010 11:25 am 
Subject:Re: [Haskell-cafe] ANNOUNCE: type-level-natural-number and friends!
From:Gregory Crosswhite (gcr@phys.washington.edu)
Date:Oct 14, 2010 11:25:01 am
List:org.haskell.haskell-cafe

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

_______________________________________________ Haskell-Cafe mailing list Hask@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe