type-level definitions naming

[Richard Eisenberg]

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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20131022/6c900af3/attachment.html>