How do type families with no equations work?

Learn
1

The package constraints shows these type families:
type family Take :: Nat → Symbol → Symbol where
type family Drop :: Nat → Symbol → Symbol where
type family Length :: Symbol → Nat where

This is similar to GHC.TypeLits, which features

type family AppendSymbol (m ::Symbol) (n :: Symbol) :: Symbol
type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol

I used to think these were magically defined through GHC/Base internal magic, but they also occur in Data.Constraint.Symbol. Could I define them myself?

1 Like
2

I think these are empty type families, meaning they don’t reduce. I can confirm that behaviour opening the package in a repl: :k! Take 1 "hi" spits out Take 1 "hi". I think the package’s focus wasn’t on type-level computation. (Also, back in the day, you couldn’t deconstruct Symbols.)

You can define AppendSymbol and ConsSymbol yourself if you want, but those type families are indeed “magical” in GHC, and will perform faster than anything you write. (I know they look similarly empty in the Hackage source (GHC.Internal.TypeLits), but they are handled specially in the compiler-- see compiler/GHC/Builtin/Types/Literals.hs.)

5 Likes