如何使用更高级别的类型

Question

玩教堂的数字.我遇到的情况是我无法引导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
-}

它有效,但类型并不像它们那样干净.按照系统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

-}

我想应该可以add用Nat -> Nat -> Nat类型签名写,但我不知道如何.

PS实际上我从底部开始,但这样可能更容易呈现这个问题.

Answer 1

bennofs是正确的,你真的想帮助沿着这里的typechecker,特别是在add你需要实例化a在forall a . a -> (a -> a) -> a与Nat(即同一forall a . ...类型).

一种方法是引入一个包含多态类型的newtype:

newtype Nat' = N Nat

现在你可以进入Nat和Nat'通过N,然后回来使用unN

unN :: Nat' -> Nat
unN (N n) = n

(值得注意的是,这newtype Nat' = N Nat是一个不同的野兽data Nat2 = forall a . N2 (a -> (a -> a) -> a).后者需要,-XExistentialQuantification因为它说,对于某些特定的选择a,你可以做一个Nat2.另一方面,前者仍然说,如果你有a -> (a -> a) -> a任何任意a,那么你可以做一个Nat'.为Nat'你需要-XRankNTypes,但你不需要存在.)

现在我们也可以inc'增加一个Nat':

inc' :: Nat' -> Nat'
inc' (N n) = N (inc n)

我们准备添加:

add :: Nat -> Nat -> Nat
add n m = unN (n (N m) inc')

这样做的原因是因为现在不是试图说服GHC自己实例化n具有多态类型的类型? a . a -> (a -> a) -> a,N而是作为提示.

例:

> natInteger (add (inc zero) (inc zero))
2

Answer 2

我不太明白RankNTypes为什么你的原始示例不起作用，但如果你将 Nat 打包到数据类型中，那么它就可以工作：

{-# LANGUAGE RankNTypes #-}

module SystemF where

data Nat = Nat (forall a. (a -> (a -> a) -> a))

zero :: Nat
zero = Nat const

inc :: Nat -> Nat
inc (Nat n) = Nat $ \z s -> s $ n z s

natInteger :: Nat -> Integer
natInteger (Nat n) = n 0 (1+)

add :: Nat -> Nat -> Nat
add (Nat a) b = a b inc

现在该Nat类型是真正的数据类型，这对类型检查器很有帮助，因为它不必一直处理多态类型，只有当您实际“解包”它时才处理它。