haskell - 为什么 GHC 不会减少我的类型族？

Question

这是一个无类型的 lambda 演算，其术语由它们的自由变量索引。我正在使用 singletons 用于类型级字符串的单例值的库。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Singletons
import Data.Singletons.TypeLits

data Expr (free :: [Symbol]) where
    Var :: Sing a -> Expr '[a]
    Lam :: Sing a -> Expr as -> Expr (Remove a as)
    App :: Expr free1 -> Expr free2 -> Expr (Union free1 free2)

一个 Var引入一个自由变量。一个 lambda 抽象绑定(bind)了一个在主体中自由出现的变量(如果有一个匹配的话)。应用程序将表达式的两个部分的自由变量连接起来，删除重复项(因此 x y 的自由变量是 x 和 y ，而 x x 的自由变量只是 x )。我写出了那些类型族:

type family Remove x xs where
    Remove x '[] = '[]
    Remove x (x ': xs) = Remove x xs
    Remove x (y ': xs) = y ': Remove x xs

type family Union xs ys where
    Union xs ys = Nub (xs :++ ys)

type family xs :++ ys where
    '[] :++ ys = ys
    (x ': xs) :++ ys = x ': (xs :++ ys)

type family Nub xs where
    Nub xs = Nub' '[] xs

type family Nub' seen xs where
    Nub' seen '[] = '[]
    Nub' seen (x ': xs) = If (Elem x seen) (Nub' seen xs) (Nub' (x ': seen) (x ': xs))

type family If c t f where
    If True t f = t
    If False t f = f

type family Elem x xs where
    Elem x '[] = False
    Elem x (x ': xs) = True
    Elem x (y ': xs) = Elem x xs

我在交互式提示下对此进行了测试:

ghci> :t Var (sing :: Sing "x")
Var (sing :: Sing "x") :: Expr '["x"]  -- good
ghci> :t (Lam (sing :: Sing "x") (Var (sing :: Sing "x")))
(Lam (sing :: Sing "x") (Var (sing :: Sing "x")))
  :: Expr (Remove "x" '["x"])  -- not so good

我惊讶地发现身份函数的类型 \x. x是 Expr (Remove "x" '["x"]) ，而不是 Expr '[] . GHC 似乎不愿意评估类型族 Remove .
我进行了更多实验，发现这对我的类型家族本身来说不是问题 - GHC 很乐意在这种情况下减少它:

ghci> :t (Proxy :: Proxy (Remove "x" '["x"]))
(Proxy :: Proxy (Remove "x" '["x"])) :: Proxy '[]

那么:为什么 GHC 不会减少 Remove "x" '["x"]至 '[]当我查询我的 GADT 的类型时？一般来说，类型检查器何时会或不会评估类型族？我可以使用启发式方法来避免对其行为感到惊讶吗？

Answer 1

有用。 GHC 似乎只是懒惰。

λ *Main > :t (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x")))
(Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x")))
  :: Expr (Remove "x" '["x"])

λ *Main > :t (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: Expr '[]
(Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: Expr '[]
  :: Expr '[]

λ *Main > :t (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: Expr '["x"]

<interactive>:1:2:
    Couldn't match type ‘'[]’ with ‘'["x"]’
    Expected type: Expr '["x"]
      Actual type: Expr (Remove "x" '["x"])
    In the expression:
        (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) ::
          Expr '["x"]

我更改了定义，因此不依赖单例库(更容易在 ad-hoc 中测试):

{-# LANGUAGE TypeOperators, DataKinds, TypeFamilies, GADTs #-}

import Data.Proxy
import GHC.TypeLits

type family Remove (x :: Symbol) (xs :: [Symbol]) where
    Remove x '[] = '[]
    Remove x (x ': xs) = Remove x xs
    Remove x (y ': xs) = y ': Remove x xs

data Expr (free :: [Symbol]) where
    Var :: KnownSymbol a => Proxy a -> Expr '[a]
    Lam :: KnownSymbol a => Proxy a -> Expr as -> Expr (Remove a as)
--    App :: Expr free1 -> Expr free2 -> Expr (Union free1 free2)