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
