From | Sent On | Attachments |
---|---|---|

Gregory Crosswhite | Oct 13, 2010 7:01 pm | |

Henning Thielemann | Oct 14, 2010 1:33 am | |

Gregory Crosswhite | Oct 14, 2010 10:12 am | |

Henning Thielemann | Oct 14, 2010 11:05 am | |

Gregory Crosswhite | Oct 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