1
4

2 回答 2

4

这里有几件事。如果你编译-Wall （你应该！）你会发现你的定义foo给出了一个不详尽的模式警告。它应该，因为你定义的方式AorB是“开放的”。也就是说，另一个模块中的某人可以自由声明

instance AorB 'C

然后您的定义foo将突然变得无效，因为它无法处理SomeC此案。要获得您正在寻找的东西，您应该使用封闭类型系列：

type family IsAorB s where
    IsAorB 'A = 'True
    IsAorB 'B = 'True
    IsAorB _  = 'False

这个族完全定义在States 上。然后，我们将像这样定义您之前的AorB约束：

type AorB s = IsAorB s ~ 'True

但是，稍后我们将需要以AorB柯里化形式使用，这对于类型同义词是不允许的。有一个用于声明 curriable 同义词的习语有点笨拙，但这是我们目前最好的：

class    (IsAorB s ~ 'True) => AorB s
instance (IsAorB s ~ 'True) => AorB s

不管怎样，有了这个新定义，你会发现不详尽的模式警告消失了foo。好的。

现在回答你的问题。您的定义的问题（forall为了清楚起见，明确添加了）

bar :: forall s. AorB s => Some s
bar = SomeA

是允许我们实例化bar @B，给我们

bar @B :: AorB B => Some B
bar = SomeA

AorB B是可满足的，所以我们应该能够得到 a Some B，对吧？但不是根据你的实现。所以这里在逻辑上是错误的。您可能希望返回一个存在量化 s的 ，换句话说，您希望bar函数选择s它，而不是调用者。非正式地

bar :: exists s. AorB s <AND> Some s

也就是说，bar选择一个s，并返回一个Some s，以及一些AorB s成立的证据。这不再是一个暗示，我们不会让调用者负责证明bar选择的类型是A或者B——调用者不知道选择了什么。

Haskell 不直接支持存在类型，但我们可以使用 GADT 对它们进行建模（确保使用PolyKindsand ConstraintKinds）

data Ex c f where
     Ex :: c a => f a -> Ex c f

Ex c f可以读作“存在a这样的c a存在并且存在价值f a”。这是存在的，因为变量a没有出现在 中Ex c f，它被构造函数隐藏了。现在我们可以实现bar

bar :: Ex AorB Some
bar = Ex SomeA

我们可以通过将其传递给您的来测试约束是否正确传播foo：

test :: Bool
test = case bar of Ex s -> foo s

你去吧。

也就是说，在设计方面我只想说

bar :: Some A

反而。类型签名应尽可能提供信息。不要隐藏你知道的信息——让抽象来隐藏。当您隐藏有关您的假设/论点的信息时，您正在使您的签名更强大；当你隐瞒你的结果时，你正在使它变得更弱。让它强大。

于 2018-07-22T00:44:26.390 回答
1

以下是基于@luqui 回答的完整工作代码，供参考：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}

module Test2 where

data State = A | B | C

type family IsAorB (s :: State) where
  IsAorB 'A = 'True
  IsAorB 'B = 'True
  IsAorB _  = 'False

-- type AorB s = IsAorB s ~ 'True

class (IsAorB s ~ 'True) => AorB s
instance (IsAorB s ~ 'True) => AorB s

data Some (s :: State) where
  SomeA :: Some 'A
  SomeB :: Some 'B
  SomeC :: Some 'C

data Ex c f where
  Ex :: c a => f a -> Ex c f

bar :: Ex AorB Some
bar = Ex SomeA
于 2018-07-22T01:43:12.077 回答