标签: higher-rank-types

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

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

我很难STArray通过Google找到的文档和其他howtos /讨论来理解.我在下面有一些更相关的问题.

根据文档,STArrays是

ST monad中的可变盒装和未装箱阵列.

这给了我一个印象,那STArray就是用作在函数之间传递的状态(假设你有一个必须经常更新的向量).

显然,这使用的方式不同:

ST s (STArray s a e)

s这里的州是什么？如果它是在内部使用的,那么为什么这不会被用户隐藏？

这也意味着,如果我们想要将一个STArray s Int Int被传递为状态,那么就可以定义

type StateArray a = Control.Monad.State (ST s (STArray s Int Int)) a

这看起来相当麻烦.

最后,

• ST和之间有什么区别State？
• 什么是STArray和IOArray,如果ST和IO是否意味着"内部"使用？

谢谢!!

我只能以相当笨拙的方式在Idris 0.9.12中执行rank-n类型:

tupleId : ((a : Type) -> a -> a) -> (a, b) -> (a, b)
tupleId f (a, b) = (f _ a, f _ b)

我需要在有类型应用程序的地方使用下划线,因为当我尝试隐藏(嵌套)类型参数时,Idris会抛出解析错误:

tupleId : ({a : Type} -> a -> a) -> (a, b) -> (a, b) -- doesn't compile

一个可能更大的问题是我根本不能在更高级别的类型中进行类约束.我无法将以下Haskell函数转换为Idris:

appShow :: Show a => (forall a. Show a => a -> String) -> a -> String
appShow show x = show x

这也防止我使用伊德里斯用作类型同义词类型,例如Lens,这是Lens s t a b = …

据我所知,对于秩2类型存在(仅)可判定类型检查算法.GHC是否以某种方式使用这一事实,它是否具有任何实际意义？

是否还存在秩-2类型的主要类型概念和类型推理算法？如果是,GHC会使用吗？

是否有秩2种以上秩任何其他优势ñ类型？

我已经看到了一些用于rank-2多态性的用例(最突出的例子是ST monad),但是没有比这更高级别的用例.有谁知道这样的用例？

编译好:

type List a = [a]

但是当我引入类约束时,编译器要求RankNTypes包括:

type List2 a = Num a => [a]

包含该扩展后,它编译得很好.为什么编译代码需要扩展名？

编辑:为什么我首先需要约束？

我检查这个镜头类型(type RefF a b = Functor f => (b -> f b) -> (a -> f a)从)这个职位,并发现它实际需要的RankNTypes,因为的Functor约束.

较高等级的类型看起来很有趣.从Haskell wikibook到这个例子:

foo :: (forall a. a -> a) -> (Char,Bool)
foo f = (f 'c', f True)

现在我们可以在foo id没有编译器爆炸的情况下进 这个例子在书中很快被我在其他几个地方看到的真实世界的例子:ST monad和runST.那很酷.

但是我还没有遇到过这样一种情况:我通过使用更高级别的参数编写自己的函数来解决问题.你呢？您在野外有什么样的rank-2或rank-n多态性？

我们习惯于为多态函数提供普遍量化的类型.存在量化类型的使用频率较低.我们如何使用通用型量词来表达存在量化类型？

forall这段代码中s 的目的是什么？

class  Monad m  where
    (>>=)       :: forall a b. m a -> (a -> m b) -> m b
    (>>)        :: forall a b. m a -> m b -> m b
        -- Explicit for-alls so that we know what order to
        -- give type arguments when desugaring

(省略了一些代码).这来自Monads的代码.

我的背景:我不太懂,forall或者Haskell隐含地拥有它们.

此外,它可能并不重要,但GHCi允许我forall在给出>>类型时省略:

Prelude> :t (>>) :: Monad m => m a -> m b -> m b
(>>) :: Monad …

说我有一个功能:

f :: Int -> (Rational, Integer)
f b = ((toRational b)+1,(toInteger b)+1)

我想像这样抽象出(+1):

f :: Int -> (Rational, Integer)
f b = (h (toRational b)
      ,h (toInteger b))
    where h = (+1)

这显然不会起作用,但如果我指定类型签名,它将起作用:

f :: Int -> (Rational, Integer)
f b = (h (toRational b)
      ,h (toInteger b))
    where h :: Num a => a -> a
          h = (+1)

假设我现在想通过传递h作为参数来进一步抽象函数:

f :: Num a => Int -> (a -> a) -> (Rational, Integer)
f b g = (h …