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

[Miguel Mitrofanov]

  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<pumpkingod at 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.oqube at 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<hesselink at gmail.com>
>>> wrote:
>>>> On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly<arnaud.oqube at 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 at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe