Re: type-level definitions naming

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 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 wrote:

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.

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries