I would vote for waiting until kind polymorphism is present, as otherwise we'd need a potentially infinite number of variations on Typeable so the kind of any type can be covered: although Data.Typeable covers up to an arity of 11, it only works where each type variable is of kind *.

But I don't know, maybe that is unnecessary?

Can I ask what Typeable is useful for? It seems like Generic is very similar, and that's already derivable (only with kind *, so it would also benefit from polykinds).

Ah, I hadn't thought through the fact each type variable needs to be of kind * -- that is a significant argument for waiting for polykinds.

My particular interest in Data.Typeable is in the context of storing something in the DOM and then later wanting to know whether it is the same type as something else. So, essentially a kind of safe run-time coercion. I'm currently doing something funky with typeclasses that works, but in principle Data.Typeable is a better approach.

I considered using Generic instead, seeing as if you know the two things are Generic then you can compare the signatures. However, Generic has the limitation that it can't handle function arrows, whereas Typeable has no trouble with that. Generic is also, in some ways, more ambitious than Typeable, since Generic wants to encode the internal structure of a type, whereas Typeable just encodes the "outer" structure. (For instance, for product types or record types, Generic records the type of each constructor or each label, whereas Typeable doesn't care about that).

Excellent points regarding Generics, I was just being lazy and not thinking through the differences really 😄

Just wanted to let folks know that I've been working on this -- that is, having the compiler automatically generate Typeable instances -- and it's going pretty well. The compiler modifications are actually pretty reasonable in the end.

And, it turns out that the lack of polymorphic kinds doesn't make much difference to what the compiler needs to do. The code on the Purescript side could be simplified in the presence of polymorphic kinds, but what the compiler generates wouldn't change radically. (Note that the code on the Purescript side is quite different from what is in Data.Typeable now).

What I'm working on at the moment is rebasing my work-in-progress on the 'fundeps' branch. Aside from being necessary, I think that with fundeps I can parameterize the TypeRep by a type-level representation of the kind of the represented type. The nice thing about that (if I can get it to work) is that the function which applies two TypeRep values (i.e. for List and Int to make List Int) could be given a signature that effectively does kind-checking (of the underlying types) at compile time, even without polymorphic kinds. (It would be trivial with polymorphic kinds, since you'd just parameterize TypeRep by the actual type it represents).

Perhaps very little of that will make sense without seeing my code, but I just wanted to give a quick update on what I'm working on. I hope to post some code for people to look at next week.

@rgrempel I'm interested to see what you've got in the works for derived Typeable instances.

How does your use case of storing data in the DOM compare to something like purescript-foreign, where we define the runtime structure we expect data to have in the form of an IsForeign instance?

I've never actually used Typeable for anything, even in Haskell, so I'm not really sure of its value yet, but I am interested to hear about possible use cases.

Another small point - if we did have compiler-supported deriving, it would be good to have a minimal implementation of a purescript-typeable library in the core library set.

Is this the kind of stuff that could eventually allow us to write user defined type class deriving mechanisms? For example, deriving Functor, Foldable, & Traversable - which is obviously not possible with Generic.

@LiamGoodacre, I'm not sure. It would allow you to "introspect" on the types at run-time in a way that is distinct from Generic (as noted above, Generic is more concerned with the "inside" of the type, whereas Typeable is more concerned with the "outside"). But I don't really have a handle on what a "user defined type class deriving mechanism" would look like.

@paf31, the comparison with Data.Foreign is an interesting one. One way to describe the mission of Foreign is that it facilitates an (alternate) representation of a type using primitive Javascript values (or, if not primitive, at least external to Purescript). I say "alternate" because, of course, the Purescript value itself is ultimately built from Javascript values (tautologically, since that is what Purescript compiles to). But sometimes you want to be able to move back and forth between the representation which Purescript normally gives you and some alternate representation.

Now, there is nothing in Data.Foreign that necessarily encodes the type of the Purescript value in the alternate representation. Of course, your IsForeign instance could write out some value that represents the type in some way. However, it might not. That is, the Purescript type might be just as "erased" in the Foreign representation as it is in Purescript itself.

To put it another way, given some Foreign data, there may well be more than one IsForeign instance that can successfully read it. And, if you want to choose the Purescript type based on the Foreign data, you either need to read some part of the Foreign data and let that tell you what type to use, or just try a bunch of IsForeign instances and use whichever one succeeds.

So, what Typeable does -- that is, provide a value which represents a type at run-time -- is not automatically done by Foreign. And, if you wanted to do it manually as part of a Foreign representation, you'd need to invent some scheme for it.

As for my particular use case, I don't need an alternate representation of the Purescript value -- I'm happy to be handed back the Purescript value exactly as it is. All I need is to be able to know, at run time, whether it is the same type as something else I now have, even though I can't arrange for the compiler to know that (as would be the usual way of doing things).

In fact, I actually have a couple of (for me) even more motivating use cases since then. One is my https://github.com/rgrempel/purescript-exists-eq package, which allows you to test for equality even where you need to forget the type. This, in turn, enables some interesting stuff in purescript-equatable-functions to do with comparing functions that have been partially applied. And that, in turn, is the basis for something I haven't published yet, Data.Lazier, which is like Data.Lazy but even lazier, in that it is possible to know that some values are equal without forcing them.

Philosophically, the paper that has influenced my thinking on Typeable is A Reflection on Types. Now, the exact approach used there needs heavy modification for Purescript, since it relies on polymorphic kinds and GADTs. However, it turns out that something reasonably elegant is achievable in Purescript, especially so now with fundeps.

Anyway, I'll try to post some actual code later this week, or at least as soon as I can. And I completely understand that it will need pretty serious review.

Just a quick update. I've been experimenting with using functional dependencies, tagless final, and a form of "Church encoding" to do some things that one might do with GADTs, if we had them. It's a bit of overkill, but I'm finding it fascinating, so I'm seeing how far I can push it. Basically, I'm trying to "forget" some type parameters, like we can do with Data.Exists, and yet be able to recover them in a form of pattern matching (unlike Data.Exists, where you would end up with a forall on the parameters you forgot).

Anyway, that's why I haven't pushed the code yet -- I'm still experimenting.

If you want a use case, Typeable is one answer to the open union problem, that pretty much every framework butts up against at some point. For example, in Halogen, in order to unify child component types, you need appropriate injections and projections so you can dispatch correctly. We currently have some ugly combinators that use nested Eithers/Coproducts. Typeable gives you these functions for "free" (injection via Dynamic, projection via coerce).

I think I'll close this issue ... I might want to revive this exploration at some point, but my current attitude (with a bit more experience) is that it's almost always a nice idea to explore alternatives to Typeable. Not that there aren't use cases for it, but the lack of it seems to be one of those things that forces some creativity.

Also, such work-in-progress as I had is quite stale now -- it would need some pretty thorough revisiting.

And, the original motivating use case for me is something I'm now preferring to handle a different way.

@rgrempel I'm curious about the alternative way you found for solving your problem. Is it the stuff in your Elm-in-PureScript project which you talked about in your PS Unscripted - Simulating GADTs for JSON decoder talk? There, you used Coyoneda and Leibniz for type equality.

Yes, it’s that In part.

lt’s also that I no longer am leaving bare Purescript values attached to the DOM somewhere — that had been the original use-case for wanting to know whether the “next” value was of the same type. Now, I’m handling the memory of the previous value as part of the data type within Purescript itself, so have different techniques available.