如何测试应用实例的同态定律?

Jul*_*ang 1 haskell proof typeclass applicative homomorphism

我正在做Typeclassopedia的练习; 在Applicative节中,我写ZipListpure功能,并检查它是否遵循Applicative法律.

我检查过:

  • 身份法
  • 交换法
  • 组成法

但是当我试图检查"同态"定律时,我发现GHCi没有得到结果MZipList.

我想这是因为我错过了指定pure我的Applicative类型课程.如何立即运行pure没有<*>它的功能Applicative

这是MZipList定义和类实例:

newtype MZipList a = MZipList { getZipList :: [a] }
    deriving (Show)

instance Functor MZipList where
  fmap gs x = pure gs <*> x

instance Applicative MZipList where
  pure a= MZipList (repeat a)
  (MZipList gs) <*> (MZipList xs) = MZipList (zipWith ($) gs xs)
Run Code Online (Sandbox Code Playgroud)

当我检查"交换"法时,例如:

*Main> (MZipList [(*2),(*3),(*4)]) <*> pure (2)
MZipList {getZipList = [4,6,8]}
*Main> pure ($ 2) <*> (MZipList [(*2),(*3),(*4)])
MZipList {getZipList = [4,6,8]}
Run Code Online (Sandbox Code Playgroud)

但是,当我检查"同态"的法律,MZipListpure不叫:

*Main> pure (*2) <*> pure 2
4
*Main>  pure ((*2) 2)
4
*Main>
Run Code Online (Sandbox Code Playgroud)

这是为什么?

Sho*_*hoe 6

什么是pure

pure只是一个在特定Applicativemonad中"插入"对象的函数.例如:

test :: [Int]
test = pure 1 -- [1]
Run Code Online (Sandbox Code Playgroud)

我们正在插入1monad列表,这会产生单例[1].如果您已经阅读过该Monad课程,那么pure基本上是相同的return(如果您不必担心).

您的实例Applicative似乎工作正常.

你的考试

在GHCi中运行命令时,你基本上是IOmonad,也是一个Applicative.所以一般来说,pure x返回一个IO (type of x).

在:

pure (*2) <*> pure 2
Run Code Online (Sandbox Code Playgroud)

你正在"放置" (*2)一个IO对象,然后放入2一个IO对象,最后<*>按照中的定义进行调用instance Applicative IO.

您没有测试您的MZipList实例.

在第二个例子中,您只需调用:

pure ((*2) 2)
Run Code Online (Sandbox Code Playgroud)

如果你还记得,(*2) 2仅仅适用(*2)2,从而真正执行2 * 2.所以你的电话实际上是:

pure 4
Run Code Online (Sandbox Code Playgroud)

在GHCi中(仍然在IOmonad 的上下文中)返回一个IO Int对象.

如何正确测试

要测试"同态"定律,您只需要给编译器一个关于您真正想要的类型的小提示:

所以代替:

pure (*2) <*> pure 2
Run Code Online (Sandbox Code Playgroud)

你会写:

pure (*2) <*> (pure 2 :: MZipList Int)
Run Code Online (Sandbox Code Playgroud)

Live demo