haskell 不理解类型等价性

bkhjykvo  于 2023-10-19  发布在  其他
关注(0)|答案(2)|浏览(139)

Haskell教程(https://www.fpcomplete.com/haskell/tutorial/monad-transformers/)说,如果我们假设以下定义

newtype State s a = State (s -> (s, a))

则以下定义

newtype StateEither s e a = StateEither (State s (Either e a))

是对

newtype StateEither s e a = StateEither (s -> (s, Either e a))

哪些替代步骤使之成为可能?

rslzwgfq

rslzwgfq1#

这两个人并不是互相改写的:类型检查器将不会推断出这两者是相同的。然而,两者非常相似。
实际上,State类型定义为:

newtype State s a = State (s -> (s, a))

这意味着对于State s a,它将s -> (a, s)函数 Package 到State数据构造函数中。如果我们因此删除State数据构造函数,我们可以将其视为一个类型为s -> (a, s)的函数,因此:

type State s a = s -> (s, a)

在这种情况下,类型State s (Either e a)因此具有类型:

s -> (s, Either e a)

因此:

newtype StateEither s e a = StateEither (State s (Either e a))

将等同于:

newtype StateEither s e a = StateEither (s -> (s, Either e a))

这里使用newtype。这对于为类型类定义不同的示例很有用,因为函数也是Monad的示例,但是我们想为StateMonad定义不同的instance

rxztt3cl

rxztt3cl2#

对于Data.Type.Coercion,编译器可以证明它们相等。这种类型的值包含两种类型是可强制的证明:

witness :: Coercion (State s (Either e a))
                    (s -> (Either e a, s))
witness = Coercion

一个更有成效的见证方式是从中获取示例。
如果你可以通过Compose (State s) (Either e)导出StateEither s e的示例,这就证明了它们在表示上是相等的。

type    StateEither :: Type -> Type -> Type -> Type
newtype StateEither s e a = StateEither (s -> (Either e a, s))
  deriving (Functor, Applicative)
  via Compose (State s) (Either e)

当完全应用时,StateEither s e a不仅与State s (Either e a)同构,而且它们在内存中的表示相同,并且可以零成本并行。

StateEither s e a
~R Compose (State s) (Either e) a
~R State s (Either e a)
~R s -> (a, Either e a)

相关问题