Haskell 相当于 Rust 的 GAT？

Question

以下 Rust 代码的 Haskell 等价物是什么:

trait Foo {
    type Bar<T>;
    
    fn foo(x: String) -> Self::Bar<String>;
}

我尝试编写以下内容:

class Foo f where
    type Bar f :: * -> *
    foo :: String -> Bar f String

但出现错误:

app/Main.hs:83:5: error:
    • Couldn't match type: Bar f0
                     with: Bar f
      Expected: String -> Bar f String
        Actual: String -> Bar f0 String
      NB: ‘Bar’ is a non-injective type family
      The type variable ‘f0’ is ambiguous
    • In the ambiguity check for ‘foo’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method:
        foo :: forall f. Foo f => String -> Bar f String
      In the class declaration for ‘Foo’
   |
83 |     foo :: String -> Bar f String
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Answer 1

总结评论:

class Foo f where
    type Bar f :: * -> *
    foo :: String -> Bar f String

这是正确的。 Haskell 的“模糊类型”错误正在以一种非常迂回的方式警告您某些事情。具体来说，在 Haskell 基础(没有任何附加扩展)中，函数 foo永远不能被调用。如果我们传递一个String ，它将返回 Bar f String ，和Bar f不是单射的，所以即使我们知道 foo "" 的结果应该是某种特定的具体类型，我们永远无法推断 f由此而来。

如果我们有一个data family ，这是单射的，那么我们就不会收到模棱两可的警告。例如，

class Foo f where
    data Bar f :: * -> *
    foo :: String -> Bar f String

据我所知，Rust 没有类似的东西。这意味着每个 instance Foo定义了一个名为 Bar f :: * -> * 的新类型(不是别名，而是实际的新类型) 。这为我们提供了非常强大的属性，称为注入(inject)性:If Bar f ~ Bar g然后f ~ g (其中 ~ 是 unification operator )。类型不再含糊。如果我们调用foo在我们知道结果必须是 Bar Int String 的情况下，那么我们可以完全自信地得出结论，我们想要的实例是 Foo Int .

现在，由于我们在 Rust 中编写函数调用的方式，关联函数(即没有 self 的函数)不太可能出现歧义。我们将在 Rust 中将等效的函数调用编写为 Foo::<i32>::foo(...) ，使用每个人最喜欢的涡轮鱼运算符，这告诉我们我们想要哪个实例。

Haskell 有类似的语法，但它仅在 compiler extension 下可用。 ，不幸的是，歧义检查不知道这个扩展。为了抑制歧义检查，我们必须启用 third compiler extension .

最后，还有一点微妙之处。您编写类型系列的方式暗示了一些您可能不希望的额外内容。

type Bar f :: * -> *

这个功能非常强大。它说Bar f必须是一个参数明确定义的类型构造函数。 Bar f可以是Maybe ，或者可以是[] ，或任何其他类型的构造函数。但是，至关重要的是，它不能依赖于 nominal 中的论点。方式。也就是说，如果我们在某个地方有另一个类型族(无论是在类型类中还是独立的)，就像这样

type family Baz x where
    Baz Int = [Int]
    Baz String = String

那么我们就无法编写实例type Bar f = Baz ，自 Baz (就其本身而言)没有明确定义。这是 Haskell 中的一个微妙之处:类型别名必须始终完全扩展。在 Rust 中也是如此，但同样，由于我们在 Rust 中使用不同的语法编写类型，因此我们不会太注意到它。但在 Rust 中，没有语法来声明更高种类的类型，因为更高种类的类型不存在。

因此，与 Rust GAT 等价的真正是

class Foo f where
    type Bar f x
    foo :: String -> Bar f String

换句话说，type Bar f :: * -> *说Bar f必须是 Haskell 类型系统中定义明确的值，其种类为 * -> * (并且部分应用的类型别名不是有效的类型级别值)。另一方面，type Bar f x只说Bar f x必须是一个明确定义的类型值 * ，这是一个弱得多的约束。

因此，将所有内容放在一起，这是一个完整的示例:

{-# LANGUAGE TypeFamilies, TypeApplications, AllowAmbiguousTypes #-}

-- Random example type family
type family Baz x where
    Baz Int = [Int]
    Baz String = String

-- The type class
class Foo f where
    type Bar f x
    foo :: String -> Bar f String

-- Example instance
instance Foo Int where
    type Bar Int x = Baz x
    foo x = x ++ " It worked!"

main :: IO ()
main = putStrLn (foo @Int "Hello from Foo Int!")

Try it online!