type-level definitions naming

[Gábor Lehel]

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