返回 Haskell 中的类型子集

Question

我正在尝试将函数的 return 类型限制为（种类）构造函数的子集。我可以使用 typeclasses 来限制输入类型，但是当我在 return 类型上尝试相同的技术时，如下所示，我收到 Couldn't match type ‘s’ with ‘'A’ 错误。

有没有办法将下面的 bar 函数限制为 return SomeA 或 SomeB？

似乎 Liquid Haskell 是一种替代方法，但似乎仅使用 DataKinds、GADTs and/or [=18= 之类的东西就可以做到这一点].

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

module Test where

data State = A | B | C

class AorB (s :: State)
instance AorB 'A
instance AorB 'B

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

-- This works
foo :: AorB s => Some s -> Bool
foo aorb = case aorb of
  SomeA -> True
  SomeB -> False

-- This fails to compile with ""Couldn't match type ‘s’ with ‘'A’""
bar :: AorB s => Some s
bar = SomeA

Answer 1

这里有几件事。如果您使用 -Wall （您应该这样做！） 进行编译，您会发现您对 foo 的定义给出了一个无穷无尽的模式警告。它应该，因为您定义 AorB 的方式是 "open"。也就是说，另一个模块中的某人可以自由声明

instance AorB 'C

然后你对 foo 的定义将突然变得无效，因为它无法处理 SomeC 的情况。要得到你要找的东西，你应该使用 封闭类型家族 :

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

这个家族是在 State 上完全定义的。然后，我们将像这样定义您之前的 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是可满足的，所以我们应该可以得到一个Some B，对吧？但不是根据您的实施。所以这里在逻辑上是错误的。您可能正在寻找 return 一个 存在量化 s，换句话说，您希望 bar 函数选择哪个 s它是，而不是来电者。非正式地

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

也就是说，bar选择了一个s，return选择了一个Some s，连同AorB s成立的一些证据。这不再是暗示，我们不会让调用者有责任证明 bar 选择的类型是 A 或 B ——调用者不知道选择了什么.

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

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

Ex c f可以读作"there exists a such that c a holds and there is a value 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

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

Answer 2

这是根据@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

返回 Haskell 中的类型子集

Returning a subset of types in Haskell

haskell

typeclass

dependent-type

liquid-haskell