Design for dataToTag#

[simonpj]

Matthew and I would like to consult you about the API exposed to users of base for the dataToTag# operator.

Currently we have a primop

dataToTag# :: forall (a :: Type). a -> Int#

and a strangely named alias in GHC.Base

getTag :: forall (a :: Type). a -> Int#
getTag x = dataToTag# x

Of course this is all wrong:

• dataToTag# is way too polymorphic: it can't possibly work for every type
• It is levity-monomorphic, so you can't use it on unlifted data types
• Plus, its implementation is a mess -- there is an ad hoc check that all uses of dataToTag# are to data types; but it's a fragile check,.

So Matthew is fixing that by introducing

type DataToTag :: forall {lev :: Levity}. TYPE (BoxedRep lev) -> Constraint
class DataToTag a where
     dataToTag# :: a -> Int#

That fixes both things at one blow:

• dataToTag# now has a type class constrained type, so it's not over-polymoprhic
• Both the class and its operation are levity-polymorphic.
• The implementation is very nice; no hacks any more.

So far so good: it's a change, but a backward-compatible change.

But we'd also like to kill off the strangely named getTag while we are about it (with a deprecation cycle). And we propose to define

dataToTag :: forall (a :: TYPE LiftedRep). DataToTag a => a -> Int
dataToTag' :: forall (a :: TYPE UnliftedRep). DataToTag a => a -> Int

as wrappers for dataToTag# that return a civilised boxed Int. It would be nice to make these levity-polymorphic too, but you can't write

dataToTag x = I# (dataToTag# x)

because there is a levity-polymorphic binder x.

An alternative would be to put dataToTag into the class like this

class DataToTag a where
     dataToTag# :: a -> Int#
     dataToTag :: a -> Int

and now dataToTag can be levity-monomorphic. But the implementation is significantly more fiddly, because we have to build that dictionary on the fly.

The naming of the unlifted version is up for grabs. I suggested dataToTag' by analogy with foldl'

[treeowl]

I don't have any thoughts on your question. However, I do have thoughts about the class, because of some work I was doing recently. In particular, it would be nice to have one or two associated types, and probably another method:

1. RoundTrips, which when 'True guarantees that tagToEnum# (dataToTag# x) = x. This holds for enumeration-like types (which may be GADTs and thus not Enum).
2. NumCons :: Nat, the number of constructors.
3. numCons :: Int, the number of constructors.

[tomjaguarpaw]

it's a change, but a backward-compatible change

Is it backwards-compatible? That means that everywhere a user can successfully compile dataToTag# today they can compile dataToTag# after the change. How about

myDataToTag :: forall (a :: Type). a -> Int#
myDataToTag = dataToTag#

That compiles today. Will it compile after this change? I doubt it. But have I missed something here?

[simonpj]

That compiles today. Will it compile after this change?

Ah, you are right. Of course: myDataToTag can't be that polymorphic: indeed that's the point!

So, fair cop: it's not backward compatible if you write over-polymorphic functions involving dataToTag.

[treeowl]

What about newtype wrappers of various sorts? Will dataToTag# still be able to peer through those?

[simonpj]

What about newtype wrappers of various sorts? Will dataToTag# still be able to peer through those?

Can you give concrete examples of what you mean? DItto for your earlier suggestions, not all of which I could parse. Thanks!

[treeowl]

@simonpj dataToTag# and tagToEnum# are both lightweight "generic" functions, but they're missing some metadata. If we have a TagToEnum class, my round trip thing is irrelevant, so ignore that. But someone who has something TagToEnum and DataToTag is relatively likely to want to know how many constructors the type has. That will let them know things like how many bits are required to serialize the type.

[Bodigrim]

And we propose to define

dataToTag :: forall (a :: TYPE LiftedRep). DataToTag a => a -> Int
dataToTag' :: forall (a :: TYPE UnliftedRep). DataToTag a => a -> Int

as wrappers for dataToTag# that return a civilised boxed Int.

dataToTag# is usually used in low-level, performance-critical manipulations, so I would not say that there is users' demand for "civilised boxed Int", if it simplifies.

[treeowl]

The newtype question: today we can apply dataToTag# to All to determine whether it's true or false. Will that remain the case? I don't think it necessarily needs to, but it would be good to make an intentional decision.

A symmetry question: I don't see a TagToEnum constraint counterpart proposed above. That seems very sad; I would surely want both. Perhaps the answer is performance? tagToEnum# is not operationally polymorphic today, as I understand it. Would it be possible to make it so, and yet be sure to specialize it even with -O0?

[treeowl]

I just discovered that tagToEnum# doesn't work for GADTs. That makes it much less useful than I imagined it to be. Oh well.

[simonpj]

Can I ask: does the CLC see dataToTag# as part of the API for base that users can rely on (and hence which the CLC creates) or as part of GHC internals, purely an internal implementation matter?

If the former, we are totally open for the CLC's guidance. Eg. no dataToTag and dataToTag' is fine with me.

[simonpj]

The newtype question: today we can apply dataToTag# to All to determine whether it's true or false

I see. To spell it out, given

newtype All = MkAll Bool

is dataToTag# (x :: All) well typed? And if so what answer does it give?

Today I think the answer is "yes it is well typed", and would return the tag on the enclosed Bool. I don't know if that's what you want, and would welcome the CLC's guidance. It's a good question.

We can implement either behaviour I think; but rejecting the above is certainly easier. Accepting it would lead to more design questions like "what if the data constructor is not in scope".

My instinct to make a conservative choice now (reject), and loosen up later if we find compelling applications.

[simonpj]

A symmetry question: I don't see a TagToEnum constraint counterpart proposed above

There will certainly be a TagToEnum follow up. But I thought it'd be simpler to do a trial run on a more focused topic.

[simonpj]

But someone who has something TagToEnum and DataToTag is relatively likely to want to know how many constructors the type has. That will let them know things like how many bits are required to serialize the type.

Hmm. I'm not convinced. Can you show some compelling examples? I suspect you'll quickly need the Data class anyway if you want to do anything polymorphic. Currently dataToTag# is essentially always used monomorphically.

[Bodigrim]

Can I ask: does the CLC see dataToTag# as part of the API for base that users can rely on (and hence which the CLC creates) or as part of GHC internals, purely an internal implementation matter?

It's kinda borderline, but I'm inclined to say that it's in scope for CLC because of a new type class.

[Bodigrim]

@simonpj could you please elaborate why do you need a type class? Could we just have dataToTag# :: forall {lev :: Levity}. TYPE (BoxedRep lev) . a -> Int# as a primop?