<div dir="ltr"><div><div><div>Unless there's some issues I'm missing, all of the `liftEq` functions could be replaced by just one:<br><br></div>    apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b)<br><br></div>
<div>`lower` could be generalized:<br><br></div><div>    inner :: (f a :~: g b) -> (a :~: b)<br><br></div><div>and this could be added:<br></div><br></div>    outer :: (f a :~: g b) -> (f :~: g)<br><div class="gmail_extra">
<br><br><div class="gmail_quote">On Mon, Oct 21, 2013 at 6:04 AM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div style="word-wrap:break-word"><div>- There is a new function (in Data.Type.Equality) gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r. Type inference for this function works well.</div></div></blockquote><div><br>
</div><div>In my experience, for partial application it's convenient to have the arguments the other way around.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div style="word-wrap:break-word"><div></div><div>- 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.</div>
</div></blockquote><div><br></div><div>No radically better ideas, but perhaps marginally: `TypeEq` and `TypeReprEq`? Or `TestEquality` and `TestCoercible`?<br></div><div>  <br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div style="word-wrap:break-word"><div>- EqualityType's method is now maybeEquality (instead of equalsT). CoercionType's method is now maybeCoercion (instead of coercionT).</div></div></blockquote><div><br></div><div>
These seem alright. I suppose they might change to track the class names, if those change.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div style="word-wrap:break-word"><div>- 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.</div>
</div></blockquote><div><br></div><div>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.<br></div><div><br></div><div>
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.<br>
<br></div><div>There's a few useful auxiliary definitions (`nat`, `foldNat`, `unfoldNat`, `infinity`, `diff`) in my version which might be worth lifting:<br><br><a href="http://hackage.haskell.org/package/data-nat-0.1.2/docs/Data-Nat.html">http://hackage.haskell.org/package/data-nat-0.1.2/docs/Data-Nat.html</a><br>
<br></div><div>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.<br>
</div></div><br clear="all"><br>-- <br>Your ship was destroyed in a monadic eruption.
</div></div>