How to implement type-level list concatenation as a GHC primitive type family
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
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@erdi.hu =-------'
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.Li... 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
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
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.Li...
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
I'd say the main reason to implement `append` in GHC would be to handle
rules that can't be solved by evaluation (e.g., eliminate append [] on the
right, some associativity rule, etc.).
The speed of evaluation shouldn't really be much different as it should be
doing the same thing, more or less.
If there is a big performance hit for just straight evaluation, it might be
better to work on that part of GHC, which would also benefit other
functions, rather than adding more special cased functions.
Cheers,
Iavor
On Tue, Jul 2, 2024, 3:30 PM Hécate via ghc-devs
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
participants (4)
-
Carter Schonwald -
Hécate -
Iavor Diatchki -
ÉRDI Gergő