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

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 ::(转换a_contained_by_D b)=> D - > b,这似乎是不可能的.有没有办法实现和编译一个能够完成我的get尝试的函数,而无需更改其余的设置？

Answer 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

任何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是在运行时传递的数据的绑定形式(不像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可表示的证据.我们需要这样才能获得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现在是单身人士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,那些DAey将是实际DA的,那些x将不再需要sung.我的handwave类型get将是Haskell,你的代码get将没问题.但与此同时

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

typechecks就好了.也就是说,你的程序(加上DInner和正确的类型get)似乎是有效的Dependent Haskell,我们几乎就在那里.

Answer 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