The "obvious" way to write the result would be (stealing some syntax made up by ski on #haskell):
fromInt :: Int -> (exists n. (Nat n) *> n) fromInt = ... meaning, "at compile time we don't know the type of the result of fromInt, because it depends on a runtime value, but we'll tell you it's _some_ type (an existential) with a Nat instance". Now, GHC haskell doesn't support existentials like that (you can make a custom data type that wraps them) but you can invert your thinking a bit and ask yourself _who_ can consume such an existential. The only kinds of functions that can deal with an arbitrary type like that (with a Nat instance) are those that are polymorphic in it. So instead of Int -> (exists n. (Nat n) *> n), we flip the existential and make a continuation and say Int -> (forall n. (Nat n) => n -> r) -> r, meaning we take the Int, and a consumer of an arbitrary type-level natural, and return what the consumer returns on our computed type-level natural. We're forced to return exactly the value that the continuation returns because we know nothing at all about the `r` type variable. Hope this helps! Dan On Fri, Nov 19, 2010 at 9:09 AM, Arnaud Bailly <arnaud.oq...@gmail.com>wrote: > Thanks a lot for the explanation. Summarizing: You can't calculate an > exact type, but you don't care if the type of the continuation is > properly set in order to "hide" the exact type of n? Am I right? > > Arnaud > > On Fri, Nov 19, 2010 at 9:24 AM, Miguel Mitrofanov > <miguelim...@yandex.ru> wrote: > > A continuation. > > > > You can't know, what type your "fromInt n" should be, but you're not > going > > to just leave it anyway, you're gonna do some calculations with it, > > resulting in something of type r. So, your calculation is gonna be of > type > > (forall n. Nat n => n -> r). So, if you imagine for a moment that > "fromInt" > > is somehow implemented, what you're gonna do with it is something like > > > > calculate :: Int -> r > > calculate i = let n = fromInt i in k n > > > > where k is of type (forall n. Nat n => n -> r). Now we capture this > pattern > > in a function: > > > > genericCalculate :: Int -> (forall n. Nat n => n -> r) -> r > > genericCalculate i k = let n = fromInt i in k n > > > > Going back to reality, fromInt can't be implemented, but genericCalculate > > probably can, since it doesn't involve calculating a type. > > > > 19.11.2010 10:25, Arnaud Bailly пишет: > >> > >> Just after hitting the button send, it appeared to me that fromInt was > >> not obvious at all, and probably impossible. > >> Not sure I understand your answer though: What would be the second > >> parameter (forall n . (Nat n) => n -> r) -> r) ? > >> > >> Thanks > >> Arnaud > >> > >> On Fri, Nov 19, 2010 at 1:07 AM, Daniel Peebles<pumpkin...@gmail.com> > >> wrote: > >>> > >>> The best you can do with fromInt is something like Int -> (forall n. > >>> (Nat n) > >>> => n -> r) -> r, since the type isn't known at compile time. > >>> > >>> On Thu, Nov 18, 2010 at 2:52 PM, Arnaud Bailly<arnaud.oq...@gmail.com> > >>> wrote: > >>>> > >>>> Thanks a lot, that works perfectly fine! > >>>> Did not know this one... > >>>> BTW, I would be interested in the fromInt too. > >>>> > >>>> Arnaud > >>>> > >>>> On Thu, Nov 18, 2010 at 8:22 PM, Erik Hesselink<hessel...@gmail.com> > >>>> wrote: > >>>>> > >>>>> On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly<arnaud.oq...@gmail.com> > >>>>> wrote: > >>>>>> > >>>>>> Hello, > >>>>>> I am trying to understand and use the Nat n type defined in the > >>>>>> aforementioned article. Unfortunately, the given code does not > compile > >>>>>> properly: > >>>>> > >>>>> [snip] > >>>>> > >>>>>> instance (Nat n) => Nat (Succ n) where > >>>>>> toInt _ = 1 + toInt (undefined :: n) > >>>>> > >>>>> [snip] > >>>>> > >>>>>> And here is the error: > >>>>>> > >>>>>> Naturals.hs:16:18: > >>>>>> Ambiguous type variable `n' in the constraint: > >>>>>> `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 > >>>>>> Probable fix: add a type signature that fixes these type > >>>>>> variable(s) > >>>>> > >>>>> You need to turn on the ScopedTypeVariables extension (using {-# > >>>>> LANGUAGE ScopedTypeVariables #-} at the top of your file, or > >>>>> -XScopedTypeVariables at the command line). Otherwise, the 'n' in the > >>>>> class declaration and in the function definition are different, and > >>>>> you want them to be the same 'n'. > >>>>> > >>>>> Erik > >>>>> > >>>> _______________________________________________ > >>>> Haskell-Cafe mailing list > >>>> Haskell-Cafe@haskell.org > >>>> http://www.haskell.org/mailman/listinfo/haskell-cafe > >>> > >> _______________________________________________ > >> Haskell-Cafe mailing list > >> Haskell-Cafe@haskell.org > >> http://www.haskell.org/mailman/listinfo/haskell-cafe > > > > _______________________________________________ > > Haskell-Cafe mailing list > > Haskell-Cafe@haskell.org > > http://www.haskell.org/mailman/listinfo/haskell-cafe > > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe