type-level definitions naming

[Gábor Lehel]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20131023/a115f3f1/attachment-0001.html>