haskell - 何时使用类型族进行类型级计算 "happen"？

Question

我试图对 Haskell 中类型族“发生”的类型级计算何时(以及多少次)形成一种直觉。对于一个具体的例子，考虑这个类型类来索引到 n-ary product使用类型级自然:

{-# 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 -> Value i ts

instance Key Zero (t:ts) where
    type Value Zero (t:ts) = t
    getValue (I v :* _) = v

instance Key n ts => 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 => NP I ts -> Value n ts
getValue' = getValue @n @ts

getTwoValues :: forall n ts. Key n ts => NP I ts -> NP I ts -> (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

我的直觉是对 getValue 的出现进行类型检查。在 main在编译时触发类型级别列表的“遍历”以搜索相应的值类型 Value (Succ Zero) '[Bool,Char] .对于大型列表，这种遍历可能代价高昂。

但是 getValue' 呢？ ?是像以前一样触发类型级别列表的“遍历”一次，还是两次，一次检查 getValue'自己和另一个要检查 getValue它取决于哪个？

那么 getTwoValues呢？ ?在其签名中有两种类型族调用 Value n ts ，即使它们对应于完全相同的类型。它们是独立计算的——减慢编译速度——还是在类型级别“共享”计算？

Answer 1

Haskell 具有“类型删除语义”。也就是说，假设编译器可以解析所有类型，那么类型推断会在编译时“发生”；运行时没有计算效果。

编译器可能无法在单独编译下“解析所有类型”:也就是说，它需要推迟对该模块的推理，直到编译导入该模块的其他模块。在最坏的情况下，这可能需要推迟执行时间；然后执行的是字典传递/字典查找。

解释现代 GHC 中的类型推断(包括类型族)的论文是 OutsideIn(X)。你的答案会在那里。

但说真的，你为什么要为“计算”类型的性能内部而烦恼呢？就是这样。你的整个问题都有一种期待程序算法的难闻气味；而类型求解的行为更像逻辑编程。询问“何时”执行它甚至比询问“何时”用惰性语言评估表达式更不合适。