【发布时间】：2014-01-21 13:45:20
【问题描述】：
玩弄教堂的数字。我遇到了无法引导 GHC 类型检查器处理高阶类型的情况。
首先我写了一个版本，没有任何类型签名：
module ChurchStripped where
zero z _ = z
inc n z s = s (n z s)
natInteger n = n 0 (1+)
add a b = a b inc
{-
*ChurchStripped> natInteger $ add (inc $ inc zero) (inc $ inc $ inc zero)
5
-}
mult a b = a zero (add b)
{-
*ChurchStripped> natInteger $ mult (inc $ inc zero) (inc $ inc $ inc zero)
6
-}
mult 的推断类型太可怕了，所以我尝试使用类型定义来清理类型：
module Church where
type Nat a = a -> (a -> a) -> a
zero :: Nat a
zero z _ = z
inc :: Nat a -> Nat a
inc n z s = s (n z s)
natInteger :: Nat Integer -> Integer
natInteger n = n 0 (1+)
{- `add :: Nat a -> Nat a -> Nat a` doesn't work, and working signature looks already suspicious -}
add :: Nat (Nat a) -> Nat a -> Nat a
add a b = a b inc
{-
*Church> natInteger $ add (inc $ inc zero) (inc $ inc $ inc zero)
5
-}
mult :: Nat (Nat a) -> Nat (Nat a) -> Nat a
mult a b = a zero (add b)
{-
*Church> natInteger $ mult (inc $ inc zero) (inc $ inc $ inc zero)
6
-}
它可以工作，但类型不够干净。按照我尝试的System F 定义：
{-# LANGUAGE RankNTypes #-}
module SystemF where
type Nat = forall a. a -> (a -> a) -> a
zero :: Nat
zero z _ = z
inc :: Nat -> Nat
inc n z s = s (n z s)
natInteger :: Nat -> Integer
natInteger n = n 0 (1+)
{- This doesn't work anymore
add :: Nat -> Nat -> Nat
add a b = a b inc
Couldn't match type `forall a1. a1 -> (a1 -> a1) -> a1'
with `a -> (a -> a) -> a'
Expected type: (a -> (a -> a) -> a) -> a -> (a -> a) -> a
Actual type: Nat -> a -> (a -> a) -> a
In the second argument of `a', namely `inc'
In the expression: a b inc
In an equation for `add': add a b = a b inc
-}
我想应该可以用Nat -> Nat -> Nat类型签名写add，但我不知道怎么做。
附：其实我是从底层开始的，不过这样表述这个问题可能更容易些。
【问题讨论】：
-
forall 引入了排名更高的类型，这肯定不是你想要的。
-
@Ingo 我不明白为什么不
-
换一种说法：您在类型中提到的每个
Nat都会有自己的a类型变量，它不能与您签名中的任何其他类型变量统一，但显然，我们写Nat -> Nat你希望as 是一样的。 -
@Ingo，不，真的希望它保持通用性。这有点像
id id案例（这不是很有趣，但很有效）。 gist.github.com/phadej/8540770 -
也许你想将类型定义为
(a->a)->(a->a)。
标签： haskell