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

[Carter Schonwald]

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

On Wed, Jul 3, 2024 at 3:42 AM Hécate via ghc-devs <ghc-devs at haskell.org>
wrote:

> 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
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20240810/b67398ca/attachment.html>