为什么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)

A Var引入了一个自由变量.lambda抽象绑定一个在体内看起来是自由的变量(如果有匹配的那个).应用程序连接表达式的两个部分的自由变量,删除重复项(因此自由变量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 似乎只是懒惰。

\n\n

\xce\xbb *Main > :t (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x")))\n(Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x")))\n  :: Expr (Remove "x" \'["x"])\n\n\xce\xbb *Main > :t (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: Expr \'[]\n(Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: Expr \'[]\n  :: Expr \'[]\n\n\xce\xbb *Main > :t (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: Expr \'["x"]\n\n<interactive>:1:2:\n    Couldn\'t match type \xe2\x80\x98\'[]\xe2\x80\x99 with \xe2\x80\x98\'["x"]\xe2\x80\x99\n    Expected type: Expr \'["x"]\n      Actual type: Expr (Remove "x" \'["x"])\n    In the expression:\n        (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) ::\n          Expr \'["x"]\n

\n\n\n\n

我更改了定义，因此不依赖于单例库（更容易在临时测试中进行测试）：

\n\n

{-# LANGUAGE TypeOperators, DataKinds, TypeFamilies, GADTs #-}\n\nimport Data.Proxy\nimport GHC.TypeLits\n\ntype family Remove (x :: Symbol) (xs :: [Symbol]) where\n    Remove x \'[] = \'[]\n    Remove x (x \': xs) = Remove x xs\n    Remove x (y \': xs) = y \': Remove x xs\n\ndata Expr (free :: [Symbol]) where\n    Var :: KnownSymbol a => Proxy a -> Expr \'[a]\n    Lam :: KnownSymbol a => Proxy a -> Expr as -> Expr (Remove a as)\n--    App :: Expr free1 -> Expr free2 -> Expr (Union free1 free2)\n

\n