haskell - 如何与更高级别的类型合作

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
-}

它可以工作，但类型并不像应有的那么干净。继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 ，但我不知道如何实现。

附注实际上我是从底层开始的，但这样表达这个问题可能更容易。

Answer 1

bennofs 是对的，你真的想在这里帮助类型检查器，特别是在 add 中。您需要在其中实例化 a在forall a . a -> (a -> a) -> a与 Nat (即相同的 forall a . ... 类型)。

一种方法是引入一个包装多态类型的新类型:

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