为什么类型系统拒绝我看似有效的程序？ [英] Why is the type system refusing my seemingly valid program?
问题描述
class转换b其中
convert :: a - > b
数据A = A导出显示
数据B = B导出显示
数据C = C导出显示
数据D = DA A | DB B | DC C导出显示
实例转换AA其中转换A = A
实例转换AB其中转换A = B
实例转换AC其中转换A = C
实例转换BA其中转换B = A
实例转换BB其中转换B = B
实例转换BC转换B = C
- 无法将C转换为A
实例转换CB在哪里转换C = B
实例转换CC在哪里转换C = C
获得（DA x）=转换x
获得（DB x）=转换x
get（DC x）= convert x
main = do
print（get（DC C）:: B） - 直到这一行，代码编译得很好。
print（get（DB B）:: A） - 添加这行并不行，不管有没有办法从B转换为A！
有些实例会从 C 转换为 B 并从 B 到 A 。然而，GHC会检查前者，但后者会失败。在检查后，似乎无法推断出 get 的通用类型：
get ::（转换A b，转换B b，转换C b）=> D - > b
我想表达的是： get ::（Convert a_contained_by_D b）=> D - > B ，这似乎是不可能的。是否有任何方法来实现和编译一个函数，它可以完成我的 get 尝试执行的操作，而不会改变其余的设置？
我想表达的是：
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 。这就是为什么你会得到经典的系统管理员逻辑：除非它们都可以 b ，否则不允许获取 D 。 问题是您需要知道 旧，而是包含在作为输入接收的特定 D 中的类型。对？你想要
print（get（DB B）:: A） - 这个工作
print（get DC C）:: A） - 失败
但是 DB B 和 DC C 只是 D 的两个不同元素，就Haskell而言对于每种类型的不同的都是相同的。如果你想区分 D 的元素，那么你需要一个 D - 依赖类型。
DInner :: D - >下面是我如何手写它的方法。 *pre>
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）=转换x
get（DB x）=转换x
get（DC x）=转换x
其中
pi是在运行时传递的数据的绑定形式（与forall ），但在哪些类型可能依赖（不同于 - >）。现在，约束条件不是针对任意Ds，而是您手中的d :: D，而约束可以通过检查DInner来准确计算需要的内容。
没有什么可以说的，但我的
pi。
不幸的是，虽然
pi正在迅速从天而降，尚未降落。无论如何，不像月亮，它可以用棍子达到。毫无疑问，你会抱怨我正在改变设置，但实际上我只是将你的程序从2017年的Haskell翻译成了2015年的Haskell。你会获取它回来，有一天，我的手机型号很高。
没什么可说的，但你可以唱歌。
第1步：打开
DataKinds和KindSignatures并为您的类型构建单例（或者让Richard Eisenberg为你做）。
data A = A导出显示
数据Aey :: A - > *其中 - 认为-ey作为adjectival后缀
Aey :: Aey'A - 如在tomatoey中
数据B = B导出显示
数据Bey :: B - > *其中
Bey :: Bey'B
数据C = C导出显示
数据Cey :: C - > *其中
Cey :: Cey'C
data D = DA A | DB B | DC C导出显示
数据Dey :: D - > *其中
DAey :: Aey a - > Dey（DA a）
DBey :: Bey b - > Dey（DB b）
DCey :: Cey c - > Dey（DC c）
这个想法是（i）数据类型变成种类，（ii）单例表示具有运行时间表示的类型级数据。因此，在运行时存在
a 等类型级别 DA a。
第2步。猜猜谁来
DInner。打开TypeFamilies。type family DInner（d :: D） :: *其中pre>
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
- ^^^^^^^^^^^^^^^^^^
- 这是pi（d :: D） - >
第4步。尝试编写
get和拧紧。我们必须在运行时匹配类型级别d是可表示的证据。我们需要获取专门用于计算DInner的类型级别d。如果我们有适当的pi，我们可以在D值上进行匹配，这个值是双重职责，但是现在匹配取代d代替。get（DAey x）= convert x - - 有x :: Aey a，需要x :: A
get（DBey x）=转换x - 等等
get（DCey x）=转换x - 等等
令人难以置信的是，我们的
xes现在是单身人士，到convert，我们需要底层数据。我们需要更多的单身设备。
第5步。引入并实例化单例类，以降级类型值（只要我们知道它们的运行时代表）。再一次，理查德·艾森伯格的
singletons库可以使用Template-Haskell这个样板，但让我们看看发生了什么
<$ p （s :: k - > *）其中 - s是某个k
类型的单例族s：s - * - - s s是类型 - k
sung的高级版本:: sx - > Sung s - sung是降级功能
实例Sing Aey其中
类型Sung Aey = A
sung Aey = A
实例Sing Bey where
类型Sung Bey = B
唱歌Bey = B
实例Sing Cey其中
类型Sung Cey = C
唱歌Cey = C
实例Sing Dey其中
类型Sung Dey = D
唱歌（DAey aey）= DA（唱aey）
唱歌（DBey bey）= DB（唱歌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。我的Handwave类型get将是Haskell，并且你的代码get会很好。但在此期间，
$ pre code $ main $
print（get（DCey Cey）:: B）
print（get（DBey Bey）:: A）
类型检测就好了。也就是说，你的程序（加上 DInner 和获得的正确类型）似乎是有效的依赖Haskell，而我们'几乎在那里。
Mind this program:
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!
There are instances to convert from C to B and from B to A. Yet, GHC typechecks the former, but fails for the latter. Upon inspection, seems like it isn't able to infer a generic enough type for get:
get :: (Convert A b, Convert B b, Convert C b) => D -> b
What I want to express is: get :: (Convert a_contained_by_D b) => D -> b, which seems impossible. Is there any way to implement and compile a function that does what my get attempts to do, without changing the rest of the setup?
If your program really seemed valid to you, then you would be able to write the type of get that does the job you want in Haskell, not in handwave. Let me help you improve your handwave and uncover the reason you are asking for the moon on a stick.
What I want to express is:
get :: (Convert a_contained_by_D b) => D -> b, which seems impossible.
As stated, that's not quite as precise as you would need. Indeed, it's what Haskell gives you now, in that
get :: (Convert A b, Convert B b, Convert C b) => D -> b
any a which can be contained by D is required, one at a time, to be convertible to that b. And that's why you're getting classic sysadmin logic: no D is allowed to be gotten unless they all can b.
The problem is that you need to know the status not of the type which might be contained in any old D, but rather the type contained in the particular D that you receive as the input. Right? You want
print (get (DB B) :: A) -- this to work
print (get (DC C) :: A) -- this to fail
but DB B and DC C are just two different elements of D, and as far as the Haskell type system is concerned, within each type everything different is the same. If you want to discriminate between elements of D, then you need a D-pendent type. Here's how I'd write it in 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
where pi is the binding form for data which are passed at run time (unlike forall) but on which types may depend (unlike ->). Now the constraint is talking not about arbitrary Ds but the very d :: D in your hand, and the constraint can compute exactly what is needed by inspecting its DInner.
There is nothing you can say that will make it go away but my pi.
Sadly, whilst pi is rapidly descending from the sky, it has not yet landed. None the less, unlike the moon, it can be reached with a stick. No doubt you will complain that I am changing the setup, but really I am just translating your program from Haskell in approximately 2017 to Haskell in 2015. You'll get it back, one day, with the very type I handwaved.
There is nothing you can say, but you can sing.
Step 1. Switch on DataKinds and KindSignatures and build the singletons for your types (or get Richard Eisenberg to do it for you).
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)
The idea is (i) that datatypes become kinds, and (ii) that singletons characterize the type-level data which have a run time presentation. So type level DA a exists at run time provided a does, etc.
Step 2. Guess who's coming to DInner. Switch on TypeFamilies.
type family DInner (d :: D) :: * where
DInner (DA a) = A
DInner (DB b) = B
DInner (DC c) = C
Step 3. Get you some RankNTypes, and now you can write
get :: forall x. forall d. Dey d -> (Convert (DInner d) x) => x
-- ^^^^^^^^^^^^^^^^^^
-- this is a plausible fake of pi (d :: D) ->
Step 4. Try to write get and screw up. We have to match on the run time evidence that the type level d is representable. We need that to get the type level d specialised in the computation of DInner. If we had proper pi, we could match on a D value that serves double duty, but for now, match on Dey d instead.
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
Maddeningly, our xes are now singletons, where, to convert, we need the underlying data. We need more of the singleton apparatus.
Step 5. Introduce and instantiate the singleton class, to "demote" type level values (as long as we know their run time representatives). Again, Richard Eisenberg's singletons library can Template-Haskell the boilerplate out of this, but let's see what's going on
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)
Step 6. Do it.
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)
Be assured, when we have proper pi, those DAeys will be actual DAs and those xs will no longer need to be sung. My handwave type for get will be Haskell, and your code for get will be fine. But in the meantime
main = do
print (get (DCey Cey) :: B)
print (get (DBey Bey) :: A)
typechecks just fine. That's to say, your program (plus DInner and the correct type for get) seems like valid Dependent Haskell, and we're nearly there.
这篇关于为什么类型系统拒绝我看似有效的程序？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
