Re: type-level definitions naming

On Mon, Oct 21, 2013 at 6:52 PM, Gábor Lehel wrote:

On Mon, Oct 21, 2013 at 3:42 PM, Richard Eisenberg wrote:

...

On Oct 21, 2013, at 6:06 AM, Gábor Lehel wrote:

On Mon, Oct 21, 2013 at 6:04 AM, Richard Eisenberg 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.