为啥类型系统拒绝我看似有效的程序？

Posted 2023-02-25

【中文标题】为啥类型系统拒绝我看似有效的程序？

【英文标题】：Why is the type system refusing my seemingly valid program?为什么类型系统拒绝我看似有效的程序？

【发布时间】：2015-04-27 03:36:17

【问题描述】：

注意这个程序：

class Convert a b where
    convert :: a -> b

data A = A deriving Show
data B = B deriving Show
data C = C deriving Show
data D = DA A | DB B | DC C deriving Show

instance Convert A A where convert A = A
instance Convert A B where convert A = B
instance Convert A C where convert A = C
instance Convert B A where convert B = A
instance Convert B B where convert B = B
instance Convert B C where convert B = C
-- There is no way to convert from C to A
instance Convert C B where convert C = B
instance Convert C C where convert C = C

get (DA x) = convert x
get (DB x) = convert x
get (DC x) = convert x

main = do
    print (get (DC C) :: B) -- Up to this line, code compiles fine.
    print (get (DB B) :: A) -- Add this line and it doesn't, regardless of having a way to convert from B to A!

有些实例可以从 C 转换为 B 以及从 B 转换为 A。然而，GHC 对前者进行类型检查，但对后者失败。经检查，似乎无法为get 推断出足够通用的类型：

get :: (Convert A b, Convert B b, Convert C b) => D -> b

我要表达的是：get :: (Convert a_contained_by_D b) => D -> b，这似乎是不可能的。有没有什么方法可以实现和编译一个函数来完成我的get 尝试做的事情，而无需更改其余设置？

【问题讨论】：

只要您有Convert C A 的实例，即使它是instance Convert C A where convert _ = error "Cannot convert from C to A"，它也可以正常编译。你有什么理由不能简单地这样做吗？

如果您担心类型安全（并且这是一个部分功能），您可以考虑将其设为 maybeConvert :: a -> Maybe b

【参考方案1】：

如果您的程序真的对您来说似乎是有效的，那么您将能够编写 get 的类型，在 Haskell 中完成您想要的工作，而不是在 handwave 中。让我帮你提高你的手波水平，揭开你在棍子上要月亮的原因。

我要表达的是：get :: (Convert a_contained_by_D b) => D -> b，这似乎是不可能的。

如上所述，这并不像您需要的那样精确。事实上，这就是 Haskell 现在为您提供的，在那个

get :: (Convert A b, Convert B b, Convert C b) => D -> b

需要D 包含的任何a，一次一个，才能转换为b。这就是为什么您要获得经典的系统管理员逻辑：不允许获得 D，除非他们都可以获得 b。

问题是您需要知道的状态不是可能包含在 any 旧 D 中的类型，而是您收到的特定 D 中包含的类型输入。正确的？你想要的

print (get (DB B) :: A)  -- this to work
print (get (DC C) :: A)  -- this to fail

但是DB B 和DC C 只是D 的两个不同元素，并且就Haskell 类型系统而言，在每种类型中所有不同之处都是相同的。如果要区分D 的元素，则需要D-pendent 类型。这是我在 handwave 中的写法。

DInner :: D -> *
DInner (DA a) = A
DInner (DB b) = B
DInner (DC c) = C

get :: forall x. pi (d :: D) -> (Convert (DInner d) x) => x
get (DA x) = convert x
get (DB x) = convert x
get (DC x) = convert x

其中pi 是在运行时传递的数据的绑定形式（与forall 不同），但取决于哪些类型（与-> 不同）。现在约束不是在谈论任意的Ds，而是在你手中的非常d :: D，并且约束可以通过检查其DInner来准确计算所需的内容。

除了我的pi之外，没有什么可以让它消失的。

遗憾的是，虽然pi 正在迅速从天而降，但它还没有降落。尽管如此，与月亮不同，它可以用一根棍子到达。毫无疑问，您会抱怨我正在更改设置，但实际上我只是将您的程序从大约 2017 年的 Haskell 翻译到 2015 年的 Haskell。您将在某一天将 get 用我挥手的那种类型返回。

你无话可说，但你可以唱歌。

第 1 步。打开 DataKinds 和 KindSignatures 并为您的类型构建单例（或让 Richard Eisenberg 为您完成）。

data A = A deriving Show
data Aey :: A -> * where  -- think of "-ey" as an adjectival suffix
  Aey :: Aey 'A           -- as in "tomatoey"

data B = B deriving Show
data Bey :: B -> * where
  Bey :: Bey 'B

data C = C deriving Show
data Cey :: C -> * where
  Cey :: Cey 'C

data D = DA A | DB B | DC C deriving Show
data Dey :: D -> * where
  DAey :: Aey a -> Dey (DA a)
  DBey :: Bey b -> Dey (DB b)
  DCey :: Cey c -> Dey (DC c)

这个想法是（i）数据类型变成种类，以及（ii）单例表征具有运行时表示的类型级数据。所以类型级别 DA a 存在于运行时，前提是 a 存在，等等。

第 2 步。猜猜谁来DInner。开启TypeFamilies。

type family DInner (d :: D) :: * where
  DInner (DA a) = A
  DInner (DB b) = B
  DInner (DC c) = C

第 3 步。给你一些RankNTypes，现在你可以写了

get :: forall x. forall d. Dey d -> (Convert (DInner d) x) => x
--               ^^^^^^^^^^^^^^^^^^
-- this is a plausible fake of pi (d :: D) ->

第 4 步。尝试写 get 并搞砸。我们必须匹配类型级别d 是可表示的运行时证据。我们需要它来获得专门用于计算DInner 的类型级别d。如果我们有正确的pi，我们可以匹配一个具有双重职责的D 值，但现在，改为匹配Dey d。

get (DAey x) = convert x   -- have x :: Aey a, need x :: A
get (DBey x) = convert x   -- and so on
get (DCey x) = convert x   -- and so forth

令人发指的是，我们的xes 现在是单例，对于convert，我们需要基础数据。我们需要更多的单例设备。

第 5 步。引入并实例化单例类，以“降级”类型级别的值（只要我们知道它们的运行时代表）。同样，Richard Eisenberg 的 singletons 库可以从 Template-Haskell 中提取样板，但让我们看看发生了什么

class Sing (s :: k -> *) where   -- s is the singleton family for some k
  type Sung s :: *               -- Sung s is the type-level version of k
  sung :: s x -> Sung s          -- sung is the demotion function

instance Sing Aey where
  type Sung Aey = A
  sung Aey = A

instance Sing Bey where
  type Sung Bey = B
  sung Bey = B

instance Sing Cey where
  type Sung Cey = C
  sung Cey = C

instance Sing Dey where
  type Sung Dey = D
  sung (DAey aey) = DA (sung aey)
  sung (DBey bey) = DB (sung bey)
  sung (DCey cey) = DC (sung cey)

第 6 步。做吧。

get :: forall x. forall d. Dey d -> (Convert (DInner d) x) => x
get (DAey x) = convert (sung x)
get (DBey x) = convert (sung x)
get (DCey x) = convert (sung x)

请放心，当我们有正确的pi 时，那些DAeys 将是实际的DAs，而那些xs 将不再需要是sung。我的get 的handwave 类型将是Haskell，而get 的代码会很好。但与此同时

main = do
  print (get (DCey Cey) :: B)
  print (get (DBey Bey) :: A)

类型检查就好了。也就是说，您的程序（加上 DInner 和 get 的正确类型）看起来像是有效的 Dependent Haskell，我们快到了。

【讨论】：

有一天我希望我对类型系统有这样的了解。最好在 pi 到来之前！杰出的。谢谢。

我希望有一天，我能写出像你一样有趣的枯燥文字——不一定是关于 Haskell 的……

啊哈哈哈“D-pendent”成就了我的一天。绝对精彩的答案。

在 GHC 7.6 上，我无法使用 type family DInner (d :: D) :: * where 语法，而是必须将其转换为使用 type families 上 Haskell Wiki 页面上指定的 type instance 语法。封闭类型族似乎仅在 GHC 7.8+ 中可用。

【参考方案2】：

要使该代码工作，它必须与任何相同类型的参数一起工作。也就是说，如果

get (DB B) :: A

然后工作

get anyValueOfTypeD :: A

必须工作，包括

get (DC C) :: A

由于缺少从 C 到 A 的实例而无法工作。

第一行

get anyValueOfTypeD :: B

之所以有效，是因为我们确实拥有将 A、B、C 转换为 B 的所有三个实例。

我认为没有任何解决方法可以让您保持 D 类型不变。如果你可以改变它，你可以使用例如

data D a = DA a | DB a | DC a

（请注意，它与原版有很大不同），甚至是 GADT

data D x where
  DA :: A -> D A
  DB :: B -> D B
  DC :: C -> D C

【讨论】：

嗯，谢谢！我赞成你，因为这是信息丰富且正确的，但我特别要求解决方法。

@Viclib 我对此添加了一些内容，但我不确定是否有任何解决方法可以让您按原样使用它们。