4

我刚刚发明了以下替代定义Maybe：

type Maybe' a = forall b. (b -> (a -> b) -> b)

just :: a -> Maybe' a
just a = \d f -> f a

nothing :: Maybe' a
nothing = const

bind :: Maybe' a -> (a -> Maybe' b) -> Maybe' b
bind ma f = ma nothing (\a -> f a)

问题是我无法添加以下实例声明

instance Monad (Maybe') where
    return = just
    a >>= f = bind a f

错误信息是：

Type synonym Maybe' should have 1 argument, but has been given none

有什么办法可以解决吗？

4

3 回答 3

8

如果Monad将其包装在newtype. 您还必须使用PolymorphicComponents扩展名（一种较弱的形式RankNTypes）来普遍量化b：

{-# LANGUAGE PolymorphicComponents #-}

newtype Maybe' a = Maybe' { unMaybe' :: forall b. (b -> (a -> b) -> b) }

just :: a -> Maybe' a
just a = Maybe' (\d f -> f a)

nothing :: Maybe' a
nothing = Maybe' const

bind :: Maybe' a -> (a -> Maybe' b) -> Maybe' b
bind ma f = Maybe' (unMaybe' ma const (\a -> unMaybe' (f a)))

instance Monad Maybe' where
    return = just
    (>>=)  = bind

您需要新类型的原因是 Haskell 类型的同义词不会“坚持”。当 Haskell 尝试将Maybe'没有 newtype的类型签名与Monad类型类匹配时，它根本看不到Maybe'，而是看到原始的底层函数类型。

Haskell 使用“主要类型”来确保每种类型都有一个范式。底层函数的范式为：

(->) b ((->) ((->) a b) b)

类型同义词不会改变类型的正常形式，但新类型会。具体来说，newtype在这种情况下，正在重新排列类型，以便正常形式现在具有实例所需a的最后一个类型参数。Monad

于 2013-08-16T03:25:31.670 回答
6

类型同义词不是类型。有了类型，您就没有类型同义词newtype。* -> *因此，您的问题现在简化为为什么类型同义词不是一流的。

答案可能是因为一流的同义词会产生太多的歧义，并且在简单的情况下无法进行类型推断。

type First a b = (a, b)
type Second a b = (b, a)
type Both a = (a, a)

如果我们可以定义Functor (First a),Functor (Second a)和Functor (Both a)实例，那么fmap (+1) (2, 3)将是模棱两可的。

顺便说一句，您的发明被称为Church encoding。教会编码任何东西都是可能的。请参阅https://gist.github.com/rampion/2176199，了解在 Haskell 中实现几个 Church 编码（对、Maybe 和列表）。

于 2013-08-16T06:13:55.783 回答
1

不能部分应用类型同义词。

类型同义词只是帮助程序员的简写，而不是作为 Haskell 语言可以谈论的东西实际存在的东西。Haskell 处理类型同义词的唯一方法是“查看”它以查看右侧的类型。参数只是给你一种“宏语言”。

所以Maybe' a完全等价于forall b. (b -> (a -> b) -> b)。它的行为就像你写的一样forall b. (b -> (a -> b) -> b)。但是，什么是Maybe'没有争论的独立存在呢？Haskell 无法处理它Maybe'，它必须用其他东西替换它。但是什么？如果它意味着什么，它必须类似于\a ~> (forall b. (b -> (a -> b) -> b)，我在其中\a ~> ...用作类型级 lambda 的伪语法；从一种类型到另一种类型的任意函数。我必须为此编写语法的原因是因为 Haskell 对此没有语法，而它没有语法的原因是因为它无法处理完全通用的类型级函数。

我不确定支持任意类型级别的 lambda（类型构造函数和类型族实际上是非常受限的形式）实际上是否不可能，但这肯定非常困难。所以不能部分应用类型同义词。

要获得可以创建实例的Monad东西（需要可以应用于类型以创建类型的东西 - 某种东西* -> *），您需要使用data或newtype创建类型构造函数。类型同义词不能用于此目的。

于 2013-08-17T00:46:26.313 回答