type-level definitions naming

Gábor Lehel illissius at gmail.com
Mon Oct 21 16:52:44 UTC 2013


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


More information about the Libraries mailing list