与RankNTypes扩展相关的奇怪类型 [英] Strange type inferencе with RankNTypes extension

问题描述

我试图在Haskell中尝试System-F类型，并通过 type 实现了自然数的Church编码。

I am trying to experiment with System-F types in Haskell and have implemented Church encoding of natural numbers via type.

当加载此代码时

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE RankNTypes #-}

type CNat = forall t . (t -> t) -> (t -> t)

c0 :: CNat
c0 _ x = x

type CPair a b = forall t . (a -> b -> t) -> t

cpair :: a -> b -> CPair a b
cpair a b f = f a b

-- pair3 :: CPair CNat String
pair3 = cpair c0 "hello"

转换为ghci 7.8.2我收到警告：

into ghci 7.8.2 I get a warning:

λ: :l test.hs 
[1 of 1] Compiling Main             ( test.hs, interpreted )

test.hs:29:1: Warning:
    Top-level binding with no type signature:
      pair3 :: forall t t1.
               (((t1 -> t1) -> t1 -> t1) -> [Char] -> t) -> t
Ok, modules loaded: Main.
λ: 

现在的问题是，不应该是

The question is, shouldn't the type be

pair3 :: forall t.
      ((forall t1. (t1 -> t1) -> t1 -> t1) -> [Char] -> t) -> t

？

UPD ：提供了一个简单的例子

UPD: A simpler example is provided

推荐答案

键入它，以便当
我明确指定它（取消注释行中的代码），编译器
不会推断它，但只检查提供的类型？现在我得到了
错误

But is there any way to specify my type for it so that when I specify it explicitly (uncomment the line in my code), the compiler would not infer it but just check the provided type? Now I am getting error

如果你想实例化类型变量 a，b 出现在 cpair 类型中，您可以添加以下显式注释。

If you want to instantiate the type variables a,b occurring in the type of cpair, you can add the following explicit annotation.

pair3 :: CPair CNat String
pair3 = (cpair :: CNat -> String -> CPair CNat String) c0 "hello"

没有那个，我相信 cpair 仅在单形类型中实例化。

Without that, cpair is only instantiated at monomorphic types, I believe.

这篇关于与RankNTypes扩展相关的奇怪类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！