Re: [Haskell-cafe] About "Fun with type functions" example

Yes it helps, although I am no type wizard! Thanks a lot for these insights, it gives me some more ideas. Best regards Arnaud On Fri, Nov 19, 2010 at 5:55 PM, Daniel Peebles wrote:

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 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 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  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 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 wrote: > > On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly > 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