<div dir="auto">One thing that’s worth noting: type level sets or  maps, whether ord or hash plus eq based, will have much algorithmics for a lot of uses of type level lists. And this difference could be even more dramatic if they’re internalized / primitive </div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jul 3, 2024 at 3:42 AM Hécate via ghc-devs <<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Thank you Gergő, this delightfully cursed! :D<br>
<br>
I was pointed by someone off-list to “Note [Adding built-in type <br>
families]” which is actually very complete!<br>
<br>
One last thing is that since everything is Xi-typed (new form of <br>
"stringly-typed" uncovered), the meaning of the parameters is a bit <br>
blurred when they all are called x1, z1, y1, in GHC.Builtin.Types.Literals.<br>
<br>
See for instance: <br>
<a href="https://hackage.haskell.org/package/ghc-9.10.1/docs/src/GHC.Builtin.Types.Literals.html#interactInertAppendSymbol" rel="noreferrer" target="_blank">https://hackage.haskell.org/package/ghc-9.10.1/docs/src/GHC.Builtin.Types.Literals.html#interactInertAppendSymbol</a><br>
<br>
Le 03/07/2024 à 06:35, ÉRDI Gergő a écrit :<br>
> I know this is not exactly what you're asking, but in similar <br>
> situations I've had very good results from implementing my type family <br>
> as a type checker plugin. Unfortunately it's not code that I can <br>
> share, but it roughly goes like this:<br>
><br>
> 1. Declare a closed type family without defining any clauses:<br>
><br>
>     type family Append (xs :: [k]) (ys :: [k]) :: [k] where<br>
><br>
> 2. Create a typechecker plugin that in `tcPluginInit` looks up this <br>
> `Append` tyfam's tycon, and in `tcPluginRewrite` maps it to a <br>
> `TcPluginRewriter`<br>
><br>
> 3. Inside the `TcPluginRewriter`, you have a `[TcType]` which are your <br>
> arguments (so the two type-level lists that are concatenated in your <br>
> example). If you can compute your tyfam result from that, you can then <br>
> return a `TcPluginRewriteTo` with the "trust-me" coercion `UnivCo`. <br>
> This is what really helps with performance vs. a native <br>
> Haskell-defined tyfam, since it avoids Core passing around huge <br>
> coercion terms corresponding to every reduction step. <br>
> (<a href="https://gitlab.haskell.org/ghc/ghc/-/issues/8095" rel="noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/issues/8095</a> <br>
> <a href="https://gitlab.haskell.org/ghc/ghc/-/issues/22323" rel="noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/issues/22323</a> and many more)<br>
><br>
> The only tricky part is that in step 3, you have to be prepared to <br>
> handle pratially meta arguments. For example, if your arguments are<br>
> `String : Double : []` and `Int : Bool : α` (with some typechecker <br>
> metavariable `α`), you can of course reduce that to `String : Double : <br>
> Int : Bool : α`. But if they are flipped, you can either bail out <br>
> until `α` is solved, or make partial progress to `Int : Bool : Append <br>
> α (String : Double : [])`. I don't know which is the right choice in <br>
> general, since bailing out might expose less info to type inference, <br>
> but partial progressing means your coercion terms will grow, since <br>
> you're restoring some of that step-by-step representation.<br>
><br>
> Let me know if any of this makes sense, I've got the flu atm so the <br>
> above might be too rambly :)<br>
><br>
> Bye,<br>
>     Gergo<br>
><br>
> On Wed, 3 Jul 2024, Hécate via ghc-devs wrote:<br>
><br>
>> Hi GHC devs,<br>
>><br>
>> I was wondering recently, considering that type family evaluation is <br>
>> notoriously slow, how one would implement type-level list <br>
>> concatenation directly within GHC in a way that is much less <br>
>> expensive to run. So I am looking for pointers, as this part of GHC <br>
>> is fairly unknown to me.<br>
>><br>
>> Thinking about it, I'm actually unsure where the tyfam evaluation is <br>
>> happening.<br>
>><br>
>> Any advice would be appreciated.<br>
>><br>
>> Cheers,<br>
>> Hécate<br>
>><br>
>><br>
><br>
-- <br>
Hécate ✨<br>
🐦: @TechnoEmpress<br>
IRC: Hecate<br>
WWW: <a href="https://glitchbra.in" rel="noreferrer" target="_blank">https://glitchbra.in</a><br>
RUN: BSD<br>
<br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div></div>