type-level definitions naming

[Edward Kmett]

Here's where i sound wishy washy:

castBy in that style looks pretty unnatural. (a :~: b) -> a -> b is the
functor from the discrete category of Hask to Hask.

I'd hate to lose it.

If you want them both to be the same I'd rather have castBy have the nicer
notation and deal with the weird ordering for gcastBy.

-Edward


On Tue, Oct 22, 2013 at 10:38 PM, Richard Eisenberg <eir at cis.upenn.edu>wrote:

> If it's going to reverse its arguments, should it be
>
> > castBy :: a -> (a :~: b) -> b
> > gcastBy :: ((a ~ b) => r) -> (a :~: b) -> r
>
> ?
> Do we even need castBy?
>
> In any case, the "by" name facilitates better infix usage.
>
> Richard
>
> On Oct 22, 2013, at 7:48 PM, Gábor Lehel <illissius at gmail.com> wrote:
>
> On Mon, Oct 21, 2013 at 6:52 PM, Gábor Lehel <illissius at gmail.com> wrote:
>
>>
>> On Mon, Oct 21, 2013 at 3:42 PM, Richard Eisenberg <eir at cis.upenn.edu>wrote:
>>
>>>
>>> On Oct 21, 2013, at 6:06 AM, Gábor Lehel <illissius at gmail.com> wrote:
>>>
>>> On Mon, Oct 21, 2013 at 6:04 AM, Richard Eisenberg <eir at cis.upenn.edu>wrote:
>>>
>>>> - There is a new function (in Data.Type.Equality) gcastWith :: (a :~:
>>>> b) -> ((a ~ b) => r) -> r. Type inference for this function works well.
>>>>
>>>
>>> In my experience, for partial application it's convenient to have the
>>> arguments the other way around.
>>>
>>> I'd be worried about type inference with partial application and
>>> reversed parameters. The values of a and b can only be gleaned from the
>>> equality witness, so I would think that delaying that parameter would cause
>>> some havoc. Is that not what you've seen?
>>>
>>
>> I haven't used it in super-complicated scenarios. But basically, when I
>> have used it, no. If it's used for a top-level definition, it will have a
>> type signature and the types will be known from there, and if it's part of
>> a larger expression just shuffled around for convenience, the equality
>> witness will presumably be in there somewhere.
>>
>> For example, you could define the three combinators from above as partial
>> applications:
>>
>>
>> inner :: (f a :~: g b) -> (a :~: b)
>> inner = gcastWith Refl
>>
>> outer :: (f a :~: g b) -> (f :~: g)
>> outer = gcastWith Refl
>>
>> apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b)
>> apply = gcastWith (gcastWith Refl)
>>
>> I'm not implying these are better in any way than just e.g. `inner Refl =
>> Refl`, but it's the kind of thing you can write which is much more annoying
>> if the arguments are in the reverse order.
>>
>
> Just want to add that this is analogous to the `maybe`, `either`,
> `uncurry` etc. functions for their respective types, so most of the same
> motivations apply.
>
> --
> Your ship was destroyed in a monadic eruption.
>
>
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20131022/2d51adc3/attachment.html>