如何使用更高等级的类型 [英] How to work with higher rank types

问题描述

玩教堂的数字。我遇到了这种情况，我无法引导高阶类型的GHC类型检查器。

首先，我编写了一个版本，没有任何类型的签名：

 模块ChurchStripped其中
 
零z _ = z 
 inc nzs =​​ s（nzs）
 natInteger n = n 0（1+）
 
 add ab = ab inc 
 
 { -  
 * ChurchStripped> natInteger $ add（inc $ inc zero）（inc $ inc $ inc zero）
 5 
  - } 
 
 mult ab = a zero（add b）
 
 { -  
 * ChurchStripped> natInteger $ mult（inc $ inc zero）（inc $ inc $ inc zero）
 6 
  - } 
  

推断的 mult 类型很糟糕，所以我尝试用类型定义清理类型：

 模块教会其中
 
类型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  - >整数
 natInteger n = n 0（1+）
 
 { - `add :: Nat a  - > Nat a  - > Nat a`不起作用，工作签名看起来已经可疑 - } 
 
 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＃ - } 
 
模块SystemF其中
 
类型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  - >整数
 natInteger n = n 0（1+）
 
 { - 这行不通了
 
 add :: Nat  - > Nat  - > Nat 
 add a b = a b inc 
 
无法匹配'forall a1'类型。 a1  - > （a1→a1）→> a1'
与`a  - > （a  - > a） - > a'
预期类型：（a  - >（a  - > a） - > a） - > a  - > （a  - > a） - > a 
实际类型：Nat  - > a  - > （a  - > a） - > a 
在'a'的第二个参数中，即'inc'
在表达式中：ab inc 
在add中的等式中：add ab = ab inc 
 
  - } 
  

我想应该可以写 add 与 Nat - > Nat - > Nat 类型的签名，但我不知道如何。

实际上我是从底部开始的，但是这样可能更容易呈现这个问题。

解决方案

我不明白 RankNTypes 足以说明原始示例不起作用的原因，但如果将Nat包装到数据类型中，则可以运行：

  { - ＃LANGUAGE RankNTypes＃ - } 
 
模块SystemF其中
 
数据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  - >整数
 natInteger（Nat n）= n 0（1+）
 
 add :: Nat  - > Nat  - > Nat 
 add（Nat a）b = ab inc 
  

现在 Nat type是一种真正的数据类型，它有助于类型检查器，因为它不必一直处理多态类型，只有当你实际解压缩它时。

Playing with the church numerals. I run into the situation I can't guide the GHC type-checker around higher order types.

First I wrote an version, without any type signatures:

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

The inferred type of mult is horrible, so I tried to clean-up the types with a type definitions:

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

It works, but the types aren't as clean as they could be. Following the System F definitions I tried:

{-# 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

-}

I guess it should be possible to write add with Nat -> Nat -> Nat type signature, but I have no idea how.

P.S. actually I started from the bottom, but it maybe easier to present this problem this way.

解决方案

I don't understand RankNTypes well enough to tell why your original example doesn't work, but if you pack Nat into a data type, then it works:

{-# 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

Now the Nat type is a real data type, which helps the type checker, because it doesn't have to deal with the polymorphic type all the time, only when you actually "unpack" it.

这篇关于如何使用更高等级的类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！