Hacker News new | ask | show | jobs
by lower 1803 days ago
Yes, types are usually represented by a DAG with sharing. OCaml does so, for example, and I assume ghc does something similar.

So, while id id has type ('a -> 'a) -> ('a -> 'a), this is stored in memory by a pointer structure that amounts to let 'b = ('a -> 'a) in ('b -> 'b). The type of id id id would become let 'b = ('a -> 'a) in let 'c = ('b -> 'b) in ('c -> 'c). This grows linearly. If one were to write out the types without sharing then their size would grow exponentially.
2 comments
chowells 1803 days ago
There was a bug in ghci (the GHC REPL) for a while which made it take exponential time to print the type of `id id id id id id id id id`. It used the linear representation for type-checking, but the pretty-printer was not implemented so cleverly.

Apparently that's been fixed. I can't confirm because that's not something I ever check the type of.

link
kmill 1802 days ago
It seems to me that id id id ... id always has type a -> a. If you're referring to the type of the first id in the sequence, then what you're saying makes sense.
link