Richard Eisenberg | 21 Oct 06:04 2013

type-level definitions naming

I've made the changes that I see fit, regarding http://ghc.haskell.org/trac/ghc/wiki/TypeLevelNamingIssues  As I wanted a little feedback before pushing, the changes are at my fork of the base repo, at https://github.com/goldfirere/packages-base

Here is what I've done:
- The function with type (a :~: b) -> a -> b is now named castWith.

- There is a new function (in Data.Type.Equality) gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r. Type inference for this function works well.

- I've renamed EqualityT and CoercionT to EqualityType and CoercionType. The T's at the ends of the old names made me think of monad transformers. I don't like the new names, though.

- EqualityType's method is now maybeEquality (instead of equalsT). CoercionType's method is now maybeCoercion (instead of coercionT).

- I've added (==) as type-level Boolean equality to Data.Type.Equality. Instead of the fully-general poly-kinded definition, my experience has shown that a recursive definition of Boolean equality over algebraic types is superior to the general poly-kinded one. So, (==) is an open type family, with many closed type family specializations over certain types (including * and (k1 -> k2), as well as promoted versions of the base datatypes).

- An earlier version of TypeLits had Nat1 as a canonical unary natural number type and conversions to and from. I expect this will be a popular addition, so I restored it. I also added instances of Eq, Ord, Data, Typeable, Read, Show, Num, Integral, Real, Enum, and Ix, in case someone wants to use Nat1 at the term level.

Questions for you all:
- Better name ideas for EqualityType/maybeEquality and CoercionType/maybeCoercion? I'm very unsatisfied.

- OK to add (==)? There is a naming tension with the (<=) and (<=?) operators in TypeLits. Following the convention of appending ? for Boolean operators, (==) should be spelled (~?). But, I don't like that terribly much, for aesthetic more than practical reasons. Please disagree with me or suggest a more unified structure. (Maybe the constraint (<=) should really be (<~)... but I think that's *very* confusing, as it looks like an arrow!)

- OK to add Nat1? Comments on the instances?

Thanks,
Richard
_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Gábor Lehel | 21 Oct 12:06 2013
Picon

Re: type-level definitions naming

Unless there's some issues I'm missing, all of the `liftEq` functions could be replaced by just one:

    apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b)

`lower` could be generalized:

    inner :: (f a :~: g b) -> (a :~: b)

and this could be added:

    outer :: (f a :~: g b) -> (f :~: g)


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've renamed EqualityT and CoercionT to EqualityType and CoercionType. The T's at the ends of the old names made me think of monad transformers. I don't like the new names, though.

No radically better ideas, but perhaps marginally: `TypeEq` and `TypeReprEq`? Or `TestEquality` and `TestCoercible`?
 
- EqualityType's method is now maybeEquality (instead of equalsT). CoercionType's method is now maybeCoercion (instead of coercionT).

These seem alright. I suppose they might change to track the class names, if those change.
 
- An earlier version of TypeLits had Nat1 as a canonical unary natural number type and conversions to and from. I expect this will be a popular addition, so I restored it. I also added instances of Eq, Ord, Data, Typeable, Read, Show, Num, Integral, Real, Enum, and Ix, in case someone wants to use Nat1 at the term level.

It seems GHC is on a mission to obsolete my packages :-). First type-eq, now data-nat. But that's good, these things should exist in a central place.

The name `Nat1` seems a bit unfortunate. If we ever get a term-level `Natural` type to complement `Integer`, will that and the current `Nat` be different concepts (in which case with `Nat1`, there would be 3)? If they would be the same, i.e. only 2 different types, I think calling one of them `Nat` and the other `Natural` would be nice. If all 3 would be different things then I don't have better ideas.

There's a few useful auxiliary definitions (`nat`, `foldNat`, `unfoldNat`, `infinity`, `diff`) in my version which might be worth lifting:

http://hackage.haskell.org/package/data-nat-0.1.2/docs/Data-Nat.html

I also have a `Bounded` instance with `maxBound = infinity`, which I added mostly for kicks, and I'm genuinely not sure whether it meets the implicit expectations for a `Bounded` instance. `n < infinity` will be `True` for any `n` that's not `infinity`, and similarly `[n..infinity]` will be an infinite list (which seems reasonable), but any comparison involving two infinities will be bottom.


--
Your ship was destroyed in a monadic eruption.
_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Richard Eisenberg | 21 Oct 15:42 2013

Re: type-level definitions naming


On Oct 21, 2013, at 6:06 AM, Gábor Lehel <illissius <at> gmail.com> wrote:

Unless there's some issues I'm missing, all of the `liftEq` functions could be replaced by just one:

    apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b)

`lower` could be generalized:

    inner :: (f a :~: g b) -> (a :~: b)

and this could be added:

    outer :: (f a :~: g b) -> (f :~: g)


I like these, and prefer them to the existing liftEqN and lower functions. These mirror more accurately what we have in Core (not that that matters much). I should also note that any similar functions are *very* easy for a user to write, so choosing just the right set of combinators is not critical.


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've renamed EqualityT and CoercionT to EqualityType and CoercionType. The T's at the ends of the old names made me think of monad transformers. I don't like the new names, though.

No radically better ideas, but perhaps marginally: `TypeEq` and `TypeReprEq`? Or `TestEquality` and `TestCoercible`?
 
- EqualityType's method is now maybeEquality (instead of equalsT). CoercionType's method is now maybeCoercion (instead of coercionT).

These seem alright. I suppose they might change to track the class names, if those change.

These names are better than mine.

 
- An earlier version of TypeLits had Nat1 as a canonical unary natural number type and conversions to and from. I expect this will be a popular addition, so I restored it. I also added instances of Eq, Ord, Data, Typeable, Read, Show, Num, Integral, Real, Enum, and Ix, in case someone wants to use Nat1 at the term level.

It seems GHC is on a mission to obsolete my packages :-). First type-eq, now data-nat. But that's good, these things should exist in a central place.

I like your implementation of Nat much more than mine and would be happy to take your definitions wholesale, with your permission. Of course, I should have looked for such a thing before rewriting it myself! But, with all the extra functionality, it feels too big to just be shoehorned into TypeLits.

Perhaps a better solution is to remove Nat1 from TypeLits and then ask that the data-nat package add type-level conversions to and from the TypeLits Nat. Of course, that introduces some naming confusing (two things named Nat!), but there's nothing so special about Nat1 that it needs to live in base. I just thought it would be convenient.


The name `Nat1` seems a bit unfortunate. If we ever get a term-level `Natural` type to complement `Integer`, will that and the current `Nat` be different concepts (in which case with `Nat1`, there would be 3)? If they would be the same, i.e. only 2 different types, I think calling one of them `Nat` and the other `Natural` would be nice. If all 3 would be different things then I don't have better ideas.

There's a few useful auxiliary definitions (`nat`, `foldNat`, `unfoldNat`, `infinity`, `diff`) in my version which might be worth lifting:

http://hackage.haskell.org/package/data-nat-0.1.2/docs/Data-Nat.html

I also have a `Bounded` instance with `maxBound = infinity`, which I added mostly for kicks, and I'm genuinely not sure whether it meets the implicit expectations for a `Bounded` instance. `n < infinity` will be `True` for any `n` that's not `infinity`, and similarly `[n..infinity]` will be an infinite list (which seems reasonable), but any comparison involving two infinities will be bottom.


Thanks for taking a look!
Richard


--
Your ship was destroyed in a monadic eruption.

_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Gábor Lehel | 21 Oct 18:52 2013
Picon

Re: type-level definitions naming




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:

Unless there's some issues I'm missing, all of the `liftEq` functions could be replaced by just one:

    apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b)

`lower` could be generalized:

    inner :: (f a :~: g b) -> (a :~: b)

and this could be added:

    outer :: (f a :~: g b) -> (f :~: g)


I like these, and prefer them to the existing liftEqN and lower functions. These mirror more accurately what we have in Core (not that that matters much). I should also note that any similar functions are *very* easy for a user to write, so choosing just the right set of combinators is not critical.


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.

(FWIW, in my package `Refl` is called `Eq` and `gcastWith` is `withEq`.)
 

 
- I've renamed EqualityT and CoercionT to EqualityType and CoercionType. The T's at the ends of the old names made me think of monad transformers. I don't like the new names, though.

No radically better ideas, but perhaps marginally: `TypeEq` and `TypeReprEq`? Or `TestEquality` and `TestCoercible`?
 
- EqualityType's method is now maybeEquality (instead of equalsT). CoercionType's method is now maybeCoercion (instead of coercionT).

These seem alright. I suppose they might change to track the class names, if those change.

These names are better than mine.

 
- An earlier version of TypeLits had Nat1 as a canonical unary natural number type and conversions to and from. I expect this will be a popular addition, so I restored it. I also added instances of Eq, Ord, Data, Typeable, Read, Show, Num, Integral, Real, Enum, and Ix, in case someone wants to use Nat1 at the term level.

It seems GHC is on a mission to obsolete my packages :-). First type-eq, now data-nat. But that's good, these things should exist in a central place.

I like your implementation of Nat much more than mine and would be happy to take your definitions wholesale, with your permission. Of course, I should have looked for such a thing before rewriting it myself! But, with all the extra functionality, it feels too big to just be shoehorned into TypeLits.

Perhaps a better solution is to remove Nat1 from TypeLits and then ask that the data-nat package add type-level conversions to and from the TypeLits Nat. Of course, that introduces some naming confusing (two things named Nat!), but there's nothing so special about Nat1 that it needs to live in base. I just thought it would be convenient.

Actually, I think it would be best if it did live in base. It's the kind of simple one-liner definition (`data Nat = Zero | Succ Nat`) which tends to be much less of a headache to just add to your code directly and carry on than to bring in an additional dependency for. (I don't have any reverse dependencies that I know of.) Most people won't need most of the other definitions most of the time (most people don't program with `Nat` at the term level, for good reason!), and if they do need one it's another one-liner that's easier to write than to depend on. They're mainly in there for completeness's sake. If it's in base, on the other hand, the path of least resistance will be to import it, and we'll gain whatever small benefits might come from everyone using the same type.

(That still leaves the question of naming, though - would be it unreasonable to rename either this or the existing `Nat` to `Natural`?)

(And feel free to take my code, if you want to - it's open source for a reason!)

 


The name `Nat1` seems a bit unfortunate. If we ever get a term-level `Natural` type to complement `Integer`, will that and the current `Nat` be different concepts (in which case with `Nat1`, there would be 3)? If they would be the same, i.e. only 2 different types, I think calling one of them `Nat` and the other `Natural` would be nice. If all 3 would be different things then I don't have better ideas.

There's a few useful auxiliary definitions (`nat`, `foldNat`, `unfoldNat`, `infinity`, `diff`) in my version which might be worth lifting:

http://hackage.haskell.org/package/data-nat-0.1.2/docs/Data-Nat.html

I also have a `Bounded` instance with `maxBound = infinity`, which I added mostly for kicks, and I'm genuinely not sure whether it meets the implicit expectations for a `Bounded` instance. `n < infinity` will be `True` for any `n` that's not `infinity`, and similarly `[n..infinity]` will be an infinite list (which seems reasonable), but any comparison involving two infinities will be bottom.


Thanks for taking a look!
Richard

And you as well!
 


--
Your ship was destroyed in a monadic eruption.




--
Your ship was destroyed in a monadic eruption.
_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Iavor Diatchki | 22 Oct 23:16 2013
Picon

Re: type-level definitions naming

Hi,

Unless we are planning some built-in support for Nat1, I think that it should live somewhere outside GHC.TypeLits.

In general, I'd prefer if GHC.TypeLits was considered part of the implementation, and not necessarily part of the official type level programming API (so that we can experiment and change it, hence the GHC.* name space)

Iavor

On Oct 21, 2013 9:52 AM, "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:

Unless there's some issues I'm missing, all of the `liftEq` functions could be replaced by just one:

    apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b)

`lower` could be generalized:

    inner :: (f a :~: g b) -> (a :~: b)

and this could be added:

    outer :: (f a :~: g b) -> (f :~: g)


I like these, and prefer them to the existing liftEqN and lower functions. These mirror more accurately what we have in Core (not that that matters much). I should also note that any similar functions are *very* easy for a user to write, so choosing just the right set of combinators is not critical.


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.

(FWIW, in my package `Refl` is called `Eq` and `gcastWith` is `withEq`.)
 

 
- I've renamed EqualityT and CoercionT to EqualityType and CoercionType. The T's at the ends of the old names made me think of monad transformers. I don't like the new names, though.

No radically better ideas, but perhaps marginally: `TypeEq` and `TypeReprEq`? Or `TestEquality` and `TestCoercible`?
 
- EqualityType's method is now maybeEquality (instead of equalsT). CoercionType's method is now maybeCoercion (instead of coercionT).

These seem alright. I suppose they might change to track the class names, if those change.

These names are better than mine.

 
- An earlier version of TypeLits had Nat1 as a canonical unary natural number type and conversions to and from. I expect this will be a popular addition, so I restored it. I also added instances of Eq, Ord, Data, Typeable, Read, Show, Num, Integral, Real, Enum, and Ix, in case someone wants to use Nat1 at the term level.

It seems GHC is on a mission to obsolete my packages :-). First type-eq, now data-nat. But that's good, these things should exist in a central place.

I like your implementation of Nat much more than mine and would be happy to take your definitions wholesale, with your permission. Of course, I should have looked for such a thing before rewriting it myself! But, with all the extra functionality, it feels too big to just be shoehorned into TypeLits.

Perhaps a better solution is to remove Nat1 from TypeLits and then ask that the data-nat package add type-level conversions to and from the TypeLits Nat. Of course, that introduces some naming confusing (two things named Nat!), but there's nothing so special about Nat1 that it needs to live in base. I just thought it would be convenient.

Actually, I think it would be best if it did live in base. It's the kind of simple one-liner definition (`data Nat = Zero | Succ Nat`) which tends to be much less of a headache to just add to your code directly and carry on than to bring in an additional dependency for. (I don't have any reverse dependencies that I know of.) Most people won't need most of the other definitions most of the time (most people don't program with `Nat` at the term level, for good reason!), and if they do need one it's another one-liner that's easier to write than to depend on. They're mainly in there for completeness's sake. If it's in base, on the other hand, the path of least resistance will be to import it, and we'll gain whatever small benefits might come from everyone using the same type.

(That still leaves the question of naming, though - would be it unreasonable to rename either this or the existing `Nat` to `Natural`?)

(And feel free to take my code, if you want to - it's open source for a reason!)

 


The name `Nat1` seems a bit unfortunate. If we ever get a term-level `Natural` type to complement `Integer`, will that and the current `Nat` be different concepts (in which case with `Nat1`, there would be 3)? If they would be the same, i.e. only 2 different types, I think calling one of them `Nat` and the other `Natural` would be nice. If all 3 would be different things then I don't have better ideas.

There's a few useful auxiliary definitions (`nat`, `foldNat`, `unfoldNat`, `infinity`, `diff`) in my version which might be worth lifting:

http://hackage.haskell.org/package/data-nat-0.1.2/docs/Data-Nat.html

I also have a `Bounded` instance with `maxBound = infinity`, which I added mostly for kicks, and I'm genuinely not sure whether it meets the implicit expectations for a `Bounded` instance. `n < infinity` will be `True` for any `n` that's not `infinity`, and similarly `[n..infinity]` will be an infinite list (which seems reasonable), but any comparison involving two infinities will be bottom.


Thanks for taking a look!
Richard

And you as well!
 


--
Your ship was destroyed in a monadic eruption.




--
Your ship was destroyed in a monadic eruption.

_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Gábor Lehel | 23 Oct 01:48 2013
Picon

Re: type-level definitions naming

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
Richard Eisenberg | 23 Oct 04:38 2013

Re: type-level definitions naming

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
Edward Kmett | 23 Oct 05:42 2013
Picon

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


_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Gábor Lehel | 23 Oct 20:21 2013
Picon

Re: type-level definitions naming

On Wed, Oct 23, 2013 at 4:38 AM, 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.

FWIW I think (with this ordering) castWith and castBy both read well infix and both not so well prefix :-)

Anyway, this is the ordering I prefer. A name like `cast` or `coerce` would be nicest (and would make the prefix/infix dilemma go away), but those are taken by Typeable and Coercible. Is going back to `subst` (and then `gsubst`) out of the question? What was the problem with that one? I think it's alright.

I happen to use the above orderings in my version (and also have (|>) = castBy), but I'm more strongly attached to it for gcastBy, whatever it ends up named.

The color of these bikesheds isn't the most important thing in the world though, so if you make an arbitrary choice I'm not going to object, it shouldn't hold anything up.
_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Edward Kmett | 23 Oct 01:44 2013
Picon

Re: type-level definitions naming



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 use the alternate order in (\\) for the constraints package and have had no issues with it after "using it in anger" for a couple of years now.

- I've renamed EqualityT and CoercionT to EqualityType and CoercionType. The T's at the ends of the old names made me think of monad transformers. I don't like the new names, though.

No radically better ideas, but perhaps marginally: `TypeEq` and `TypeReprEq`? Or `TestEquality` and `TestCoercible`?

Out of those alternatives I rather prefer TestEquality and TestCoercible over randomly introducing unrelated abbreviations. =/

-Edward
_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries

Gmane