Why is `typeOfFree :: a -> TypeRef` missing?

Learn
1

Hi,

Typeable is provided for every type and should not be derived explicitly.
So why GHC does not have a function?

typeOfFree :: a -> TypeRep
2

I guess you mean TypeRep rather than TypeRef? Well, there is

typeOf :: Typeable a => a -> TypeRep

https://www.stackage.org/haddock/lts-23.10/base-4.19.2.0/Data-Typeable.html#v:typeOf

so is your question “why does it have a Typeable constraint”? If so then the answer is that without the constraint you can violate parametricity. For example, id would not longer be the only function of type forall a. a -> a.

EDIT: Oh, I’m not sure about forall a. a -> a actually, but it would certainly let you write more than two forall a. a -> a -> a. And the other TypeRep (Data.Reflection.TypeRep) is enough for two forall a. a -> a.

1 Like
3

Thanks

typeOf has constraint by definition because it is a class method.
I am looking for another function. I anticipate that it should exploit some hack beyond unsafeCoerce.

4

Right, I think you’re asking why is there no typeOfFree :: a -> TypeRep, i.e. without class constraint? Well, the answer is parametricity, as I said above. I strongly suggest you try not to define it! Things might go terribly wrong. What are you actually trying to do?

4 Likes
5

Two answers:

  • Practical: GHC has type erasure. Type erasure gets rid of all type information at compile type, there are no types at runtime. So you can’t implement that type. The type constraint’s whole purpose really is to provide a dictionary which preserves that type information.
  • Theoretical: If you can write a function that basically does “if it’s an int, return something different to other types”, then you break parametricity. This hasn’t stopped Haskellers before, look at seq (Free theorems in the presence of seq | Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages), but I think it would be a step too far by most people’s standards.
3 Likes
6

I’m going to elaborate on the benefits of parametricity (and end up implying that the theoretical benefits are practical). Roughly, the “parametric” in “parametric polymorphism” means that the polymorphic function does the same thing for all types, in contrast with OO’s “ad hoc polymorphism” meaning that the polymorphic function can do different things for different types(*).

For example suppose I wrote duo :: a -> [a], and I claim that it does the same thing as replicate 2. How do you or I test it? In Haskell, because of parametricity, you just need one test duo () and you can rest assured that it works the same way for all types. (In Python, you may be paranoid and test for a lot more types.)

BTW mock testing by dependency injection is based on the same premise.

When I teach this stuff in a course, I also put this question on assignments:

Many beginners wish Haskell’s show were show :: a -> String without the “annoying” constraint Show a. Java actually has that as .toString(). Let’s explore what can go wrong: Implement <T> LinkedList<T> funny(T x) to behave differently for different types, unlike my duo example in Haskell.

(*) Of course that’s a first-order pessimistic scaremongering black-and-white story. A more nuanced story is that when programmers aren’t trolling, they don’t abuse the freedom availed by ad hoc, the “different” things are still closely related, so there is a spectrum and there are grey areas.

4 Likes