Rank2Types的目的是什么?

And*_*kin 106 polymorphism haskell types higher-rank-types

我对Haskell并不十分精通,所以这可能是一个非常简单的问题.

Rank2Types解决了什么语言限制?Haskell中的函数是否已经支持多态参数?

Lui*_*las 157

除非你直接研究System F,否则很难理解更高级别的多态性,因为Haskell旨在为了简单起见隐藏你的细节.

但基本上,粗略的想法是多态类型并不真正具有a -> b他们在Haskell中所做的形式; 实际上,他们看起来像这样,总是用明确的量词:

id :: ?a.a ? a
id = ?t.?x:t.x
Run Code Online (Sandbox Code Playgroud)

如果您不知道"∀"符号,则将其读作"for all"; ?x.dog(x)意思是"对于所有x,x是狗." "Λ"是大写lambda,用于抽象类型参数; 第二行说的是id是一个接受类型t的函数,然后返回一个由该类型参数化的函数.

你可以看到,在系统F中,你不能只是立即将这样的函数应用于id值; 首先,您需要将Λ-函数应用于某个类型,以获得应用于值的λ函数.例如:

(?t.?x:t.x) Int 5 = (?x:Int.x) 5
                  = 5
Run Code Online (Sandbox Code Playgroud)

标准Haskell(即Haskell 98和2010)通过不使用任何这些类型量词,大写lambda和类型应用程序来简化这一点,但GHC在分析程序进行编译时将其置于幕后.(我相信这是所有编译时的东西,没有运行时开销.)

但是Haskell对此的自动处理意味着它假定"∀"永远不会出现在函数("→")类型的左侧分支上. Rank2TypesRankNTypes关闭这些限制,并允许您覆盖Haskell的默认规则以插入位置forall.

你为什么想做这个?因为完整的,不受限制的系统F是强大的,它可以做很多很酷的东西.例如,可以使用更高级别的类型来实现类型隐藏和模块化.例如,以下rank-1类型的普通旧函数(设置场景):

f :: ?r.?a.((a ? r) ? a ? r) ? r
Run Code Online (Sandbox Code Playgroud)

要使用f,主叫方首先必须选用什么类型ra,然后提供结果类型的参数.所以,你可以挑选r = Inta = String:

f Int String :: ((String ? Int) ? String ? Int) ? Int
Run Code Online (Sandbox Code Playgroud)

但现在将其与以下更高级别的类型进行比较:

f' :: ?r.(?a.(a ? r) ? a ? r) ? r
Run Code Online (Sandbox Code Playgroud)

这种类型的功能如何工作?好吧,要使用它,首先要指定要使用的类型r.我们选择Int:

f' Int :: (?a.(a ? Int) ? a ? Int) ? Int
Run Code Online (Sandbox Code Playgroud)

但现在?a位于功能箭头内部,因此您无法选择要使用的类型a; 你必须申请f' Int适当类型的Λ-函数.这意味着get 的实现f'选择要使用的类型a,而不是调用者f'.相反,没有更高级别的类型,呼叫者总是选择类型.

这对什么有用?嗯,实际上对于很多事情,但有一个想法是你可以使用它来模拟面向对象编程之类的东西,其中"对象"将一些隐藏数据与一些处理隐藏数据的方法捆绑在一起.因此,例如,具有两个方法的对象 - 一个返回一个Int,另一个返回一个String,可以用这种类型实现:

myObject :: ?r.(?a.(a ? Int, a -> String) ? a ? r) ? r
Run Code Online (Sandbox Code Playgroud)

这是如何运作的?该对象实现为具有隐藏类型的一些内部数据的函数a.为了实际使用该对象,它的客户端传递一个"回调"函数,该对象将使用这两种方法调用.例如:

myObject String (?a. ?(length, name):(a ? Int, a ? String). ?objData:a. name objData)
Run Code Online (Sandbox Code Playgroud)

在这里,我们基本上是调用对象的第二个方法,即一个类型a ? String为未知的方法a.嗯,myObject客户不知道; 但是这些客户从签名中知道他们能够将两个函数中的任何一个应用于它,并获得一个Int或一个String.

对于一个实际的Haskell示例,下面是我自学时编写的代码RankNTypes.这实现了一种类型ShowBox,它将一些隐藏类型的值与其Show类实例捆绑在一起.请注意,在底部的示例中,我列出了ShowBox第一个元素是由数字构成的,第二个元素来自字符串.由于使用较高级别类型隐藏了类型,因此不违反类型检查.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}

type ShowBox = forall b. (forall a. Show a => a -> b) -> b

mkShowBox :: Show a => a -> ShowBox
mkShowBox x = \k -> k x

-- | This is the key function for using a 'ShowBox'.  You pass in
-- a function @k@ that will be applied to the contents of the 
-- ShowBox.  But you don't pick the type of @k@'s argument--the 
-- ShowBox does.  However, it's restricted to picking a type that
-- implements @Show@, so you know that whatever type it picks, you
-- can use the 'show' function.
runShowBox :: forall b. (forall a. Show a => a -> b) -> ShowBox -> b
-- Expanded type:
--
--     runShowBox 
--         :: forall b. (forall a. Show a => a -> b) 
--                   -> (forall b. (forall a. Show a => a -> b) -> b)
--                   -> b
--
runShowBox k box = box k


example :: [ShowBox] 
-- example :: [ShowBox] expands to this:
--
--     example :: [forall b. (forall a. Show a => a -> b) -> b]
--
-- Without the annotation the compiler infers the following, which
-- breaks in the definition of 'result' below:
--
--     example :: forall b. [(forall a. Show a => a -> b) -> b]
--
example = [mkShowBox 5, mkShowBox "foo"]

result :: [String]
result = map (runShowBox show) example
Run Code Online (Sandbox Code Playgroud)

PS:对于任何读过这个想知道ExistentialTypesGHC 如何使用的人forall,我相信原因是因为它在幕后使用这种技术.

  • 如果你有`exists`关键字,你可以定义一个存在类型(例如)`data Any = Any(exists a.a)`,其中`Any ::(存在a .a) - > Any`.使用∀xP(x)→Q≡(∃xP(x))→Q,我们可以得出结论:'Any`也可以有一个类型`forall a.a - > Any`,这就是`forall`关键字的来源.我相信GHC实现的存在类型只是普通的数据类型,它们也带有所有必需的类型类词典(我找不到参考支持这个,对不起). (5认同)
  • 谢谢你非常精心的回答!(顺便说一下,这也最终激励我学习正确的类型理论和系统F.) (2认同)
  • @Vitus:GHC存在与类型词典无关.你可以有`数据ApplyBox r = forall a.ApplyBox(a - > r)a`; 当你将模式匹配到`ApplyBox fx`时,你会得到`f :: h - > r`和`x :: h`来获得一个"隐藏的"限制类型`h`.如果我理解正确,类型类字典案例将被翻译成如下:`data ShowBox = forall a.显示一个=> ShowBox a`被翻译成`data ShowBox'= forall a.ShowBox'(ShowDict'a)a`; `instance Show ShowBox'where show(ShowBox'dict val)= show'dict val`; `show':: ShowDict a - > a - > String`. (2认同)

sep*_*p2k 113

Haskell中的函数是否已经支持多态参数?

它们可以,但只有1级.这意味着虽然您可以编写一个函数,在没有此扩展的情况下使用不同类型的参数,但是您不能在同一个调用中编写将其参数用作不同类型的函数.

例如,如果没有此扩展名,g则无法键入以下函数,因为在定义中使用了不同的参数类型f:

f g = g 1 + g "lala"
Run Code Online (Sandbox Code Playgroud)

请注意,将多态函数作为参数传递给另一个函数是完全可能的.所以类似的东西map id ["a","b","c"]是完全合法的.但该函数可能只将其用作单形.在示例中map使用id,就好像它有类型String -> String.当然,您也可以传递给定类型的简单单形函数而不是id.没有rank2types,函数无法要求其参数必须是多态函数,因此也无法将其用作多态函数.

  • 添加一些连接我的答案的单词:考虑Haskell函数`f'gxy = gx + gy`.它的推断等级-1类型是"forall a r".Num r =>(a - > r) - > a - > a - > r`.由于`forall a`在函数箭头之外,调用者必须首先为`a`选择一个类型; 如果他们选择`Int`,我们得到`f':: forall r.Num r =>(Int - > r) - > Int - > Int - > r`,现在我们已经修复了`g`参数,所以它可以采用`Int`而不是`String`.如果我们启用`RankNTypes`,我们可以使用类型`forall bc r注释`f'`.Num r =>(forall a.a - > r) - > b - > c - > r`.但不能使用它 - 会是什么? (5认同)

dfe*_*uer 42

路易斯·卡西利亚斯的答案提供了很多关于2级类型意味着什么的很好的信息,但我只是扩展他没有涵盖的一点.要求参数是多态的,不仅仅允许它与多种类型一起使用; 它还限制了该函数对其参数的作用以及它如何产生其结果.也就是说,它给呼叫者提供了较小的灵活性.你为什么想这么做?我将从一个简单的例子开始:

假设我们有一个数据类型

data Country = BigEnemy | MediumEnemy | PunyEnemy | TradePartner | Ally | BestAlly
Run Code Online (Sandbox Code Playgroud)

我们想写一个函数

f g = launchMissilesAt $ g [BigEnemy, MediumEnemy, PunyEnemy]
Run Code Online (Sandbox Code Playgroud)

它接受一个函数,该函数应该选择它给出的列表中的一个元素,并返回一个IO在该目标上发射导弹的动作.我们可以给出f一个简单的类型:

f :: ([Country] -> Country) -> IO ()
Run Code Online (Sandbox Code Playgroud)

问题是我们可能会意外地跑

f (\_ -> BestAlly)
Run Code Online (Sandbox Code Playgroud)

然后我们就会遇到大麻烦!给出f1级多态类型

f :: ([a] -> a) -> IO ()
Run Code Online (Sandbox Code Playgroud)

没有任何帮助,因为我们a在打电话时选择了类型f,我们只是将它专门化Country\_ -> BestAlly再次使用我们的恶意软件.解决方案是使用rank 2类型:

f :: (forall a . [a] -> a) -> IO ()
Run Code Online (Sandbox Code Playgroud)

现在我们传入的函数需要是多态的,所以\_ -> BestAlly不要键入check!事实上,没有函数返回不在列表中的元素将进行类型检查(尽管一些函数进入无限循环或产生错误因此永远不会返回).

当然,上述是设计的,但这种技术的变化是使STmonad安全的关键.


Ben*_*son 15

较高等级的类型并不像其他答案那样具有异国情调.信不信由你,许多面向对象的语言(包括Java和C#!)都以它们为特色.(当然,这些社区中没有人通过可怕的名字"更高级别的类型"来了解它们.)

我想给这个例子是一个教科书实现Visitor模式,我用的所有的时间在我的日常工作.这个答案并非旨在介绍访客模式; 知识在其他地方很容易 获得 .

在这个虚构的虚构人力资源应用程序中,我们希望对可能是全职长期员工或临时承包商的员工进行操作.我首选的访问者模式变体(实际上是与之相关的变量RankNTypes)参数化访问者的返回类型.

interface IEmployeeVisitor<T>
{
    T Visit(PermanentEmployee e);
    T Visit(Contractor c);
}

class XmlVisitor : IEmployeeVisitor<string> { /* ... */ }
class PaymentCalculator : IEmployeeVisitor<int> { /* ... */ }
Run Code Online (Sandbox Code Playgroud)

关键是许多具有不同返回类型的访问者都可以对相同的数据进行操作.这意味着IEmployee必须表达对T应该是什么的意见.

interface IEmployee
{
    T Accept<T>(IEmployeeVisitor<T> v);
}
class PermanentEmployee : IEmployee
{
    // ...
    public T Accept<T>(IEmployeeVisitor<T> v)
    {
        return v.Visit(this);
    }
}
class Contractor : IEmployee
{
    // ...
    public T Accept<T>(IEmployeeVisitor<T> v)
    {
        return v.Visit(this);
    }
}
Run Code Online (Sandbox Code Playgroud)

我想提请你注意这些类型.观察到IEmployeeVisitor普遍量化其返回类型,而IEmployee在其Accept方法中量化它- 也就是说,在更高的等级.从C#到Haskell的匆匆翻译:

data IEmployeeVisitor r = IEmployeeVisitor {
    visitPermanent :: PermanentEmployee -> r,
    visitContractor :: Contractor -> r
}

newtype IEmployee = IEmployee {
    accept :: forall r. IEmployeeVisitor r -> r
}
Run Code Online (Sandbox Code Playgroud)

所以你有它.当您编写包含泛型方法的类型时,更高级别的类型会显示在C#中.

  • 我很想知道是否有其他人写过有关 C#/Java/Blub 对更高级别类型的支持的文章。亲爱的读者,如果您知道任何此类资源,请将其发送给我! (2认同)