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

[Hécate]

Thank you Gergő, this delightfully cursed! :D

I was pointed by someone off-list to “Note [Adding built-in type 
families]” which is actually very complete!

One last thing is that since everything is Xi-typed (new form of 
"stringly-typed" uncovered), the meaning of the parameters is a bit 
blurred when they all are called x1, z1, y1, in GHC.Builtin.Types.Literals.

See for instance: 
https://hackage.haskell.org/package/ghc-9.10.1/docs/src/GHC.Builtin.Types.Literals.html#interactInertAppendSymbol

Le 03/07/2024 à 06:35, ÉRDI Gergő a écrit :
> 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
>>
>>
>
-- 
Hécate ✨
🐦: @TechnoEmpress
IRC: Hecate
WWW: https://glitchbra.in
RUN: BSD