单态限制对类型约束的影响 [英] Effects of monomorphism restriction on type class constraints

问题描述

此代码在添加 baz 的类型声明时中断：

  baz（x：y：_）= x == y 
 baz [_] = baz [] 
 baz [] = False 
  

常见解释（参见>为什么我不能声明推断的类型？）是因为多态递归。

但是这个解释不适用使用另一个多态递归示例解释效果消失的原因：

  foo f（x：y：_）= fxy 
 foo f [_] = foo f [] 
 foo f [] = False 
  

它也没有解释为什么GHC认为递归是单形的，没有类型声明。

可以用来解释示例是否可以读取在 http://www.haskell.org/onlinereport/decls.h tml＃sect4.5.5 应用于我的 baz 个案？

I。添加签名会消除单形性限制，并且在没有限制的情况下右边[]出现含糊不清的情况，并且出现一个'固有含糊'的类型 forall a。公式a => [a] ？

解决方案

baz 在一个绑定组中，泛化在完成整个组的输入后完成。没有类型签名，这意味着 baz 被假定为单式，因此递归中的 [] 类型调用是由那个（看ghc的-ddump -simput输出）。使用类型签名时，编译器被明确告知函数是多态的，所以它不能假定递归调用中的 [] 类型是相同的，因此它是不明确的。

正如John L所说，在 foo 中，类型由 f - 只要 f 具有monotype。您可以通过将 f 与（==）（需要<$ c $）相同的类型来创建相同的歧义c> Rank2Types ），

  { - ＃LANGUAGE Rank2Types＃ - } 
 foo： ：等式b => （方程式a => a  - > a  - > Bool） - > [b]  - > Bool 
 foo f（x：y：_）= fxy 
 foo f [_] = foo f [] 
 foo _ [] = False 
  

给出

 模糊变量`b0 '在约束中：
（Eq b0）由于使用'foo'引起
可能的修复：添加修复这些类型变量的类型签名
在表达式中：foo f [] 
在'foo'的等式中：foo f [_] = foo f [] 
  

This code breaks when a type declaration for baz is added:

baz (x:y:_) = x == y
baz [_] = baz []
baz [] = False

A common explanation (see Why can't I declare the inferred type? for an example) is that it's because of polymorphic recursion.

But that explanation doesn't explain why the effect disappears with another polymorphically recursive example:

foo f (x:y:_) = f x y
foo f [_] = foo f []
foo f [] = False

It also doesn't explain why GHC thinks the recursion is monomorphic without type declaration.

Can the explanation of the example with reads in http://www.haskell.org/onlinereport/decls.html#sect4.5.5 be applied to my baz case?

I.e. adding a signature removes monomorphism restriction, and without the restriction an ambiguity of right-side [] appears, with an 'inherently ambigous' type of forall a . Eq a => [a]?

解决方案

The equations for baz are in one binding group, generalisation is done after the entire group has been typed. Without a type signature, that means baz is assumed to have a monotype, so the type of [] in the recursive call is given by that (look at ghc's -ddump-simpl output). With a type signature, the compiler is explicitly told that the function is polymorphic, so it can't assume the type of [] in the recursive call to be the same, hence it's ambiguous.

As John L said, in foo, the type is fixed by the occurrence of f - as long as f has a monotype. You can create the same ambiguity by giving f the same type as (==) (which requires Rank2Types),

{-# LANGUAGE Rank2Types #-}
foo :: Eq b => (forall a. Eq a => a -> a -> Bool) -> [b] -> Bool
foo f (x:y:_) = f x y
foo f[_] = foo f []
foo _ [] = False

That gives

Ambiguous type variable `b0' in the constraint:
  (Eq b0) arising from a use of `foo'
Probable fix: add a type signature that fixes these type variable(s)
In the expression: foo f []
In an equation for `foo': foo f [_] = foo f []

这篇关于单态限制对类型约束的影响的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！