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

Question

注意这个程序:

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尝试做，而不改变其余的设置？

Answer 1

如果您的程序对您来说确实有效，那么您将能够编写 get 的类型这可以在 Haskell 中完成您想要的工作，而不是在 handwave 中。让我帮助你提高你的手波并揭示你在棍子上要求月亮的原因。

What I want to express is: get :: (Convert a_contained_by_D b) => D -> b, which seems impossible.

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

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

任意 a可以被 D 包含需要一次一个，才能转换为 b .这就是您获得经典系统管理逻辑的原因:否 D除非他们都能得到 b .

问题是您需要知道状态不是任何旧的 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 - 悬垂类型。以下是我在 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是在运行时传递的数据的绑定(bind)形式(与 forall 不同)，但取决于哪些类型(与 -> 不同)。现在约束不是在谈论任意 D s 但非常 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 的运行时证据。是有代表性的。我们需要它来获得类型级别 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

令人发指的是，我们的 x es 现在是单例，其中，到 convert ，我们需要基础数据。我们需要更多的单例设备。

步骤 5. 引入并实例化单例类，以“降级”类型级别的值(只要我们知道它们的运行时代表)。同样，理查德·艾森伯格的 singletons库可以从中模板-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 , 那些 DAey s 将是实际的 DA s 和那些 x s 不再需要是 sung .我的手电类型为 get将是 Haskell，您的代码为 get会没事的。但与此同时

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

类型检查就好了。也就是说，您的程序(加上 DInner 和 get 的正确类型)似乎是有效的 Dependent Haskell，我们快到了。