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@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@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
