title: When does type-level computation "happen" with type families?
body: <p>I'm trying to form an intuition about when (and how many times) type-level computation with type families "happens" in Haskell. For a concrete example, consider this typeclass for indexing into an <a href="http://hackage.haskell.org/package/sop-core-0.4.0.0/docs/Data-SOP-NP.html" rel="noreferrer">n-ary product</a> using a type-level natural:</p>
  
  <pre><code>{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses,
               ScopedTypeVariables, TypeApplications, AllowAmbiguousTypes
  #-}
  import Data.Kind (Type)
  import Data.SOP (I(..),NP(..)) -- identity functor and n-ary product from "sop-core"
  
  data N = Zero | Succ N -- to be used as a kind
  
  class Key (i :: N) (ts :: [Type]) where
      type Value i ts :: Type
      getValue  :: NP I ts -&gt; Value i ts
  
  instance Key Zero (t:ts) where
      type Value Zero (t:ts) = t
      getValue (I v :* _) = v
  
  instance Key n ts =&gt; Key (Succ n) (t : ts) where
      type Value (Succ n) (t:ts) = Value n ts
      getValue (_ :* rest) = getValue @n rest
  
  getValue' :: forall n ts. Key n ts =&gt; NP I ts -&gt; Value n ts
  getValue' = getValue @n @ts
  
  getTwoValues :: forall n ts. Key n ts =&gt; NP I ts -&gt; NP I ts -&gt; (Value n ts, Value n ts)
  getTwoValues np1 np2 = let getty = getValue @n @ts in (getty np1, getty np2)
  
  main :: IO ()
  main = do let np = I True :* I 'c' :* Nil
            print $ getValue     @(Succ Zero) np
            print $ getValue'    @(Succ Zero) np
            print $ getTwoValues @(Succ Zero) np np
  </code></pre>
  
  <p>My intuition is that typechecking that occurrence of <code>getValue</code> in <code>main</code> triggers the "traversal" of the type-level list at compile-time in search of the corresponding value type <code>Value (Succ Zero) '[Bool,Char]</code>. This traversal can be costly for large lists.</p>
  
  <p>But what about <code>getValue'</code>? Does it trigger the "traversal" of the type level list one time, as before, or <em>two</em> times, one to check <code>getValue'</code> itself and another to check the <code>getValue</code> on which it depends?</p>
  
  <p>And what about <code>getTwoValues</code>? In its signature there are two type family invocations <code>Value n ts</code>, even if they correspond to the exact same type. Do they get computed independently—slowing compilation—or is the computation "shared" at the type level?</p>