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

[Arnaud Bailly]

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