GHC为什么不减少我的类型家庭? [英] Why won't GHC reduce my type family?

问题描述

这是无类型的lambda演算，其项由其自由变量索引.我正在使用 singletons 库获取类型级别字符串的单例值

Here's an untyped lambda calculus whose terms are indexed by their free variables. I'm using the singletons library for singleton values of type-level strings.

{-# 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).我写出了这些类型族:

A Var introduces a free variable. A lambda abstraction binds a variable which appears free in the body (if there's one which matches). Applications join up the free variables of the two parts of the expression, removing duplicates (so the free variables of x y are x and y, while the free variables of x x are just x). I wrote out those type families:

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

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

I tested this out at the interactive prompt:

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很高兴在这种情况下减少这种情况:

I was surprised to learn that the type of the identity function \x. x is Expr (Remove "x" '["x"]), not Expr '[]. GHC seems unwilling to evaluate the type family Remove. I experimented a little more and learned that it's not a problem with my type family per se - GHC is happy to reduce it in this case:

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

所以:为什么我查询GADT的类型时，GHC为何不将Remove "x" '["x"]减小为'[]?通常，类型检查器何时会评估类型族?我可以使用试探法来避免对其行为感到惊讶吗?

So: Why won't GHC reduce Remove "x" '["x"] to '[] when I query the type of my GADT? In general, when will-or-won't the type checker evaluate a type family? Are there heuristics I can use to avoid being surprised by its behaviour?

推荐答案

它有效. GHC似乎只是懒惰.

It works. GHC seems to be just lazy.

λ *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"]

---

我更改了定义，因此不依赖单例库(更容易在临时进行测试):

---

I changed definitions so there isn't dependency on singletons library (easier to test in 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)

这篇关于GHC为什么不减少我的类型家庭?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！