Safely Exposing Haskell’s Hidden Powers

Haskell is an influential functional programming language with an advanced type system that is capable of detecting many bugs. In some cases, the Glasgow Haskell Compiler (GHC), the de facto standard compiler of Haskell, is more powerful than the Haskell programming language itself. It has the capability to do things programmers cannot do using the language because of safety reasons. We refer to this functionality as Haskell's hidden powers. We safely expose the following three hidden powers to Haskell programmers that were previously unavailable or only available with less safety guarantees. We expose the hidden power of unification variables, which are used to discover unknown types during type inference, by developing partial type signatures: type signatures that can contain unknown parts, indicated with wildcards ('_'). Partial type signatures have been integrated in GHC and are used in practice. We expose the hidden power of the dictionary translation and explicit dictionary application to overcome the restriction that only a single instance of a type class can ever be provided for a type without compromising on the two safety properties that rely on this restriction: global uniqueness of instances, for which we formulate the role criterion, and coherence, for which we provide a check and a formal proof. We have implemented a working prototype in GHC. We expose the full power and expressiveness of meta-programming in a strongly type-safe manner. Whereas a weakly type-safe meta-programming system only gives guarantees about the type safety of the meta-program, a strongly type-safe one also gives guarantees about the type-safety of the programs generated by the meta-program. To overcome the limited expressivity of existing systems, we propose a new approach based on two key design decisions: (1) we use a dependently-typed meta-language to attain the expressiveness required to represent well-typed object programs, and (2) we use a simpler, explicitly-typed intermediate language of the compiler as the object language. With our prototype implementation for GHC, we have developed strongly type-safe variants of real-world meta-programs to demonstrate the applicability of our approach.status: publishe