无法匹配Haskell中的多态类型 [英] Could not match polymorphic type in haskell

问题描述

我不确定下面的k4为什么不起作用，而k3起作用时，为什么它的多态性足够. ghci中的错误是

I am not sure why k4 below does not work, when k3 does, its enough polymorphic. The error in ghci is

• Couldn't match type ‘K' a0 a0’ with ‘End K'’
  Expected type: K' a0 a0 -> K'' a a

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
#!/usr/bin/env stack
-- stack --install-ghc --resolver lts-8.21 runghc --package http-conduit --package lens
{-# LANGUAGE ExistentialQuantification, RankNTypes #-}

module YonedaLan where

type End g = forall a. g a a 

data K'  b c = K'
data K'' b c = K''

k1 :: () -> End K'
k1 x = K'

k2 :: End K' -> End K''
k2 x = case x of (K') -> K''

k3 :: () -> End K''
k3 x = k2 ( k1 x)

k4 :: () -> End K''
k4 = k2 . k1

除了不编写自由点的样式外，还有一些最佳实践来应对这种情况吗?

Beside not writing point free style, is there some best practice for dealing with this ?

推荐答案

问题是GHC类型系统永远不会将类型变量实例化为多态类型.这样做将需要类型系统中的难以置信.

The problem is that the GHC type system will never instantiate a type variable to a polymorphic type. Doing that would require impredicativity in the type system.

在您的具体示例中，我们有

In your concrete example, we have

(.) :: (b->c) -> (a->b) -> (a->c)

，然后要键入check k2 . k1，我们需要实例化为多态类型的b ~ End K'.

and, to type check k2 . k1 we would need to instantiate b ~ End K' which is a polymorphic type.

典型的解决方法是将End K'设置为包装多态类型的单态类型.例如

A typical workaround would be to make End K' into a monomorphic type which wraps a polymorphic type. E.g.

newtype End g = End { unEnd :: forall a. g a a }

要付出的代价是在每次使用时明确包装/拆开类型为End g的值.利用GHC的安全胁迫"也可以缓解这种情况.

The price to pay is to explicitly wrap / unwrap values of type End g at every usage. This can also be mitigated exploiting GHC's "safe coercions".

请注意，其他一些语言(例如Agda，Coq，Idris)也可以很好地处理您的代码(适当翻译)，因为它们具有强制性的类型系统.但是，他们的推理机制与Haskell不同-难以置信使它变得更加困难.有时(如果不是经常的话)类型推断引擎找不到隐式类型参数，而必须显式提供类型.

Note that some other languages (like Agda, Coq, Idris) would handle your code (suitably translated) just fine, since they have an impredicative type system. However, their inference machinery are different from Haskell -- impredicativity makes it far harder. Sometimes, if not often, the type inference engine can't find the implicit type arguments, and types have to be explicitly provided.

这篇关于无法匹配Haskell中的多态类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！