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

[Arnaud Bailly]

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
<miguelimo38 at 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<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
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>