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

注意这个程序：

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 to B和来自B to 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尝试在不更改其余设置的情况下做什么？

如果你的程序really对你来说似乎有效，那么你就可以写出以下类型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

any a可以包含在D需要一次一个，才能转换为该b。这就是为什么你会得到经典的系统管理逻辑：不D被允许获得，除非他们都可以b.

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

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

but DB B and DC C只是两个不同的元素D，就 Haskell 类型系统而言，在每种类型中一切不同都是一样的。如果你想区分以下元素D，那么你需要一个D- 下垂型。这是我用手波写的方式。

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

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

你无法说任何话可以让它消失，但我的pi.

可悲的是，同时pi正在从天而降，还没有落地。尽管如此，与月球不同的是，它可以用棍子到达。毫无疑问你会抱怨我正在改变设置，但实际上我只是将你的程序从大约 2017 年的 Haskell 翻译成 2015 年的 Haskell。你会get有一天，它回来了，和我挥手时的那种类型一样。

你无话可说，但你可以sing.

步骤 1. 开机DataKinds and 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是有代表性的。我们需要它来获得类型级别d专门从事计算DInner。如果我们有适当的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. 引入并实例化单例类，以“降级”类型级别值（只要我们知道它们的运行时代表）。再次，理查德·艾森伯格的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, those DAeys 将是实际的DA和那些xs 将不再需要sung。我的手波类型为get将是 Haskell，你的代码是get会没事的。但与此同时

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

类型检查就好了。也就是说，你的程序（加上DInner以及正确的类型get) 看起来像是有效的 Dependent Haskell，而且我们已经快到了。