How to implement type-level list concatenation as a GHC primitive type family

[ÉRDI Gergő]

I know this is not exactly what you're asking, but in similar situations 
I've had very good results from implementing my type family as a type 
checker plugin. Unfortunately it's not code that I can share, but it 
roughly goes like this:

1. Declare a closed type family without defining any clauses:

     type family Append (xs :: [k]) (ys :: [k]) :: [k] where

2. Create a typechecker plugin that in `tcPluginInit` looks up this 
`Append` tyfam's tycon, and in `tcPluginRewrite` maps it to a 
`TcPluginRewriter`

3. Inside the `TcPluginRewriter`, you have a `[TcType]` which are your 
arguments (so the two type-level lists that are concatenated in your 
example). If you can compute your tyfam result from that, you can then 
return a `TcPluginRewriteTo` with the "trust-me" coercion `UnivCo`. This 
is what really helps with performance vs. a native Haskell-defined tyfam, 
since it avoids Core passing around huge coercion terms corresponding 
to every reduction step. (https://gitlab.haskell.org/ghc/ghc/-/issues/8095 
https://gitlab.haskell.org/ghc/ghc/-/issues/22323 and many more)

The only tricky part is that in step 3, you have to be prepared to handle 
pratially meta arguments. For example, if your arguments are
`String : Double : []` and `Int : Bool : α` (with some typechecker 
metavariable `α`), you can of course reduce that to `String : Double : Int 
: Bool : α`. But if they are flipped, you can either bail out until `α` 
is solved, or make partial progress to `Int : Bool : Append α (String : 
Double : [])`. I don't know which is the right choice in general, since 
bailing out might expose less info to type inference, but partial 
progressing means your coercion terms will grow, since you're restoring 
some of that step-by-step representation.

Let me know if any of this makes sense, I've got the flu atm so the above 
might be too rambly :)

Bye,
 	Gergo

On Wed, 3 Jul 2024, Hécate via ghc-devs wrote:

> Hi GHC devs,
>
> I was wondering recently, considering that type family evaluation is 
> notoriously slow, how one would implement type-level list concatenation 
> directly within GHC in a way that is much less expensive to run. So I am 
> looking for pointers, as this part of GHC is fairly unknown to me.
>
> Thinking about it, I'm actually unsure where the tyfam evaluation is 
> happening.
>
> Any advice would be appreciated.
>
> Cheers,
> Hécate
>
>

-- 

   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= gergo at erdi.hu =-------'