Implement type family reduction via term-level functions
Motivation
Today I see two problems:
- Type family reduction could be painfully slow. In a complex case (type-level parser) rewriter took ~ 50% compilation time. Example.
- Writing base type families could cause one of two unwanted consequences:
- In the case of adding them as built-in type families code base of GHC could be terribly grown. First char kind MR for example. This MR includes many useful type families, but it was decided to make a smaller MR with only a few TFs to avoid increasing GHC codebase for ~ 2000 lines mostly because of TFs.
- Adding them via plugins is a painful process for developers at least because they have to track all changes in unstable GHC plugin API.
In both cases, developers have to learn many implementation details and internals of GHC.
Proposal
I want to add a new TYPEFUN pragma, which works in the following way:
type family IsAlphaNum c
{-# TYPEFUN IsAlphaNum = Data.Char.isAlphaNum #-}
- This pragma says which term-level function use for reducing type family.
- It reduces only when inputs contain no type variables.
- It works only when all types (both arguments and result) are promotable in any way.
The main idea is to use pre-compiled to bytecode term-level functions in process of type checking which should solve both problems from the motivation part: accelerate type family reduction and make writing TFs much easier.